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: