doc-src/System/present.tex
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;
     1 
     2 %% $Id$
     3 
     4 \chapter{Presenting theories}\label{ch:present}
     5 
     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).
    12 
    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}.
    22 
    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}
    40 
    41 
    42 \section{Generating theory browser information} \label{sec:info}
    43 \index{theory browsing information|bold}
    44 
    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.
    52 
    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.
    59 
    60 \medskip
    61 
    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}
    68 ISABELLE_USEDIR_OPTIONS="-i true"
    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.
    76 
    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.
    87 
    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{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
    97     \url{http://isabelle.in.tum.de/library/} \\
    98   \end{tabular}
    99 \end{center}
   100 
   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 http://isabelle.in.tum.de/library/ HOL Foo
   116 \end{ttbox}
   117 
   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.
   127 
   128 
   129 \section{Browsing theory graphs} \label{sec:browse}
   130 \index{theory graph browser|bold} 
   131 
   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.
   140 
   141 
   142 \subsection{Invoking the graph browser}
   143 
   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]
   148 
   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}.
   155 
   156 \medskip The \texttt{-c} option causes the input file to be removed after use.
   157 
   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.
   161 
   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.
   164 
   165 
   166 \subsection{Using the graph browser}
   167 
   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}
   176 
   177 
   178 \subsubsection*{The directory tree window}
   179 
   180 We describe the usage of the directory browser and the meaning of the
   181 different items in the browser window.
   182 \begin{itemize}
   183   
   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.
   189   
   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.
   196   
   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.
   201 
   202 \end{itemize}
   203 
   204 
   205 \subsubsection*{The graph display window}
   206 
   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.
   217 
   218 
   219 \subsubsection*{The ``File'' menu}
   220 
   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}
   225   
   226 \item[Open \dots] Open a new graph file.
   227   
   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.
   231   
   232 \item[Export to EPS] Outputs the current graph in Encapsulated Postscript
   233   format. The resulting file can be included in other documents.
   234 
   235 \item[Quit] Quit the graph browser.
   236 
   237 \end{description}
   238 
   239 
   240 \subsection*{*Syntax of graph definition files}
   241 
   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*}
   248 
   249 The meaning of the items in a vertex description is as follows:
   250 \begin{description}
   251   
   252 \item[vertexname] The name of the vertex.
   253   
   254 \item[vertexID] The vertex identifier. Note that there may be two
   255   vertices with equal names, whereas identifiers must be unique.
   256   
   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.
   261   
   262 \item[path] The path of the corresponding theory file. This is
   263   specified relatively to the path of the graph definition file.
   264   
   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.
   270 
   271 \end{description}
   272 
   273 
   274 \section{Creating Isabelle session directories --- \texttt{isatool mkdir}}
   275 \label{sec:tool-mkdir}
   276 
   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
   285 
   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
   291 
   292   Prepare session directory, including IsaMakefile and document source,
   293   with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
   294 \end{ttbox}
   295 
   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.
   299 
   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.
   304 
   305 
   306 \subsection*{Options}
   307 
   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.
   312 
   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.
   317 
   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.
   325 
   326 \medskip The \texttt{-q} enables quiet mode, suppressing further notes on how
   327 to proceed.
   328 
   329 
   330 \subsection*{Examples}
   331 
   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}.
   343 
   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.
   351 
   352 
   353 \section{Running Isabelle sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir}
   354 
   355 The \tooldx{usedir} utility builds object-logic images, or runs example
   356 sessions based on existing logics. Its usage is:
   357 \begin{ttbox}
   358 
   359 Usage: usedir [OPTIONS] LOGIC NAME
   360 
   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)
   379 
   380   Build object-logic or run examples. Also creates browsing
   381   information (HTML etc.) according to settings.
   382 
   383   ISABELLE_USEDIR_OPTIONS=
   384   HOL_USEDIR_OPTIONS=
   385 \end{ttbox}
   386 
   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.
   393 
   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.
   397 
   398 
   399 \subsection*{Options}
   400 
   401 Basically, there are two different modes of operation: \emph{build mode}
   402 (enabled through the \texttt{-b} option) and \emph{example mode} (default).
   403 
   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.
   409 
   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.
   414 
   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.
   418 
   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.
   422 
   423 The \texttt{-m} options specifies additional print modes to be activated
   424 temporarily while the session is processed.
   425 
   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.
   432 
   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.
   443 
   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).
   451 
   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.
   462 
   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}.
   466 
   467 \medskip The \texttt{-v} option causes additional information to be printed
   468 while running the session, notably the location of prepared documents.
   469 
   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.
   480 
   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.
   485 
   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.
   489 
   490 
   491 \subsection*{Examples}
   492 
   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.
   498 
   499 
   500 \section{Preparing Isabelle session documents --- \texttt{isatool document}}
   501 \label{sec:tool-document}
   502 
   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]
   507 
   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
   514 
   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.
   523 
   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!
   528 
   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}.
   532 
   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}.
   541 
   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.
   546 
   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).
   552 
   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}.
   557 
   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.
   566 
   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.
   572 
   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.
   581 
   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.
   585 
   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}).
   595 
   596 
   597 \section{Running {\LaTeX} within the Isabelle environment --- \texttt{isatool latex}}
   598 \label{sec:tool-latex}
   599 
   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]
   604 
   605   Options are:
   606     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
   607                  ps.gz, pdf, bbl, idx, sty, syms
   608 
   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}).
   618 
   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}).
   624 
   625 The \texttt{syms} output is for internal use; it generates lists of symbols
   626 that are available without loading additional {\LaTeX} packages.
   627 
   628 
   629 \subsubsection*{Examples}
   630 
   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:
   637 
   638 \begin{ttbox}
   639   cd ~/isabelle/browser_info/HOL/Test/document
   640   isatool latex -o pdf
   641 \end{ttbox}
   642 
   643 
   644 %%% Local Variables: 
   645 %%% mode: latex
   646 %%% TeX-master: "system"
   647 %%% End: