doc-src/System/Thy/Presentation.thy
author wenzelm
Mon Sep 15 20:51:40 2008 +0200 (2008-09-15 ago)
changeset 28225 5d1fc22bccdf
parent 28221 ca9fdab0f971
child 28238 398bf960d3d4
permissions -rw-r--r--
tuned;
     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 usedir"}; \\
    42 
    43       @{verbatim "isatool document"} & run by the Isabelle process if
    44       document preparation is enabled; \\
    45 
    46       @{verbatim "isatool latex"} & universal {\LaTeX} tool wrapper
    47       invoked multiple times by @{verbatim "isatool document"}; also
    48       useful for manual experiments; \\
    49 
    50   \end{tabular}
    51   \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
    52   \end{center}
    53   \end{figure}
    54 *}
    55 
    56 
    57 section {* Generating theory browser information \label{sec:info} *}
    58 
    59 text {*
    60   \index{theory browsing information|bold}
    61 
    62   As a side-effect of running a logic sessions, Isabelle is able to
    63   generate theory browsing information, including HTML documents that
    64   show a theory's definition, the theorems proved in its ML file and
    65   the relationship with its ancestors and descendants.  Besides the
    66   HTML file that is generated for every theory, Isabelle stores links
    67   to all theories in an index file. These indexes are linked with
    68   other indexes to represent the overall tree structure of logic
    69   sessions.
    70 
    71   Isabelle also generates graph files that represent the theory
    72   hierarchy of a logic.  There is a graph browser Java applet embedded
    73   in the generated HTML pages, and also a stand-alone application that
    74   allows browsing theory graphs without having to start a WWW client
    75   first.  The latter version also includes features such as generating
    76   Postscript files, which are not available in the applet version.
    77   See \secref{sec:browse} for further information.
    78 
    79   \medskip
    80 
    81   The easiest way to let Isabelle generate theory browsing information
    82   for existing sessions is to append ``@{verbatim "-i true"}'' to the
    83   @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim
    84   "isatool make"} (or @{verbatim "./build"} in the distribution).  For
    85   example, add something like this to your Isabelle settings file
    86 
    87 \begin{ttbox}
    88 ISABELLE_USEDIR_OPTIONS="-i true"
    89 \end{ttbox}
    90 
    91   and then change into the @{verbatim "src/FOL"} directory of the
    92   Isabelle distribution and run @{verbatim "isatool make"}, or even
    93   @{verbatim "isatool make all"}.  The presentation output will appear
    94   in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
    95   @{verbatim "~/isabelle/browser_info/FOL"}.  Note that option
    96   @{verbatim "-v true"} will make the internal runs of @{tool usedir}
    97   more explicit about such details.
    98 
    99   Many standard Isabelle sessions (such as @{verbatim "HOL/ex"}) also
   100   provide actual printable documents.  These are prepared
   101   automatically as well if enabled like this, using the @{verbatim
   102   "-d"} option
   103 \begin{ttbox}
   104 ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
   105 \end{ttbox}
   106   Enabling options @{verbatim "-i"} and @{verbatim "-d"}
   107   simultaneously as shown above causes an appropriate ``document''
   108   link to be included in the HTML index.  Documents (or raw document
   109   sources) may be generated independently of browser information as
   110   well, see \secref{sec:tool-document} for further details.
   111 
   112   \bigskip The theory browsing information is stored in a
   113   sub-directory directory determined by the @{setting_ref
   114   ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the
   115   session identifier (according to the tree structure of sub-sessions
   116   by default).  A complete WWW view of all standard object-logics and
   117   examples of the Isabelle distribution is available at the usual
   118   Isabelle sites:
   119   \begin{center}\small
   120   \begin{tabular}{l}
   121     \url{http://isabelle.in.tum.de/dist/library/} \\
   122     \url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/} \\
   123     \url{http://mirror.cse.unsw.edu.au/pub/isabelle/dist/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{center}\small
   300   \begin{tabular}{rcl}
   301     @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\
   302     @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"}
   303   \end{tabular}
   304   \end{center}
   305 
   306   The meaning of the items in a vertex description is as follows:
   307 
   308   \begin{description}
   309   
   310   \item[@{text vertex_name}] The name of the vertex.
   311   
   312   \item[@{text vertex_ID}] The vertex identifier. Note that there may
   313   be several vertices with equal names, whereas identifiers must be
   314   unique.
   315   
   316   \item[@{text dir_name}] The name of the ``directory'' the vertex
   317   should be placed in.  A ``@{verbatim "+"}'' sign after @{text
   318   dir_name} indicates that the nodes in the directory are initially
   319   visible. Directories are initially invisible by default.
   320   
   321   \item[@{text path}] The path of the corresponding theory file. This
   322   is specified relatively to the path of the graph definition file.
   323   
   324   \item[List of successor/predecessor nodes] A ``@{verbatim "<"}''
   325   sign before the list means that successor nodes are listed, a
   326   ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
   327   neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
   328   browser assumes that successor nodes are listed.
   329 
   330   \end{description}
   331 *}
   332 
   333 
   334 section {* Creating Isabelle session directories
   335   \label{sec:tool-mkdir} *}
   336 
   337 text {*
   338   The @{tool_def mkdir} utility prepares Isabelle session source
   339   directories, including a sensible default setup of @{verbatim
   340   IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document}
   341   directory with a minimal @{verbatim root.tex} that is sufficient to
   342   print all theories of the session (in the order of appearance); see
   343   \secref{sec:tool-document} for further information on Isabelle
   344   document preparation.  The usage of @{verbatim "isatool 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 isatool mkdir Foo && isatool 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 "isatool make"} again would
   413   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
   424   @{verbatim "isatool mkdir"}).  See @{verbatim "src/HOL/IsaMakefile"}
   425   of the Isabelle distribution for 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     -c BOOL      tell ML system to compress output image (default true)
   447     -d FORMAT    build document as FORMAT (default false)
   448     -f NAME      use ML file NAME (default ROOT.ML)
   449     -g BOOL      generate session graph image for document (default false)
   450     -i BOOL      generate theory browser information (default false)
   451     -m MODE      add print mode for output
   452     -p LEVEL     set level of detail for proof objects
   453     -r           reset session path
   454     -s NAME      override session NAME
   455     -v BOOL      be verbose (default false)
   456 
   457   Build object-logic or run examples. Also creates browsing
   458   information (HTML etc.) according to settings.
   459 
   460   ISABELLE_USEDIR_OPTIONS=
   461   HOL_USEDIR_OPTIONS=
   462 \end{ttbox}
   463 
   464   Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
   465   setting is implicitly prefixed to \emph{any} @{tool usedir}
   466   call. Since the @{verbatim IsaMakefile}s of all object-logics
   467   distributed with Isabelle just invoke \texttt{usedir} for the real
   468   work, one may control compilation options globally via above
   469   variable. In particular, generation of \rmindex{HTML} browsing
   470   information and document preparation is controlled here.
   471 
   472   The @{setting_ref HOL_USEDIR_OPTIONS} setting is specific to the
   473   plain and main Isabelle/HOL images; its value is appended to
   474   @{setting ISABELLE_USEDIR_OPTIONS} for these particular sessions
   475   only.
   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, @{verbatim 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 "isatool usedir -D generated HOL Foo"} produces a
   548   complete set of document sources at @{verbatim "Foo/generated"}.
   549   Subsequent invocation of @{verbatim "isatool document
   550   Foo/generated"} (see also \secref{sec:tool-document}) will process
   551   the final result independently of an Isabelle job.  This decoupled
   552   mode of operation facilitates debugging of serious {\LaTeX} errors,
   553   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 "-v"} option causes additional information
   560   to be printed while running the session, notably the location of
   561   prepared documents.
   562 
   563   \medskip The @{verbatim "-M"} option specifies the maximum number of
   564   parallel threads used for processing independent tasks when checking
   565   theory sources (multithreading only works on suitable ML platforms).
   566   The special value of ``@{verbatim 0}'' or ``@{verbatim max}'' refers
   567   to the number of actual CPU cores of the underlying machine, which
   568   is a good starting point for optimal performance tuning.  The
   569   @{verbatim "-T"} option determines the level of detail in tracing
   570   output concerning the internal locking and scheduling in
   571   multithreaded operation.  This may be helpful in isolating
   572   performance bottle-necks, e.g.\ due to excessive wait states when
   573   locking critical code sections.
   574 
   575   \medskip Any @{tool usedir} session is named by some \emph{session
   576   identifier}. These accumulate, documenting the way sessions depend
   577   on others. For example, consider @{verbatim "Pure/FOL/ex"}, which
   578   refers to the examples of FOL, which in turn is built upon Pure.
   579 
   580   The current session's identifier is by default just the base name of
   581   the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim
   582   NAME} argument (in example mode). This may be overridden explicitly
   583   via the @{verbatim "-s"} option.
   584 *}
   585 
   586 
   587 subsubsection {* Examples *}
   588 
   589 text {*
   590   Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's
   591   object-logics as a model for your own developments.  For example,
   592   see @{verbatim "src/FOL/IsaMakefile"}.  The Isabelle @{tool_ref
   593   mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation
   594   of @{tool usedir} as well.
   595 *}
   596 
   597 
   598 section {* Preparing Isabelle session documents
   599   \label{sec:tool-document} *}
   600 
   601 text {*
   602   The @{tool_def document} utility prepares logic session documents,
   603   processing the sources both as provided by the user and generated by
   604   Isabelle.  Its usage is:
   605 \begin{ttbox}
   606 Usage: document [OPTIONS] [DIR]
   607 
   608   Options are:
   609     -c           cleanup -- be aggressive in removing old stuff
   610     -n NAME      specify document name (default 'document')
   611     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
   612                  ps.gz, pdf
   613     -t TAGS      specify tagged region markup
   614 
   615   Prepare the theory session document in DIR (default 'document')
   616   producing the specified output format.
   617 \end{ttbox}
   618   This tool is usually run automatically as part of the corresponding
   619   Isabelle batch process, provided document preparation has been
   620   enabled (cf.\ the @{verbatim "-d"} option of the @{tool_ref usedir}
   621   tool).  It may be manually invoked on the generated browser
   622   information document output as well, e.g.\ in case of errors
   623   encountered in the batch run.
   624 
   625   \medskip The @{verbatim "-c"} option tells the @{tool document} tool
   626   to dispose the document sources after successful operation.  This is
   627   the right thing to do for sources generated by an Isabelle process,
   628   but take care of your files in manual document preparation!
   629 
   630   \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify
   631   the final output file name and format, the default is ``@{verbatim
   632   document.dvi}''.  Note that the result will appear in the parent of
   633   the target @{verbatim DIR}.
   634 
   635   \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret
   636   tagged Isabelle command regions.  Tags are specified as a comma
   637   separated list of modifier/name pairs: ``@{verbatim "+"}@{text
   638   foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim
   639   "-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to
   640   fold text tagged as @{text foo}.  The builtin default is equivalent
   641   to the tag specification ``@{verbatim
   642   "/theory,/proof,/ML,+visible,-invisible"}''; see also the {\LaTeX}
   643   macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
   644   @{verbatim "\\isafoldtag"}, in @{verbatim isabelle.sty}.
   645 
   646   \medskip Document preparation requires a properly setup ``@{verbatim
   647   document}'' directory within the logic session sources.  This
   648   directory is supposed to contain all the files needed to produce the
   649   final document --- apart from the actual theories which are
   650   generated by Isabelle.
   651 
   652   \medskip For most practical purposes, the @{tool document} tool is
   653   smart enough to create any of the specified output formats, taking
   654   @{verbatim root.tex} supplied by the user as a starting point.  This
   655   even includes multiple runs of {\LaTeX} to accommodate references
   656   and bibliographies (the latter assumes @{verbatim root.bib} within
   657   the same directory).
   658 
   659   In more complex situations, a separate @{verbatim IsaMakefile} for
   660   the document sources may be given instead.  This should provide
   661   targets for any admissible document format; these have to produce
   662   corresponding output files named after @{verbatim root} as well,
   663   e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}.
   664 
   665   \medskip When running the session, Isabelle copies the original
   666   @{verbatim document} directory into its proper place within
   667   @{verbatim ISABELLE_BROWSER_INFO} according to the session path.
   668   Then, for any processed theory @{text A} some {\LaTeX} source is
   669   generated and put there as @{text A}@{verbatim ".tex"}.
   670   Furthermore, a list of all generated theory files is put into
   671   @{verbatim session.tex}.  Typically, the root {\LaTeX} file provided
   672   by the user would include @{verbatim session.tex} to get a document
   673   containing all the theories.
   674 
   675   The {\LaTeX} versions of the theories require some macros defined in
   676   @{verbatim isabelle.sty} as distributed with Isabelle.  Doing
   677   @{verbatim "\\usepackage{isabelle}"} in @{verbatim root.tex} should
   678   be fine; the underlying Isabelle @{tool latex} tool already includes
   679   an appropriate path specification for {\TeX} inputs.
   680 
   681   If the text contains any references to Isabelle symbols (such as
   682   @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim
   683   isabellesym.sty} should be included as well.  This package contains
   684   a standard set of {\LaTeX} macro definitions @{verbatim
   685   "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
   686   "<"}@{text foo}@{verbatim ">"}, (see \appref{app:symbols} for a
   687   complete list of predefined Isabelle symbols).  Users may invent
   688   further symbols as well, just by providing {\LaTeX} macros in a
   689   similar fashion as in @{verbatim isabellesym.sty} of the
   690   distribution.
   691 
   692   For proper setup of DVI and PDF documents (with hyperlinks and
   693   bookmarks), we recommend to include @{verbatim pdfsetup.sty} as
   694   well.
   695 
   696   \medskip As a final step of document preparation within Isabelle,
   697   @{verbatim "isatool document -c"} is run on the resulting @{verbatim
   698   document} directory.  Thus the actual output document is built and
   699   installed in its proper place (as linked by the session's @{verbatim
   700   index.html} if option @{verbatim "-i"} of @{tool_ref usedir} has
   701   been enabled, cf.\ \secref{sec:info}).  The generated sources are
   702   deleted after successful run of {\LaTeX} and friends.  Note that a
   703   separate copy of the sources may be retained by passing an option
   704   @{verbatim "-D"} to the @{tool usedir} utility when running the
   705   session.
   706 *}
   707 
   708 
   709 section {* Running {\LaTeX} within the Isabelle environment
   710   \label{sec:tool-latex} *}
   711 
   712 text {*
   713   The @{tool_def latex} utility provides the basic interface for
   714   Isabelle document preparation.  Its usage is:
   715 \begin{ttbox}
   716 Usage: latex [OPTIONS] [FILE]
   717 
   718   Options are:
   719     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
   720                  ps.gz, pdf, bbl, idx, sty, syms
   721 
   722   Run LaTeX (and related tools) on FILE (default root.tex),
   723   producing the specified output format.
   724 \end{ttbox}
   725 
   726   Appropriate {\LaTeX}-related programs are run on the input file,
   727   according to the given output format: @{executable latex},
   728   @{executable pdflatex}, @{executable dvips}, @{executable bibtex}
   729   (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim
   730   idx}).  The actual commands are determined from the settings
   731   environment (@{setting ISABELLE_LATEX} etc.).
   732 
   733   The @{verbatim sty} output format causes the Isabelle style files to
   734   be updated from the distribution.  This is useful in special
   735   situations where the document sources are to be processed another
   736   time by separate tools (cf.\ option @{verbatim "-D"} of the @{tool
   737   usedir} utility).
   738 
   739   The @{verbatim syms} output is for internal use; it generates lists
   740   of symbols that are available without loading additional {\LaTeX}
   741   packages.
   742 *}
   743 
   744 
   745 subsubsection {* Examples *}
   746 
   747 text {*
   748   Invoking @{verbatim "isatool latex"} by hand may be occasionally
   749   useful when debugging failed attempts of the automatic document
   750   preparation stage of batch-mode Isabelle.  The abortive process
   751   leaves the sources at a certain place within @{setting
   752   ISABELLE_BROWSER_INFO}, see the runtime error message for details.
   753   This enables users to inspect {\LaTeX} runs in further detail, e.g.\
   754   like this:
   755 \begin{ttbox}
   756   cd ~/isabelle/browser_info/HOL/Test/document
   757   isatool latex -o pdf
   758 \end{ttbox}
   759 *}
   760 
   761 end