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