doc-src/System/Thy/document/Presentation.tex
author wenzelm
Mon Jan 04 11:55:23 2010 +0100 (2010-01-04 ago)
changeset 34238 b28be884edda
parent 32088 2110fcd86efb
child 35587 f037aa6699c3
permissions -rw-r--r--
discontinued special HOL_USEDIR_OPTIONS;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Presentation}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Presentation\isanewline
    12 \isakeyword{imports}\ Pure\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{Presenting theories \label{ch:present}%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \begin{isamarkuptext}%
    26 Isabelle provides several ways to present the outcome of formal
    27   developments, including WWW-based browsable libraries or actual
    28   printable documents.  Presentation is centered around the concept of
    29   \emph{logic sessions}.  The global session structure is that of a
    30   tree, with Isabelle Pure at its root, further object-logics derived
    31   (e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions
    32   in leaf positions (usually without a separate image).
    33 
    34   The Isabelle tools \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} and \indexref{}{tool}{make}\hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} provide
    35   the primary means for managing Isabelle sessions, including proper
    36   setup for presentation.  Here the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} tool takes care
    37   to let \indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} process run any
    38   additional stages required for document preparation, notably the
    39   tools \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} and \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}}.  The complete tool
    40   chain for managing batch-mode Isabelle sessions is illustrated in
    41   \figref{fig:session-tools}.
    42 
    43   \begin{figure}[htbp]
    44   \begin{center}
    45   \begin{tabular}{lp{0.6\textwidth}}
    46 
    47       \verb|isabelle| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} & invoked once by the user
    48       to create the initial source setup (common \verb|IsaMakefile| plus a single session directory); \\
    49 
    50       \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} & invoked repeatedly by the
    51       user to keep session output up-to-date (HTML, documents etc.); \\
    52 
    53       \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} & part of the standard
    54       \verb|IsaMakefile| entry of a session; \\
    55 
    56       \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} & run through \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}; \\
    57 
    58       \verb|isabelle| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} & run by the Isabelle
    59       process if document preparation is enabled; \\
    60 
    61       \verb|isabelle| \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} & universal {\LaTeX} tool
    62       wrapper invoked multiple times by \verb|isabelle| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}; also useful for manual experiments; \\
    63 
    64   \end{tabular}
    65   \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
    66   \end{center}
    67   \end{figure}%
    68 \end{isamarkuptext}%
    69 \isamarkuptrue%
    70 %
    71 \isamarkupsection{Generating theory browser information \label{sec:info}%
    72 }
    73 \isamarkuptrue%
    74 %
    75 \begin{isamarkuptext}%
    76 \index{theory browsing information|bold}
    77 
    78   As a side-effect of running a logic sessions, Isabelle is able to
    79   generate theory browsing information, including HTML documents that
    80   show a theory's definition, the theorems proved in its ML file and
    81   the relationship with its ancestors and descendants.  Besides the
    82   HTML file that is generated for every theory, Isabelle stores links
    83   to all theories in an index file. These indexes are linked with
    84   other indexes to represent the overall tree structure of logic
    85   sessions.
    86 
    87   Isabelle also generates graph files that represent the theory
    88   hierarchy of a logic.  There is a graph browser Java applet embedded
    89   in the generated HTML pages, and also a stand-alone application that
    90   allows browsing theory graphs without having to start a WWW client
    91   first.  The latter version also includes features such as generating
    92   Postscript files, which are not available in the applet version.
    93   See \secref{sec:browse} for further information.
    94 
    95   \medskip
    96 
    97   The easiest way to let Isabelle generate theory browsing information
    98   for existing sessions is to append ``\verb|-i true|'' to the
    99   \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} before invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} (or \hyperlink{file.$ISABELLE-HOME/build}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}build}}}}).  For
   100   example, add something like this to your Isabelle settings file
   101 
   102 \begin{ttbox}
   103 ISABELLE_USEDIR_OPTIONS="-i true"
   104 \end{ttbox}
   105 
   106   and then change into the \hyperlink{file.~~/src/FOL}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL}}}} directory and run
   107   \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|.  The presentation output will appear in
   108   \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
   109   \verb|~/.isabelle/browser_info/FOL|.  Note that option
   110   \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
   111   more explicit about such details.
   112 
   113   Many standard Isabelle sessions (such as \hyperlink{file.~~/src/HOL/ex}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}ex}}}})
   114   also provide actual printable documents.  These are prepared
   115   automatically as well if enabled like this, using the \verb|-d| option
   116 \begin{ttbox}
   117 ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
   118 \end{ttbox}
   119   Enabling options \verb|-i| and \verb|-d|
   120   simultaneously as shown above causes an appropriate ``document''
   121   link to be included in the HTML index.  Documents (or raw document
   122   sources) may be generated independently of browser information as
   123   well, see \secref{sec:tool-document} for further details.
   124 
   125   \bigskip The theory browsing information is stored in a
   126   sub-directory directory determined by the \indexref{}{setting}{ISABELLE\_BROWSER\_INFO}\hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} setting plus a prefix corresponding to the
   127   session identifier (according to the tree structure of sub-sessions
   128   by default).  A complete WWW view of all standard object-logics and
   129   examples of the Isabelle distribution is available at the usual
   130   Isabelle sites:
   131   \begin{center}\small
   132   \begin{tabular}{l}
   133     \url{http://isabelle.in.tum.de/dist/library/} \\
   134     \url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/} \\
   135     \url{http://mirror.cse.unsw.edu.au/pub/isabelle/dist/library/} \\
   136   \end{tabular}
   137   \end{center}
   138   
   139   \medskip In order to present your own theories on the web, simply
   140   copy the corresponding subdirectory from \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} to your WWW server, having generated browser
   141   info like this:
   142 \begin{ttbox}
   143 isabelle usedir -i true HOL Foo
   144 \end{ttbox}
   145 
   146   This assumes that directory \verb|Foo| contains some \verb|ROOT.ML| file to load all your theories, and HOL is your parent
   147   logic image (\verb|isabelle| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} assists in
   148   setting up Isabelle session directories.  Theory browser information
   149   for HOL should have been generated already beforehand.
   150   Alternatively, one may specify an external link to an existing body
   151   of HTML data by giving \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} a \verb|-P| option like
   152   this:
   153 \begin{ttbox}
   154 isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
   155 \end{ttbox}
   156 
   157   \medskip For production use, the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} tool is usually
   158   invoked in an appropriate \verb|IsaMakefile|, via the Isabelle
   159   \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} tool.  There is a separate \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool to
   160   provide easy setup of all this, with only minimal manual editing
   161   required.
   162 \begin{ttbox}
   163 isabelle mkdir HOL Foo && isabelle make
   164 \end{ttbox}
   165   See \secref{sec:tool-mkdir} for more information on preparing
   166   Isabelle session directories, including the setup for documents.%
   167 \end{isamarkuptext}%
   168 \isamarkuptrue%
   169 %
   170 \isamarkupsection{Browsing theory graphs \label{sec:browse}%
   171 }
   172 \isamarkuptrue%
   173 %
   174 \begin{isamarkuptext}%
   175 \index{theory graph browser|bold} 
   176 
   177   The Isabelle graph browser is a general tool for visualizing
   178   dependency graphs.  Certain nodes of the graph (i.e.~theories) can
   179   be grouped together in ``directories'', whose contents may be
   180   hidden, thus enabling the user to collapse irrelevant portions of
   181   information.  The browser is written in Java, it can be used both as
   182   a stand-alone application and as an applet.  Note that the option
   183   \verb|-g| of \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
   184   graph presentations in batch mode for inclusion in session
   185   documents.%
   186 \end{isamarkuptext}%
   187 \isamarkuptrue%
   188 %
   189 \isamarkupsubsection{Invoking the graph browser%
   190 }
   191 \isamarkuptrue%
   192 %
   193 \begin{isamarkuptext}%
   194 The stand-alone version of the graph browser is wrapped up as an
   195   Isabelle tool called \indexdef{}{tool}{browser}\hypertarget{tool.browser}{\hyperlink{tool.browser}{\mbox{\isa{\isatt{browser}}}}}:
   196 
   197 \begin{ttbox}
   198 Usage: browser [OPTIONS] [GRAPHFILE]
   199 
   200   Options are:
   201     -c           cleanup -- remove GRAPHFILE after use
   202     -o FILE      output to FILE (ps, eps, pdf)
   203 \end{ttbox}
   204   When no filename is specified, the browser automatically changes to
   205   the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}.
   206 
   207   \medskip The \verb|-c| option causes the input file to be
   208   removed after use.
   209 
   210   The \verb|-o| option indicates batch-mode operation, with the
   211   output written to the indicated file; note that \verb|pdf|
   212   produces an \verb|eps| copy as well.
   213 
   214   \medskip The applet version of the browser is part of the standard
   215   WWW theory presentation, see the link ``theory dependencies'' within
   216   each session index.%
   217 \end{isamarkuptext}%
   218 \isamarkuptrue%
   219 %
   220 \isamarkupsubsection{Using the graph browser%
   221 }
   222 \isamarkuptrue%
   223 %
   224 \begin{isamarkuptext}%
   225 The browser's main window, which is shown in
   226   \figref{fig:browserwindow}, consists of two sub-windows.  In the
   227   left sub-window, the directory tree is displayed. The graph itself
   228   is displayed in the right sub-window.
   229 
   230   \begin{figure}[ht]
   231   \includegraphics[width=\textwidth]{browser_screenshot}
   232   \caption{\label{fig:browserwindow} Browser main window}
   233   \end{figure}%
   234 \end{isamarkuptext}%
   235 \isamarkuptrue%
   236 %
   237 \isamarkupsubsubsection{The directory tree window%
   238 }
   239 \isamarkuptrue%
   240 %
   241 \begin{isamarkuptext}%
   242 We describe the usage of the directory browser and the meaning of
   243   the different items in the browser window.
   244 
   245   \begin{itemize}
   246   
   247   \item A red arrow before a directory name indicates that the
   248   directory is currently ``folded'', i.e.~the nodes in this directory
   249   are collapsed to one single node. In the right sub-window, the names
   250   of nodes corresponding to folded directories are enclosed in square
   251   brackets and displayed in red color.
   252   
   253   \item A green downward arrow before a directory name indicates that
   254   the directory is currently ``unfolded''. It can be folded by
   255   clicking on the directory name.  Clicking on the name for a second
   256   time unfolds the directory again.  Alternatively, a directory can
   257   also be unfolded by clicking on the corresponding node in the right
   258   sub-window.
   259   
   260   \item Blue arrows stand before ordinary node names. When clicking on
   261   such a name (i.e.\ that of a theory), the graph display window
   262   focuses to the corresponding node. Double clicking invokes a text
   263   viewer window in which the contents of the theory file are
   264   displayed.
   265 
   266   \end{itemize}%
   267 \end{isamarkuptext}%
   268 \isamarkuptrue%
   269 %
   270 \isamarkupsubsubsection{The graph display window%
   271 }
   272 \isamarkuptrue%
   273 %
   274 \begin{isamarkuptext}%
   275 When pointing on an ordinary node, an upward and a downward arrow is
   276   shown.  Initially, both of these arrows are green. Clicking on the
   277   upward or downward arrow collapses all predecessor or successor
   278   nodes, respectively. The arrow's color then changes to red,
   279   indicating that the predecessor or successor nodes are currently
   280   collapsed. The node corresponding to the collapsed nodes has the
   281   name ``\verb|[....]|''. To uncollapse the nodes again, simply
   282   click on the red arrow or on the node with the name ``\verb|[....]|''. Similar to the directory browser, the contents of
   283   theory files can be displayed by double clicking on the
   284   corresponding node.%
   285 \end{isamarkuptext}%
   286 \isamarkuptrue%
   287 %
   288 \isamarkupsubsubsection{The ``File'' menu%
   289 }
   290 \isamarkuptrue%
   291 %
   292 \begin{isamarkuptext}%
   293 Due to Java Applet security restrictions this menu is only available
   294   in the full application version. The meaning of the menu items is as
   295   follows:
   296 
   297   \begin{description}
   298   
   299   \item[Open \dots] Open a new graph file.
   300   
   301   \item[Export to PostScript] Outputs the current graph in Postscript
   302   format, appropriately scaled to fit on one single sheet of A4 paper.
   303   The resulting file can be printed directly.
   304   
   305   \item[Export to EPS] Outputs the current graph in Encapsulated
   306   Postscript format. The resulting file can be included in other
   307   documents.
   308 
   309   \item[Quit] Quit the graph browser.
   310 
   311   \end{description}%
   312 \end{isamarkuptext}%
   313 \isamarkuptrue%
   314 %
   315 \isamarkupsubsection{Syntax of graph definition files%
   316 }
   317 \isamarkuptrue%
   318 %
   319 \begin{isamarkuptext}%
   320 A graph definition file has the following syntax:
   321 
   322   \begin{center}\small
   323   \begin{tabular}{rcl}
   324     \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}{\isacharplus}{\isachardoublequote}} \\
   325     \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}{\isacharasterisk}{\isachardoublequote}}
   326   \end{tabular}
   327   \end{center}
   328 
   329   The meaning of the items in a vertex description is as follows:
   330 
   331   \begin{description}
   332   
   333   \item[\isa{vertex{\isacharunderscore}name}] The name of the vertex.
   334   
   335   \item[\isa{vertex{\isacharunderscore}ID}] The vertex identifier. Note that there may
   336   be several vertices with equal names, whereas identifiers must be
   337   unique.
   338   
   339   \item[\isa{dir{\isacharunderscore}name}] The name of the ``directory'' the vertex
   340   should be placed in.  A ``\verb|+|'' sign after \isa{dir{\isacharunderscore}name} indicates that the nodes in the directory are initially
   341   visible. Directories are initially invisible by default.
   342   
   343   \item[\isa{path}] The path of the corresponding theory file. This
   344   is specified relatively to the path of the graph definition file.
   345   
   346   \item[List of successor/predecessor nodes] A ``\verb|<|''
   347   sign before the list means that successor nodes are listed, a
   348   ``\verb|>|'' sign means that predecessor nodes are listed. If
   349   neither ``\verb|<|'' nor ``\verb|>|'' is found, the
   350   browser assumes that successor nodes are listed.
   351 
   352   \end{description}%
   353 \end{isamarkuptext}%
   354 \isamarkuptrue%
   355 %
   356 \isamarkupsection{Creating Isabelle session directories
   357   \label{sec:tool-mkdir}%
   358 }
   359 \isamarkuptrue%
   360 %
   361 \begin{isamarkuptext}%
   362 The \indexdef{}{tool}{mkdir}\hypertarget{tool.mkdir}{\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}} utility prepares Isabelle session source
   363   directories, including a sensible default setup of \verb|IsaMakefile|, \verb|ROOT.ML|, and a \verb|document|
   364   directory with a minimal \verb|root.tex| that is sufficient to
   365   print all theories of the session (in the order of appearance); see
   366   \secref{sec:tool-document} for further information on Isabelle
   367   document preparation.  The usage of \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is:
   368 
   369 \begin{ttbox}
   370 Usage: mkdir [OPTIONS] [LOGIC] NAME
   371 
   372   Options are:
   373     -I FILE      alternative IsaMakefile output
   374     -P           include parent logic target
   375     -b           setup build mode (session outputs heap image)
   376     -q           quiet mode
   377 
   378   Prepare session directory, including IsaMakefile and document source,
   379   with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
   380 \end{ttbox}
   381 
   382   The \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool is conservative in the sense that any
   383   existing \verb|IsaMakefile| etc.\ is left unchanged.  Thus it
   384   is safe to invoke it multiple times, although later runs may not
   385   have the desired effect.
   386 
   387   Note that \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is unable to change \verb|IsaMakefile|
   388   incrementally --- manual changes are required for multiple
   389   sub-sessions.  On order to get an initial working session, the only
   390   editing needed is to add appropriate \verb|use_thy| calls to the
   391   generated \verb|ROOT.ML| file.%
   392 \end{isamarkuptext}%
   393 \isamarkuptrue%
   394 %
   395 \isamarkupsubsubsection{Options%
   396 }
   397 \isamarkuptrue%
   398 %
   399 \begin{isamarkuptext}%
   400 The \verb|-I| option specifies an alternative to \verb|IsaMakefile| for dependencies.  Note that ``\verb|-|'' refers
   401   to \emph{stdout}, i.e.\ ``\verb|-I-|'' provides an easy way
   402   to peek at \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}'s idea of \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} setup required for
   403   some particular of Isabelle session.
   404 
   405   \medskip The \verb|-P| option includes a target for the
   406   parent \verb|LOGIC| session in the generated \verb|IsaMakefile|.  The corresponding sources are assumed to be located
   407   within the Isabelle distribution.
   408 
   409   \medskip The \verb|-b| option sets up the current directory
   410   as the base for a new session that provides an actual logic image,
   411   as opposed to one that only runs several theories based on an
   412   existing image.  Note that in the latter case, everything except
   413   \verb|IsaMakefile| would be placed into a separate directory
   414   \verb|NAME|, rather than the current one.  See
   415   \secref{sec:tool-usedir} for further information on \emph{build
   416   mode} vs.\ \emph{example mode} of the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility.
   417 
   418   \medskip The \verb|-q| option enables quiet mode, suppressing
   419   further notes on how to proceed.%
   420 \end{isamarkuptext}%
   421 \isamarkuptrue%
   422 %
   423 \isamarkupsubsubsection{Examples%
   424 }
   425 \isamarkuptrue%
   426 %
   427 \begin{isamarkuptext}%
   428 The standard setup of a single ``example session'' based on the
   429   default logic, with proper document generation is generated like
   430   this:
   431 \begin{ttbox}
   432 isabelle mkdir Foo && isabelle make
   433 \end{ttbox}
   434 
   435   \noindent The theory sources should be put into the \verb|Foo|
   436   directory, and its \verb|ROOT.ML| should be edited to load all
   437   required theories.  Invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} again
   438   would run the whole session, generating browser information and the
   439   document automatically.  The \verb|IsaMakefile| is typically
   440   tuned manually later, e.g.\ adding source dependencies, or changing
   441   the options passed to \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}.
   442 
   443   \medskip Large projects may demand further sessions, potentially
   444   with separate logic images being created.  This usually requires
   445   manual editing of the generated \verb|IsaMakefile|, which is
   446   meant to cover all of the sub-session directories at the same time
   447   (this is the deeper reasong why \verb|IsaMakefile| is not made
   448   part of the initial session directory created by \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}).  See \hyperlink{file.~~/src/HOL/IsaMakefile}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}IsaMakefile}}}} for
   449   a full-blown example.%
   450 \end{isamarkuptext}%
   451 \isamarkuptrue%
   452 %
   453 \isamarkupsection{Running Isabelle sessions \label{sec:tool-usedir}%
   454 }
   455 \isamarkuptrue%
   456 %
   457 \begin{isamarkuptext}%
   458 The \indexdef{}{tool}{usedir}\hypertarget{tool.usedir}{\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}} utility builds object-logic images, or runs
   459   example sessions based on existing logics. Its usage is:
   460 \begin{ttbox}
   461 
   462 Usage: usedir [OPTIONS] LOGIC NAME
   463 
   464   Options are:
   465     -C BOOL      copy existing document directory to -D PATH (default true)
   466     -D PATH      dump generated document sources into PATH
   467     -M MAX       multithreading: maximum number of worker threads (default 1)
   468     -P PATH      set path for remote theory browsing information
   469     -T LEVEL     multithreading: trace level (default 0)
   470     -V VERSION   declare alternative document VERSION
   471     -b           build mode (output heap image, using current dir)
   472     -d FORMAT    build document as FORMAT (default false)
   473     -f NAME      use ML file NAME (default ROOT.ML)
   474     -g BOOL      generate session graph image for document (default false)
   475     -i BOOL      generate theory browser information (default false)
   476     -m MODE      add print mode for output
   477     -p LEVEL     set level of detail for proof objects (default 0)
   478     -q LEVEL     set level of parallel proof checking (default 1)
   479     -r           reset session path
   480     -s NAME      override session NAME
   481     -t BOOL      internal session timing (default false)
   482     -v BOOL      be verbose (default false)
   483 
   484   Build object-logic or run examples. Also creates browsing
   485   information (HTML etc.) according to settings.
   486 
   487   ISABELLE_USEDIR_OPTIONS=
   488 
   489   ML_PLATFORM=x86-linux
   490   ML_HOME=/usr/local/polyml-5.2.1/x86-linux
   491   ML_SYSTEM=polyml-5.2.1
   492   ML_OPTIONS=-H 500
   493 \end{ttbox}
   494 
   495   Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}}
   496   setting is implicitly prefixed to \emph{any} \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
   497   call. Since the \verb|IsaMakefile|s of all object-logics
   498   distributed with Isabelle just invoke \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} for the real
   499   work, one may control compilation options globally via above
   500   variable. In particular, generation of \rmindex{HTML} browsing
   501   information and document preparation is controlled here.%
   502 \end{isamarkuptext}%
   503 \isamarkuptrue%
   504 %
   505 \isamarkupsubsubsection{Options%
   506 }
   507 \isamarkuptrue%
   508 %
   509 \begin{isamarkuptext}%
   510 Basically, there are two different modes of operation: \emph{build
   511   mode} (enabled through the \verb|-b| option) and
   512   \emph{example mode} (default).
   513 
   514   Calling \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} with \verb|-b| runs \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} with input image \verb|LOGIC| and output to
   515   \verb|NAME|, as provided on the command line. This will be a
   516   batch session, running \verb|ROOT.ML| from the current
   517   directory and then quitting.  It is assumed that \verb|ROOT.ML|
   518   contains all ML commands required to build the logic.
   519 
   520   In example mode, \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} runs a read-only session of
   521   \verb|LOGIC| and automatically runs \verb|ROOT.ML| from
   522   within directory \verb|NAME|.  It assumes that this file
   523   contains appropriate ML commands to run the desired examples.
   524 
   525   \medskip The \verb|-i| option controls theory browser data
   526   generation. It may be explicitly turned on or off --- as usual, the
   527   last occurrence of \verb|-i| on the command line wins.
   528 
   529   The \verb|-P| option specifies a path (or actual URL) to be
   530   prefixed to any \emph{non-local} reference of existing theories.
   531   Thus user sessions may easily link to existing Isabelle libraries
   532   already present on the WWW.
   533 
   534   The \verb|-m| options specifies additional print modes to be
   535   activated temporarily while the session is processed.
   536 
   537   \medskip The \verb|-d| option controls document preparation.
   538   Valid arguments are \verb|false| (do not prepare any document;
   539   this is default), or any of \verb|dvi|, \verb|dvi.gz|,
   540   \verb|ps|, \verb|ps.gz|, \verb|pdf|.  The logic
   541   session has to provide a properly setup \verb|document|
   542   directory.  See \secref{sec:tool-document} and
   543   \secref{sec:tool-latex} for more details.
   544 
   545   \medskip The \verb|-V| option declares alternative document
   546   versions, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool).  The
   547   standard document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end
   548   commands, proof body texts, and ML code will be presented
   549   faithfully.  An alternative version ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
   550   original text by a short place-holder.  The form ``\isa{name}\verb|=-|,'' means to remove document \isa{name} from
   551   the list of versions to be processed.  Any number of \verb|-V| options may be given; later declarations have precedence over
   552   earlier ones.
   553 
   554   \medskip The \verb|-g| option produces images of the theory
   555   dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
   556   generated document, both as \verb|session_graph.eps| and
   557   \verb|session_graph.pdf| at the same time.  To include this in
   558   the final {\LaTeX} document one could say \verb|\includegraphics{session_graph}| in \verb|document/root.tex| (omitting the file-name extension enables
   559   {\LaTeX} to select to correct version, either for the DVI or PDF
   560   output path).
   561 
   562   \medskip The \verb|-D| option causes the generated document
   563   sources to be dumped at location \verb|PATH|; this path is
   564   relative to the session's main directory.  If the \verb|-C|
   565   option is true, this will include a copy of an existing \verb|document| directory as provided by the user.  For example,
   566   \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}~\verb|-D generated HOL|\isasep\isanewline%
   567 \verb|  Foo| produces a complete set of document sources at \verb|Foo/generated|.  Subsequent invocation of \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|Foo/generated| (see also
   568   \secref{sec:tool-document}) will process the final result
   569   independently of an Isabelle job.  This decoupled mode of operation
   570   facilitates debugging of serious {\LaTeX} errors, for example.
   571 
   572   \medskip The \verb|-p| option determines the level of detail
   573   for internal proof objects, see also the \emph{Isabelle Reference
   574   Manual}~\cite{isabelle-ref}.
   575 
   576   \medskip The \verb|-q| option specifies the level of parallel
   577   proof checking: \verb|0| no proofs, \verb|1| toplevel
   578   proofs (default), \verb|2| toplevel and nested Isar proofs.
   579   The resulting speedup may vary, depending on the number of worker
   580   threads, granularity of proofs, and whether proof terms are enabled.
   581 
   582   \medskip The \verb|-t| option produces a more detailed
   583   internal timing report of the session.
   584 
   585   \medskip The \verb|-v| option causes additional information
   586   to be printed while running the session, notably the location of
   587   prepared documents.
   588 
   589   \medskip The \verb|-M| option specifies the maximum number of
   590   parallel threads used for processing independent tasks when checking
   591   theory sources (multithreading only works on suitable ML platforms).
   592   The special value of \verb|0| or \verb|max| refers to the
   593   number of actual CPU cores of the underlying machine, which is a
   594   good starting point for optimal performance tuning.  The \verb|-T| option determines the level of detail in tracing output
   595   concerning the internal locking and scheduling in multithreaded
   596   operation.  This may be helpful in isolating performance
   597   bottle-necks, e.g.\ due to excessive wait states when locking
   598   critical code sections.
   599 
   600   \medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
   601   identifier}. These accumulate, documenting the way sessions depend
   602   on others. For example, consider \verb|Pure/FOL/ex|, which
   603   refers to the examples of FOL, which in turn is built upon Pure.
   604 
   605   The current session's identifier is by default just the base name of
   606   the \verb|LOGIC| argument (in build mode), or of the \verb|NAME| argument (in example mode). This may be overridden explicitly
   607   via the \verb|-s| option.%
   608 \end{isamarkuptext}%
   609 \isamarkuptrue%
   610 %
   611 \isamarkupsubsubsection{Examples%
   612 }
   613 \isamarkuptrue%
   614 %
   615 \begin{isamarkuptext}%
   616 Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
   617   object-logics as a model for your own developments.  For example,
   618   see \hyperlink{file.~~/src/FOL/IsaMakefile}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}IsaMakefile}}}}.  The Isabelle \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool creates \verb|IsaMakefile|s with proper invocation
   619   of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} as well.%
   620 \end{isamarkuptext}%
   621 \isamarkuptrue%
   622 %
   623 \isamarkupsection{Preparing Isabelle session documents
   624   \label{sec:tool-document}%
   625 }
   626 \isamarkuptrue%
   627 %
   628 \begin{isamarkuptext}%
   629 The \indexdef{}{tool}{document}\hypertarget{tool.document}{\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}} utility prepares logic session documents,
   630   processing the sources both as provided by the user and generated by
   631   Isabelle.  Its usage is:
   632 \begin{ttbox}
   633 Usage: document [OPTIONS] [DIR]
   634 
   635   Options are:
   636     -c           cleanup -- be aggressive in removing old stuff
   637     -n NAME      specify document name (default 'document')
   638     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
   639                  ps.gz, pdf
   640     -t TAGS      specify tagged region markup
   641 
   642   Prepare the theory session document in DIR (default 'document')
   643   producing the specified output format.
   644 \end{ttbox}
   645   This tool is usually run automatically as part of the corresponding
   646   Isabelle batch process, provided document preparation has been
   647   enabled (cf.\ the \verb|-d| option of the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
   648   tool).  It may be manually invoked on the generated browser
   649   information document output as well, e.g.\ in case of errors
   650   encountered in the batch run.
   651 
   652   \medskip The \verb|-c| option tells the \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool
   653   to dispose the document sources after successful operation.  This is
   654   the right thing to do for sources generated by an Isabelle process,
   655   but take care of your files in manual document preparation!
   656 
   657   \medskip The \verb|-n| and \verb|-o| option specify
   658   the final output file name and format, the default is ``\verb|document.dvi|''.  Note that the result will appear in the parent of
   659   the target \verb|DIR|.
   660 
   661   \medskip The \verb|-t| option tells {\LaTeX} how to interpret
   662   tagged Isabelle command regions.  Tags are specified as a comma
   663   separated list of modifier/name pairs: ``\verb|+|\isa{foo}'' (or just ``\isa{foo}'') means to keep, ``\verb|-|\isa{foo}'' to drop, and ``\verb|/|\isa{foo}'' to
   664   fold text tagged as \isa{foo}.  The builtin default is equivalent
   665   to the tag specification ``\verb|+theory,+proof,+ML,+visible,-invisible|''; see also the {\LaTeX}
   666   macros \verb|\isakeeptag|, \verb|\isadroptag|, and
   667   \verb|\isafoldtag|, in \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}}.
   668 
   669   \medskip Document preparation requires a properly setup ``\verb|document|'' directory within the logic session sources.  This
   670   directory is supposed to contain all the files needed to produce the
   671   final document --- apart from the actual theories which are
   672   generated by Isabelle.
   673 
   674   \medskip For most practical purposes, the \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool is
   675   smart enough to create any of the specified output formats, taking
   676   \verb|root.tex| supplied by the user as a starting point.  This
   677   even includes multiple runs of {\LaTeX} to accommodate references
   678   and bibliographies (the latter assumes \verb|root.bib| within
   679   the same directory).
   680 
   681   In more complex situations, a separate \verb|IsaMakefile| for
   682   the document sources may be given instead.  This should provide
   683   targets for any admissible document format; these have to produce
   684   corresponding output files named after \verb|root| as well,
   685   e.g.\ \verb|root.dvi| for target format \verb|dvi|.
   686 
   687   \medskip When running the session, Isabelle copies the original
   688   \verb|document| directory into its proper place within
   689   \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} according to the session path.
   690   Then, for any processed theory \isa{A} some {\LaTeX} source is
   691   generated and put there as \isa{A}\verb|.tex|.
   692   Furthermore, a list of all generated theory files is put into
   693   \verb|session.tex|.  Typically, the root {\LaTeX} file provided
   694   by the user would include \verb|session.tex| to get a document
   695   containing all the theories.
   696 
   697   The {\LaTeX} versions of the theories require some macros defined in
   698   \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}}.  Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
   699   the underlying Isabelle \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} tool already includes an
   700   appropriate path specification for {\TeX} inputs.
   701 
   702   If the text contains any references to Isabelle symbols (such as
   703   \verb|\|\verb|<forall>|) then \verb|isabellesym.sty| should be included as well.  This package
   704   contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, see \cite{isabelle-implementation} for a
   705   complete list of predefined Isabelle symbols.  Users may invent
   706   further symbols as well, just by providing {\LaTeX} macros in a
   707   similar fashion as in \hyperlink{file.~~/lib/texinputs/isabellesym.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabellesym{\isachardot}sty}}}} of
   708   the distribution.
   709 
   710   For proper setup of DVI and PDF documents (with hyperlinks and
   711   bookmarks), we recommend to include \hyperlink{file.~~/lib/texinputs/pdfsetup.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}pdfsetup{\isachardot}sty}}}} as well.
   712 
   713   \medskip As a final step of document preparation within Isabelle,
   714   \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the
   715   resulting \verb|document| directory.  Thus the actual output
   716   document is built and installed in its proper place (as linked by
   717   the session's \verb|index.html| if option \verb|-i| of
   718   \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} has been enabled, cf.\ \secref{sec:info}).  The
   719   generated sources are deleted after successful run of {\LaTeX} and
   720   friends.  Note that a separate copy of the sources may be retained
   721   by passing an option \verb|-D| to the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility
   722   when running the session.%
   723 \end{isamarkuptext}%
   724 \isamarkuptrue%
   725 %
   726 \isamarkupsection{Running {\LaTeX} within the Isabelle environment
   727   \label{sec:tool-latex}%
   728 }
   729 \isamarkuptrue%
   730 %
   731 \begin{isamarkuptext}%
   732 The \indexdef{}{tool}{latex}\hypertarget{tool.latex}{\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}}} utility provides the basic interface for
   733   Isabelle document preparation.  Its usage is:
   734 \begin{ttbox}
   735 Usage: latex [OPTIONS] [FILE]
   736 
   737   Options are:
   738     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
   739                  ps.gz, pdf, bbl, idx, sty, syms
   740 
   741   Run LaTeX (and related tools) on FILE (default root.tex),
   742   producing the specified output format.
   743 \end{ttbox}
   744 
   745   Appropriate {\LaTeX}-related programs are run on the input file,
   746   according to the given output format: \hyperlink{executable.latex}{\mbox{\isa{\isatt{latex}}}},
   747   \hyperlink{executable.pdflatex}{\mbox{\isa{\isatt{pdflatex}}}}, \hyperlink{executable.dvips}{\mbox{\isa{\isatt{dvips}}}}, \hyperlink{executable.bibtex}{\mbox{\isa{\isatt{bibtex}}}}
   748   (for \verb|bbl|), and \hyperlink{executable.makeindex}{\mbox{\isa{\isatt{makeindex}}}} (for \verb|idx|).  The actual commands are determined from the settings
   749   environment (\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LATEX}}}} etc.).
   750 
   751   The \verb|sty| output format causes the Isabelle style files to
   752   be updated from the distribution.  This is useful in special
   753   situations where the document sources are to be processed another
   754   time by separate tools (cf.\ option \verb|-D| of the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility).
   755 
   756   The \verb|syms| output is for internal use; it generates lists
   757   of symbols that are available without loading additional {\LaTeX}
   758   packages.%
   759 \end{isamarkuptext}%
   760 \isamarkuptrue%
   761 %
   762 \isamarkupsubsubsection{Examples%
   763 }
   764 \isamarkuptrue%
   765 %
   766 \begin{isamarkuptext}%
   767 Invoking \verb|isabelle| \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} by hand may be
   768   occasionally useful when debugging failed attempts of the automatic
   769   document preparation stage of batch-mode Isabelle.  The abortive
   770   process leaves the sources at a certain place within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}, see the runtime error message for details.
   771   This enables users to inspect {\LaTeX} runs in further detail, e.g.\
   772   like this:
   773 \begin{ttbox}
   774   cd ~/.isabelle/browser_info/HOL/Test/document
   775   isabelle latex -o pdf
   776 \end{ttbox}%
   777 \end{isamarkuptext}%
   778 \isamarkuptrue%
   779 %
   780 \isadelimtheory
   781 %
   782 \endisadelimtheory
   783 %
   784 \isatagtheory
   785 \isacommand{end}\isamarkupfalse%
   786 %
   787 \endisatagtheory
   788 {\isafoldtheory}%
   789 %
   790 \isadelimtheory
   791 %
   792 \endisadelimtheory
   793 \end{isabellebody}%
   794 %%% Local Variables:
   795 %%% mode: latex
   796 %%% TeX-master: "root"
   797 %%% End: