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