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