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