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