parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
3 \def\isabellecontext{Presentation}%
12 \isacommand{theory}\isamarkupfalse%
13 \ Presentation\isanewline
14 \isakeyword{imports}\ Pure\isanewline
23 \isamarkupchapter{Presenting theories \label{ch:present}%
27 \begin{isamarkuptext}%
28 Isabelle provides several ways to present the outcome of formal
29 developments, including WWW-based browsable libraries or actual
30 printable documents. Presentation is centered around the concept of
31 \emph{logic sessions}. The global session structure is that of a
32 tree, with Isabelle Pure at its root, further object-logics derived
33 (e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions
34 in leaf positions (usually without a separate image).
36 The Isabelle tools \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} and \indexref{}{tool}{make}\hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} provide
37 the primary means for managing Isabelle sessions, including proper
38 setup for presentation. Here the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} tool takes care
39 to let \indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} process run any
40 additional stages required for document preparation, notably the
41 tools \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} and \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}}. The complete tool
42 chain for managing batch-mode Isabelle sessions is illustrated in
43 \figref{fig:session-tools}.
47 \begin{tabular}{lp{0.6\textwidth}}
49 \verb|isabelle| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} & invoked once by the user
50 to create the initial source setup (common \verb|IsaMakefile| plus a single session directory); \\
52 \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} & invoked repeatedly by the
53 user to keep session output up-to-date (HTML, documents etc.); \\
55 \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} & part of the standard
56 \verb|IsaMakefile| entry of a session; \\
58 \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} & run through \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}; \\
60 \verb|isabelle| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} & run by the Isabelle
61 process if document preparation is enabled; \\
63 \verb|isabelle| \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} & universal {\LaTeX} tool
64 wrapper invoked multiple times by \verb|isabelle| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}; also useful for manual experiments; \\
67 \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
73 \isamarkupsection{Generating theory browser information \label{sec:info}%
77 \begin{isamarkuptext}%
78 \index{theory browsing information|bold}
80 As a side-effect of running a logic sessions, Isabelle is able to
81 generate theory browsing information, including HTML documents that
82 show a theory's definition, the theorems proved in its ML file and
83 the relationship with its ancestors and descendants. Besides the
84 HTML file that is generated for every theory, Isabelle stores links
85 to all theories in an index file. These indexes are linked with
86 other indexes to represent the overall tree structure of logic
89 Isabelle also generates graph files that represent the theory
90 hierarchy of a logic. There is a graph browser Java applet embedded
91 in the generated HTML pages, and also a stand-alone application that
92 allows browsing theory graphs without having to start a WWW client
93 first. The latter version also includes features such as generating
94 Postscript files, which are not available in the applet version.
95 See \secref{sec:browse} for further information.
99 The easiest way to let Isabelle generate theory browsing information
100 for existing sessions is to append ``\verb|-i true|'' to the
101 \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} before invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} (or \hyperlink{file.$ISABELLE-HOME/build}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}build}}}}). For
102 example, add something like this to your Isabelle settings file
105 ISABELLE_USEDIR_OPTIONS="-i true"
108 and then change into the \hyperlink{file.~~/src/FOL}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL}}}} directory and run
109 \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|. The presentation output will appear in
110 \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
111 \verb|~/.isabelle/browser_info/FOL|. Note that option
112 \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
113 more explicit about such details.
115 Many standard Isabelle sessions (such as \hyperlink{file.~~/src/HOL/ex}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}ex}}}})
116 also provide actual printable documents. These are prepared
117 automatically as well if enabled like this, using the \verb|-d| option
119 ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
121 Enabling options \verb|-i| and \verb|-d|
122 simultaneously as shown above causes an appropriate ``document''
123 link to be included in the HTML index. Documents (or raw document
124 sources) may be generated independently of browser information as
125 well, see \secref{sec:tool-document} for further details.
127 \bigskip The theory browsing information is stored in a
128 sub-directory directory determined by the \indexref{}{setting}{ISABELLE\_BROWSER\_INFO}\hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} setting plus a prefix corresponding to the
129 session identifier (according to the tree structure of sub-sessions
130 by default). A complete WWW view of all standard object-logics and
131 examples of the Isabelle distribution is available at the usual
135 \url{http://isabelle.in.tum.de/dist/library/} \\
136 \url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/} \\
137 \url{http://mirror.cse.unsw.edu.au/pub/isabelle/dist/library/} \\
141 \medskip In order to present your own theories on the web, simply
142 copy the corresponding subdirectory from \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} to your WWW server, having generated browser
145 isabelle usedir -i true HOL Foo
148 This assumes that directory \verb|Foo| contains some \verb|ROOT.ML| file to load all your theories, and HOL is your parent
149 logic image (\verb|isabelle| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} assists in
150 setting up Isabelle session directories. Theory browser information
151 for HOL should have been generated already beforehand.
152 Alternatively, one may specify an external link to an existing body
153 of HTML data by giving \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} a \verb|-P| option like
156 isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
159 \medskip For production use, the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} tool is usually
160 invoked in an appropriate \verb|IsaMakefile|, via the Isabelle
161 \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} tool. There is a separate \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool to
162 provide easy setup of all this, with only minimal manual editing
165 isabelle mkdir HOL Foo && isabelle make
167 See \secref{sec:tool-mkdir} for more information on preparing
168 Isabelle session directories, including the setup for documents.%
172 \isamarkupsection{Browsing theory graphs \label{sec:browse}%
176 \begin{isamarkuptext}%
177 \index{theory graph browser|bold}
179 The Isabelle graph browser is a general tool for visualizing
180 dependency graphs. Certain nodes of the graph (i.e.~theories) can
181 be grouped together in ``directories'', whose contents may be
182 hidden, thus enabling the user to collapse irrelevant portions of
183 information. The browser is written in Java, it can be used both as
184 a stand-alone application and as an applet. Note that the option
185 \verb|-g| of \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
186 graph presentations in batch mode for inclusion in session
191 \isamarkupsubsection{Invoking the graph browser%
195 \begin{isamarkuptext}%
196 The stand-alone version of the graph browser is wrapped up as an
197 Isabelle tool called \indexdef{}{tool}{browser}\hypertarget{tool.browser}{\hyperlink{tool.browser}{\mbox{\isa{\isatt{browser}}}}}:
200 Usage: browser [OPTIONS] [GRAPHFILE]
203 -c cleanup -- remove GRAPHFILE after use
204 -o FILE output to FILE (ps, eps, pdf)
206 When no filename is specified, the browser automatically changes to
207 the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}.
209 \medskip The \verb|-c| option causes the input file to be
212 The \verb|-o| option indicates batch-mode operation, with the
213 output written to the indicated file; note that \verb|pdf|
214 produces an \verb|eps| copy as well.
216 \medskip The applet version of the browser is part of the standard
217 WWW theory presentation, see the link ``theory dependencies'' within
222 \isamarkupsubsection{Using the graph browser%
226 \begin{isamarkuptext}%
227 The browser's main window, which is shown in
228 \figref{fig:browserwindow}, consists of two sub-windows. In the
229 left sub-window, the directory tree is displayed. The graph itself
230 is displayed in the right sub-window.
233 \includegraphics[width=\textwidth]{browser_screenshot}
234 \caption{\label{fig:browserwindow} Browser main window}
239 \isamarkupsubsubsection{The directory tree window%
243 \begin{isamarkuptext}%
244 We describe the usage of the directory browser and the meaning of
245 the different items in the browser window.
249 \item A red arrow before a directory name indicates that the
250 directory is currently ``folded'', i.e.~the nodes in this directory
251 are collapsed to one single node. In the right sub-window, the names
252 of nodes corresponding to folded directories are enclosed in square
253 brackets and displayed in red color.
255 \item A green downward arrow before a directory name indicates that
256 the directory is currently ``unfolded''. It can be folded by
257 clicking on the directory name. Clicking on the name for a second
258 time unfolds the directory again. Alternatively, a directory can
259 also be unfolded by clicking on the corresponding node in the right
262 \item Blue arrows stand before ordinary node names. When clicking on
263 such a name (i.e.\ that of a theory), the graph display window
264 focuses to the corresponding node. Double clicking invokes a text
265 viewer window in which the contents of the theory file are
272 \isamarkupsubsubsection{The graph display window%
276 \begin{isamarkuptext}%
277 When pointing on an ordinary node, an upward and a downward arrow is
278 shown. Initially, both of these arrows are green. Clicking on the
279 upward or downward arrow collapses all predecessor or successor
280 nodes, respectively. The arrow's color then changes to red,
281 indicating that the predecessor or successor nodes are currently
282 collapsed. The node corresponding to the collapsed nodes has the
283 name ``\verb|[....]|''. To uncollapse the nodes again, simply
284 click on the red arrow or on the node with the name ``\verb|[....]|''. Similar to the directory browser, the contents of
285 theory files can be displayed by double clicking on the
290 \isamarkupsubsubsection{The ``File'' menu%
294 \begin{isamarkuptext}%
295 Due to Java Applet security restrictions this menu is only available
296 in the full application version. The meaning of the menu items is as
301 \item[Open \dots] Open a new graph file.
303 \item[Export to PostScript] Outputs the current graph in Postscript
304 format, appropriately scaled to fit on one single sheet of A4 paper.
305 The resulting file can be printed directly.
307 \item[Export to EPS] Outputs the current graph in Encapsulated
308 Postscript format. The resulting file can be included in other
311 \item[Quit] Quit the graph browser.
317 \isamarkupsubsection{Syntax of graph definition files%
321 \begin{isamarkuptext}%
322 A graph definition file has the following syntax:
326 \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}{\isacharplus}{\isachardoublequote}} \\
327 \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}{\isacharasterisk}{\isachardoublequote}}
331 The meaning of the items in a vertex description is as follows:
335 \item[\isa{vertex{\isacharunderscore}name}] The name of the vertex.
337 \item[\isa{vertex{\isacharunderscore}ID}] The vertex identifier. Note that there may
338 be several vertices with equal names, whereas identifiers must be
341 \item[\isa{dir{\isacharunderscore}name}] The name of the ``directory'' the vertex
342 should be placed in. A ``\verb|+|'' sign after \isa{dir{\isacharunderscore}name} indicates that the nodes in the directory are initially
343 visible. Directories are initially invisible by default.
345 \item[\isa{path}] The path of the corresponding theory file. This
346 is specified relatively to the path of the graph definition file.
348 \item[List of successor/predecessor nodes] A ``\verb|<|''
349 sign before the list means that successor nodes are listed, a
350 ``\verb|>|'' sign means that predecessor nodes are listed. If
351 neither ``\verb|<|'' nor ``\verb|>|'' is found, the
352 browser assumes that successor nodes are listed.
358 \isamarkupsection{Creating Isabelle session directories
359 \label{sec:tool-mkdir}%
363 \begin{isamarkuptext}%
364 The \indexdef{}{tool}{mkdir}\hypertarget{tool.mkdir}{\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}} utility prepares Isabelle session source
365 directories, including a sensible default setup of \verb|IsaMakefile|, \verb|ROOT.ML|, and a \verb|document|
366 directory with a minimal \verb|root.tex| that is sufficient to
367 print all theories of the session (in the order of appearance); see
368 \secref{sec:tool-document} for further information on Isabelle
369 document preparation. The usage of \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is:
372 Usage: mkdir [OPTIONS] [LOGIC] NAME
375 -I FILE alternative IsaMakefile output
376 -P include parent logic target
377 -b setup build mode (session outputs heap image)
380 Prepare session directory, including IsaMakefile and document source,
381 with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
384 The \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool is conservative in the sense that any
385 existing \verb|IsaMakefile| etc.\ is left unchanged. Thus it
386 is safe to invoke it multiple times, although later runs may not
387 have the desired effect.
389 Note that \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is unable to change \verb|IsaMakefile|
390 incrementally --- manual changes are required for multiple
391 sub-sessions. On order to get an initial working session, the only
392 editing needed is to add appropriate \verb|use_thy| calls to the
393 generated \verb|ROOT.ML| file.%
397 \isamarkupsubsubsection{Options%
401 \begin{isamarkuptext}%
402 The \verb|-I| option specifies an alternative to \verb|IsaMakefile| for dependencies. Note that ``\verb|-|'' refers
403 to \emph{stdout}, i.e.\ ``\verb|-I-|'' provides an easy way
404 to peek at \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}'s idea of \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} setup required for
405 some particular of Isabelle session.
407 \medskip The \verb|-P| option includes a target for the
408 parent \verb|LOGIC| session in the generated \verb|IsaMakefile|. The corresponding sources are assumed to be located
409 within the Isabelle distribution.
411 \medskip The \verb|-b| option sets up the current directory
412 as the base for a new session that provides an actual logic image,
413 as opposed to one that only runs several theories based on an
414 existing image. Note that in the latter case, everything except
415 \verb|IsaMakefile| would be placed into a separate directory
416 \verb|NAME|, rather than the current one. See
417 \secref{sec:tool-usedir} for further information on \emph{build
418 mode} vs.\ \emph{example mode} of the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility.
420 \medskip The \verb|-q| option enables quiet mode, suppressing
421 further notes on how to proceed.%
425 \isamarkupsubsubsection{Examples%
429 \begin{isamarkuptext}%
430 The standard setup of a single ``example session'' based on the
431 default logic, with proper document generation is generated like
434 isabelle mkdir Foo && isabelle make
437 \noindent The theory sources should be put into the \verb|Foo|
438 directory, and its \verb|ROOT.ML| should be edited to load all
439 required theories. Invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} again
440 would run the whole session, generating browser information and the
441 document automatically. The \verb|IsaMakefile| is typically
442 tuned manually later, e.g.\ adding source dependencies, or changing
443 the options passed to \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}.
445 \medskip Large projects may demand further sessions, potentially
446 with separate logic images being created. This usually requires
447 manual editing of the generated \verb|IsaMakefile|, which is
448 meant to cover all of the sub-session directories at the same time
449 (this is the deeper reasong why \verb|IsaMakefile| is not made
450 part of the initial session directory created by \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}). See \hyperlink{file.~~/src/HOL/IsaMakefile}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}IsaMakefile}}}} for
451 a full-blown example.%
455 \isamarkupsection{Running Isabelle sessions \label{sec:tool-usedir}%
459 \begin{isamarkuptext}%
460 The \indexdef{}{tool}{usedir}\hypertarget{tool.usedir}{\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}} utility builds object-logic images, or runs
461 example sessions based on existing logics. Its usage is:
464 Usage: usedir [OPTIONS] LOGIC NAME
467 -C BOOL copy existing document directory to -D PATH (default true)
468 -D PATH dump generated document sources into PATH
469 -M MAX multithreading: maximum number of worker threads (default 1)
470 -P PATH set path for remote theory browsing information
471 -Q BOOL check proofs in parallel (default true)
472 -T LEVEL multithreading: trace level (default 0)
473 -V VERSION declare alternative document VERSION
474 -b build mode (output heap image, using current dir)
475 -d FORMAT build document as FORMAT (default false)
476 -f NAME use ML file NAME (default ROOT.ML)
477 -g BOOL generate session graph image for document (default false)
478 -i BOOL generate theory browser information (default false)
479 -m MODE add print mode for output
480 -p LEVEL set level of detail for proof objects (default 0)
481 -q LEVEL set level of parallel proof checking (default 1)
482 -r reset session path
483 -s NAME override session NAME
484 -t BOOL internal session timing (default false)
485 -v BOOL be verbose (default false)
487 Build object-logic or run examples. Also creates browsing
488 information (HTML etc.) according to settings.
490 ISABELLE_USEDIR_OPTIONS=
493 ML_PLATFORM=x86-linux
494 ML_HOME=/usr/local/polyml-5.2.1/x86-linux
495 ML_SYSTEM=polyml-5.2.1
499 Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}}
500 setting is implicitly prefixed to \emph{any} \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
501 call. Since the \verb|IsaMakefile|s of all object-logics
502 distributed with Isabelle just invoke \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} for the real
503 work, one may control compilation options globally via above
504 variable. In particular, generation of \rmindex{HTML} browsing
505 information and document preparation is controlled here.
507 The \indexref{}{setting}{HOL\_USEDIR\_OPTIONS}\hyperlink{setting.HOL-USEDIR-OPTIONS}{\mbox{\isa{\isatt{HOL{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} setting is specific to the
508 plain and main Isabelle/HOL images; its value is appended to
509 \hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} for these particular sessions
514 \isamarkupsubsubsection{Options%
518 \begin{isamarkuptext}%
519 Basically, there are two different modes of operation: \emph{build
520 mode} (enabled through the \verb|-b| option) and
521 \emph{example mode} (default).
523 Calling \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} with \verb|-b| runs \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} with input image \verb|LOGIC| and output to
524 \verb|NAME|, as provided on the command line. This will be a
525 batch session, running \verb|ROOT.ML| from the current
526 directory and then quitting. It is assumed that \verb|ROOT.ML|
527 contains all ML commands required to build the logic.
529 In example mode, \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} runs a read-only session of
530 \verb|LOGIC| and automatically runs \verb|ROOT.ML| from
531 within directory \verb|NAME|. It assumes that this file
532 contains appropriate ML commands to run the desired examples.
534 \medskip The \verb|-i| option controls theory browser data
535 generation. It may be explicitly turned on or off --- as usual, the
536 last occurrence of \verb|-i| on the command line wins.
538 The \verb|-P| option specifies a path (or actual URL) to be
539 prefixed to any \emph{non-local} reference of existing theories.
540 Thus user sessions may easily link to existing Isabelle libraries
541 already present on the WWW.
543 The \verb|-m| options specifies additional print modes to be
544 activated temporarily while the session is processed.
546 \medskip The \verb|-d| option controls document preparation.
547 Valid arguments are \verb|false| (do not prepare any document;
548 this is default), or any of \verb|dvi|, \verb|dvi.gz|,
549 \verb|ps|, \verb|ps.gz|, \verb|pdf|. The logic
550 session has to provide a properly setup \verb|document|
551 directory. See \secref{sec:tool-document} and
552 \secref{sec:tool-latex} for more details.
554 \medskip The \verb|-V| option declares alternative document
555 versions, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool). The
556 standard document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end
557 commands, proof body texts, and ML code will be presented
558 faithfully. An alternative version ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
559 original text by a short place-holder. The form ``\isa{name}\verb|=-|,'' means to remove document \isa{name} from
560 the list of versions to be processed. Any number of \verb|-V| options may be given; later declarations have precedence over
563 \medskip The \verb|-g| option produces images of the theory
564 dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
565 generated document, both as \verb|session_graph.eps| and
566 \verb|session_graph.pdf| at the same time. To include this in
567 the final {\LaTeX} document one could say \verb|\includegraphics{session_graph}| in \verb|document/root.tex| (omitting the file-name extension enables
568 {\LaTeX} to select to correct version, either for the DVI or PDF
571 \medskip The \verb|-D| option causes the generated document
572 sources to be dumped at location \verb|PATH|; this path is
573 relative to the session's main directory. If the \verb|-C|
574 option is true, this will include a copy of an existing \verb|document| directory as provided by the user. For example,
575 \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}~\verb|-D generated HOL|\isasep\isanewline%
576 \verb| Foo| produces a complete set of document sources at \verb|Foo/generated|. Subsequent invocation of \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|Foo/generated| (see also
577 \secref{sec:tool-document}) will process the final result
578 independently of an Isabelle job. This decoupled mode of operation
579 facilitates debugging of serious {\LaTeX} errors, for example.
581 \medskip The \verb|-p| option determines the level of detail
582 for internal proof objects, see also the \emph{Isabelle Reference
583 Manual}~\cite{isabelle-ref}.
585 \medskip The \verb|-q| option specifies the level of parallel
586 proof checking: \verb|0| no proofs, \verb|1| toplevel
587 proofs (default), \verb|2| toplevel and nested Isar proofs.
588 The resulting speedup may vary, depending on the number of worker
589 threads, granularity of proofs, and whether proof terms are enabled.
591 \medskip The \verb|-t| option produces a more detailed
592 internal timing report of the session.
594 \medskip The \verb|-v| option causes additional information
595 to be printed while running the session, notably the location of
598 \medskip The \verb|-M| option specifies the maximum number of
599 parallel threads used for processing independent tasks when checking
600 theory sources (multithreading only works on suitable ML platforms).
601 The special value of \verb|0| or \verb|max| refers to the
602 number of actual CPU cores of the underlying machine, which is a
603 good starting point for optimal performance tuning. The \verb|-T| option determines the level of detail in tracing output
604 concerning the internal locking and scheduling in multithreaded
605 operation. This may be helpful in isolating performance
606 bottle-necks, e.g.\ due to excessive wait states when locking
607 critical code sections.
609 \medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
610 identifier}. These accumulate, documenting the way sessions depend
611 on others. For example, consider \verb|Pure/FOL/ex|, which
612 refers to the examples of FOL, which in turn is built upon Pure.
614 The current session's identifier is by default just the base name of
615 the \verb|LOGIC| argument (in build mode), or of the \verb|NAME| argument (in example mode). This may be overridden explicitly
616 via the \verb|-s| option.%
620 \isamarkupsubsubsection{Examples%
624 \begin{isamarkuptext}%
625 Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
626 object-logics as a model for your own developments. For example,
627 see \hyperlink{file.~~/src/FOL/IsaMakefile}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}IsaMakefile}}}}. The Isabelle \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool creates \verb|IsaMakefile|s with proper invocation
628 of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} as well.%
632 \isamarkupsection{Preparing Isabelle session documents
633 \label{sec:tool-document}%
637 \begin{isamarkuptext}%
638 The \indexdef{}{tool}{document}\hypertarget{tool.document}{\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}} utility prepares logic session documents,
639 processing the sources both as provided by the user and generated by
640 Isabelle. Its usage is:
642 Usage: document [OPTIONS] [DIR]
645 -c cleanup -- be aggressive in removing old stuff
646 -n NAME specify document name (default 'document')
647 -o FORMAT specify output format: dvi (default), dvi.gz, ps,
649 -t TAGS specify tagged region markup
651 Prepare the theory session document in DIR (default 'document')
652 producing the specified output format.
654 This tool is usually run automatically as part of the corresponding
655 Isabelle batch process, provided document preparation has been
656 enabled (cf.\ the \verb|-d| option of the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
657 tool). It may be manually invoked on the generated browser
658 information document output as well, e.g.\ in case of errors
659 encountered in the batch run.
661 \medskip The \verb|-c| option tells the \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool
662 to dispose the document sources after successful operation. This is
663 the right thing to do for sources generated by an Isabelle process,
664 but take care of your files in manual document preparation!
666 \medskip The \verb|-n| and \verb|-o| option specify
667 the final output file name and format, the default is ``\verb|document.dvi|''. Note that the result will appear in the parent of
668 the target \verb|DIR|.
670 \medskip The \verb|-t| option tells {\LaTeX} how to interpret
671 tagged Isabelle command regions. Tags are specified as a comma
672 separated list of modifier/name pairs: ``\verb|+|\isa{foo}'' (or just ``\isa{foo}'') means to keep, ``\verb|-|\isa{foo}'' to drop, and ``\verb|/|\isa{foo}'' to
673 fold text tagged as \isa{foo}. The builtin default is equivalent
674 to the tag specification ``\verb|+theory,+proof,+ML,+visible,-invisible|''; see also the {\LaTeX}
675 macros \verb|\isakeeptag|, \verb|\isadroptag|, and
676 \verb|\isafoldtag|, in \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}}.
678 \medskip Document preparation requires a properly setup ``\verb|document|'' directory within the logic session sources. This
679 directory is supposed to contain all the files needed to produce the
680 final document --- apart from the actual theories which are
681 generated by Isabelle.
683 \medskip For most practical purposes, the \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool is
684 smart enough to create any of the specified output formats, taking
685 \verb|root.tex| supplied by the user as a starting point. This
686 even includes multiple runs of {\LaTeX} to accommodate references
687 and bibliographies (the latter assumes \verb|root.bib| within
690 In more complex situations, a separate \verb|IsaMakefile| for
691 the document sources may be given instead. This should provide
692 targets for any admissible document format; these have to produce
693 corresponding output files named after \verb|root| as well,
694 e.g.\ \verb|root.dvi| for target format \verb|dvi|.
696 \medskip When running the session, Isabelle copies the original
697 \verb|document| directory into its proper place within
698 \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} according to the session path.
699 Then, for any processed theory \isa{A} some {\LaTeX} source is
700 generated and put there as \isa{A}\verb|.tex|.
701 Furthermore, a list of all generated theory files is put into
702 \verb|session.tex|. Typically, the root {\LaTeX} file provided
703 by the user would include \verb|session.tex| to get a document
704 containing all the theories.
706 The {\LaTeX} versions of the theories require some macros defined in
707 \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}}. Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
708 the underlying Isabelle \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} tool already includes an
709 appropriate path specification for {\TeX} inputs.
711 If the text contains any references to Isabelle symbols (such as
712 \verb|\|\verb|<forall>|) then \verb|isabellesym.sty| should be included as well. This package
713 contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, see \cite{isabelle-implementation} for a
714 complete list of predefined Isabelle symbols. Users may invent
715 further symbols as well, just by providing {\LaTeX} macros in a
716 similar fashion as in \hyperlink{file.~~/lib/texinputs/isabellesym.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabellesym{\isachardot}sty}}}} of
719 For proper setup of DVI and PDF documents (with hyperlinks and
720 bookmarks), we recommend to include \hyperlink{file.~~/lib/texinputs/pdfsetup.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}pdfsetup{\isachardot}sty}}}} as well.
722 \medskip As a final step of document preparation within Isabelle,
723 \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the
724 resulting \verb|document| directory. Thus the actual output
725 document is built and installed in its proper place (as linked by
726 the session's \verb|index.html| if option \verb|-i| of
727 \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} has been enabled, cf.\ \secref{sec:info}). The
728 generated sources are deleted after successful run of {\LaTeX} and
729 friends. Note that a separate copy of the sources may be retained
730 by passing an option \verb|-D| to the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility
731 when running the session.%
735 \isamarkupsection{Running {\LaTeX} within the Isabelle environment
736 \label{sec:tool-latex}%
740 \begin{isamarkuptext}%
741 The \indexdef{}{tool}{latex}\hypertarget{tool.latex}{\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}}} utility provides the basic interface for
742 Isabelle document preparation. Its usage is:
744 Usage: latex [OPTIONS] [FILE]
747 -o FORMAT specify output format: dvi (default), dvi.gz, ps,
748 ps.gz, pdf, bbl, idx, sty, syms
750 Run LaTeX (and related tools) on FILE (default root.tex),
751 producing the specified output format.
754 Appropriate {\LaTeX}-related programs are run on the input file,
755 according to the given output format: \hyperlink{executable.latex}{\mbox{\isa{\isatt{latex}}}},
756 \hyperlink{executable.pdflatex}{\mbox{\isa{\isatt{pdflatex}}}}, \hyperlink{executable.dvips}{\mbox{\isa{\isatt{dvips}}}}, \hyperlink{executable.bibtex}{\mbox{\isa{\isatt{bibtex}}}}
757 (for \verb|bbl|), and \hyperlink{executable.makeindex}{\mbox{\isa{\isatt{makeindex}}}} (for \verb|idx|). The actual commands are determined from the settings
758 environment (\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LATEX}}}} etc.).
760 The \verb|sty| output format causes the Isabelle style files to
761 be updated from the distribution. This is useful in special
762 situations where the document sources are to be processed another
763 time by separate tools (cf.\ option \verb|-D| of the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility).
765 The \verb|syms| output is for internal use; it generates lists
766 of symbols that are available without loading additional {\LaTeX}
771 \isamarkupsubsubsection{Examples%
775 \begin{isamarkuptext}%
776 Invoking \verb|isabelle| \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} by hand may be
777 occasionally useful when debugging failed attempts of the automatic
778 document preparation stage of batch-mode Isabelle. The abortive
779 process leaves the sources at a certain place within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}, see the runtime error message for details.
780 This enables users to inspect {\LaTeX} runs in further detail, e.g.\
783 cd ~/.isabelle/browser_info/HOL/Test/document
784 isabelle latex -o pdf
794 \isacommand{end}\isamarkupfalse%
805 %%% TeX-master: "root"