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}\isactrlsup {\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}\isactrlsup {\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 -T LEVEL multithreading: trace level (default 0)
472 -V VERSION declare alternative document VERSION
473 -b build mode (output heap image, using current dir)
474 -c BOOL tell ML system to compress output image (default true)
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
481 -r reset session path
482 -s NAME override session NAME
483 -v BOOL be verbose (default false)
485 Build object-logic or run examples. Also creates browsing
486 information (HTML etc.) according to settings.
488 ISABELLE_USEDIR_OPTIONS=
492 Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}}
493 setting is implicitly prefixed to \emph{any} \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
494 call. Since the \verb|IsaMakefile|s of all object-logics
495 distributed with Isabelle just invoke \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} for the real
496 work, one may control compilation options globally via above
497 variable. In particular, generation of \rmindex{HTML} browsing
498 information and document preparation is controlled here.
500 The \indexref{}{setting}{HOL\_USEDIR\_OPTIONS}\hyperlink{setting.HOL-USEDIR-OPTIONS}{\mbox{\isa{\isatt{HOL{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} setting is specific to the
501 plain and main Isabelle/HOL images; its value is appended to
502 \hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} for these particular sessions
507 \isamarkupsubsubsection{Options%
511 \begin{isamarkuptext}%
512 Basically, there are two different modes of operation: \emph{build
513 mode} (enabled through the \verb|-b| option) and
514 \emph{example mode} (default).
516 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
517 \verb|NAME|, as provided on the command line. This will be a
518 batch session, running \verb|ROOT.ML| from the current
519 directory and then quitting. It is assumed that \verb|ROOT.ML|
520 contains all ML commands required to build the logic.
522 In example mode, \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} runs a read-only session of
523 \verb|LOGIC| and automatically runs \verb|ROOT.ML| from
524 within directory \verb|NAME|. It assumes that this file
525 contains appropriate ML commands to run the desired examples.
527 \medskip The \verb|-i| option controls theory browser data
528 generation. It may be explicitly turned on or off --- as usual, the
529 last occurrence of \verb|-i| on the command line wins.
531 The \verb|-P| option specifies a path (or actual URL) to be
532 prefixed to any \emph{non-local} reference of existing theories.
533 Thus user sessions may easily link to existing Isabelle libraries
534 already present on the WWW.
536 The \verb|-m| options specifies additional print modes to be
537 activated temporarily while the session is processed.
539 \medskip The \verb|-d| option controls document preparation.
540 Valid arguments are \verb|false| (do not prepare any document;
541 this is default), or any of \verb|dvi|, \verb|dvi.gz|,
542 \verb|ps|, \verb|ps.gz|, \verb|pdf|. The logic
543 session has to provide a properly setup \verb|document|
544 directory. See \secref{sec:tool-document} and
545 \secref{sec:tool-latex} for more details.
547 \medskip The \verb|-V| option declares alternative document
548 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
549 standard document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end
550 commands, proof body texts, and ML code will be presented
551 faithfully. An alternative version ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
552 original text by a short place-holder. The form ``\isa{name}\verb|=-|,'' means to remove document \isa{name} from
553 the list of versions to be processed. Any number of \verb|-V| options may be given; later declarations have precedence over
556 \medskip The \verb|-g| option produces images of the theory
557 dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
558 generated document, both as \verb|session_graph.eps| and
559 \verb|session_graph.pdf| at the same time. To include this in
560 the final {\LaTeX} document one could say \verb|\includegraphics{session_graph}| in \verb|document/root.tex| (omitting the file-name extension enables
561 {\LaTeX} to select to correct version, either for the DVI or PDF
564 \medskip The \verb|-D| option causes the generated document
565 sources to be dumped at location \verb|PATH|; this path is
566 relative to the session's main directory. If the \verb|-C|
567 option is true, this will include a copy of an existing \verb|document| directory as provided by the user. For example,
568 \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}~\verb|-D generated HOL|\isasep\isanewline%
569 \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
570 \secref{sec:tool-document}) will process the final result
571 independently of an Isabelle job. This decoupled mode of operation
572 facilitates debugging of serious {\LaTeX} errors, for example.
574 \medskip The \verb|-p| option determines the level of detail
575 for internal proof objects, see also the \emph{Isabelle Reference
576 Manual}~\cite{isabelle-ref}.
578 \medskip The \verb|-v| option causes additional information
579 to be printed while running the session, notably the location of
582 \medskip The \verb|-M| option specifies the maximum number of
583 parallel threads used for processing independent tasks when checking
584 theory sources (multithreading only works on suitable ML platforms).
585 The special value of \verb|0| or \verb|max| refers to the
586 number of actual CPU cores of the underlying machine, which is a
587 good starting point for optimal performance tuning. The \verb|-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 \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
594 identifier}. These accumulate, documenting the way sessions depend
595 on others. For example, consider \verb|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 \verb|LOGIC| argument (in build mode), or of the \verb|NAME| argument (in example mode). This may be overridden explicitly
600 via the \verb|-s| option.%
604 \isamarkupsubsubsection{Examples%
608 \begin{isamarkuptext}%
609 Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
610 object-logics as a model for your own developments. For example,
611 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
612 of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} as well.%
616 \isamarkupsection{Preparing Isabelle session documents
617 \label{sec:tool-document}%
621 \begin{isamarkuptext}%
622 The \indexdef{}{tool}{document}\hypertarget{tool.document}{\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}} utility prepares logic session documents,
623 processing the sources both as provided by the user and generated by
624 Isabelle. Its usage is:
626 Usage: document [OPTIONS] [DIR]
629 -c cleanup -- be aggressive in removing old stuff
630 -n NAME specify document name (default 'document')
631 -o FORMAT specify output format: dvi (default), dvi.gz, ps,
633 -t TAGS specify tagged region markup
635 Prepare the theory session document in DIR (default 'document')
636 producing the specified output format.
638 This tool is usually run automatically as part of the corresponding
639 Isabelle batch process, provided document preparation has been
640 enabled (cf.\ the \verb|-d| option of the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
641 tool). It may be manually invoked on the generated browser
642 information document output as well, e.g.\ in case of errors
643 encountered in the batch run.
645 \medskip The \verb|-c| option tells the \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool
646 to dispose the document sources after successful operation. This is
647 the right thing to do for sources generated by an Isabelle process,
648 but take care of your files in manual document preparation!
650 \medskip The \verb|-n| and \verb|-o| option specify
651 the final output file name and format, the default is ``\verb|document.dvi|''. Note that the result will appear in the parent of
652 the target \verb|DIR|.
654 \medskip The \verb|-t| option tells {\LaTeX} how to interpret
655 tagged Isabelle command regions. Tags are specified as a comma
656 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
657 fold text tagged as \isa{foo}. The builtin default is equivalent
658 to the tag specification ``\verb|/theory,/proof,/ML,+visible,-invisible|''; see also the {\LaTeX}
659 macros \verb|\isakeeptag|, \verb|\isadroptag|, and
660 \verb|\isafoldtag|, in \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}}.
662 \medskip Document preparation requires a properly setup ``\verb|document|'' directory within the logic session sources. This
663 directory is supposed to contain all the files needed to produce the
664 final document --- apart from the actual theories which are
665 generated by Isabelle.
667 \medskip For most practical purposes, the \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool is
668 smart enough to create any of the specified output formats, taking
669 \verb|root.tex| supplied by the user as a starting point. This
670 even includes multiple runs of {\LaTeX} to accommodate references
671 and bibliographies (the latter assumes \verb|root.bib| within
674 In more complex situations, a separate \verb|IsaMakefile| for
675 the document sources may be given instead. This should provide
676 targets for any admissible document format; these have to produce
677 corresponding output files named after \verb|root| as well,
678 e.g.\ \verb|root.dvi| for target format \verb|dvi|.
680 \medskip When running the session, Isabelle copies the original
681 \verb|document| directory into its proper place within
682 \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} according to the session path.
683 Then, for any processed theory \isa{A} some {\LaTeX} source is
684 generated and put there as \isa{A}\verb|.tex|.
685 Furthermore, a list of all generated theory files is put into
686 \verb|session.tex|. Typically, the root {\LaTeX} file provided
687 by the user would include \verb|session.tex| to get a document
688 containing all the theories.
690 The {\LaTeX} versions of the theories require some macros defined in
691 \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;
692 the underlying Isabelle \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} tool already includes an
693 appropriate path specification for {\TeX} inputs.
695 If the text contains any references to Isabelle symbols (such as
696 \verb|\|\verb|<forall>|) then \verb|isabellesym.sty| should be included as well. This package
697 contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, (see \appref{app:symbols} for a
698 complete list of predefined Isabelle symbols). Users may invent
699 further symbols as well, just by providing {\LaTeX} macros in a
700 similar fashion as in \hyperlink{file.~~/lib/texinputs/isabellesym.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabellesym{\isachardot}sty}}}} of
703 For proper setup of DVI and PDF documents (with hyperlinks and
704 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.
706 \medskip As a final step of document preparation within Isabelle,
707 \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the
708 resulting \verb|document| directory. Thus the actual output
709 document is built and installed in its proper place (as linked by
710 the session's \verb|index.html| if option \verb|-i| of
711 \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} has been enabled, cf.\ \secref{sec:info}). The
712 generated sources are deleted after successful run of {\LaTeX} and
713 friends. Note that a separate copy of the sources may be retained
714 by passing an option \verb|-D| to the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility
715 when running the session.%
719 \isamarkupsection{Running {\LaTeX} within the Isabelle environment
720 \label{sec:tool-latex}%
724 \begin{isamarkuptext}%
725 The \indexdef{}{tool}{latex}\hypertarget{tool.latex}{\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}}} utility provides the basic interface for
726 Isabelle document preparation. Its usage is:
728 Usage: latex [OPTIONS] [FILE]
731 -o FORMAT specify output format: dvi (default), dvi.gz, ps,
732 ps.gz, pdf, bbl, idx, sty, syms
734 Run LaTeX (and related tools) on FILE (default root.tex),
735 producing the specified output format.
738 Appropriate {\LaTeX}-related programs are run on the input file,
739 according to the given output format: \hyperlink{executable.latex}{\mbox{\isa{\isatt{latex}}}},
740 \hyperlink{executable.pdflatex}{\mbox{\isa{\isatt{pdflatex}}}}, \hyperlink{executable.dvips}{\mbox{\isa{\isatt{dvips}}}}, \hyperlink{executable.bibtex}{\mbox{\isa{\isatt{bibtex}}}}
741 (for \verb|bbl|), and \hyperlink{executable.makeindex}{\mbox{\isa{\isatt{makeindex}}}} (for \verb|idx|). The actual commands are determined from the settings
742 environment (\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LATEX}}}} etc.).
744 The \verb|sty| output format causes the Isabelle style files to
745 be updated from the distribution. This is useful in special
746 situations where the document sources are to be processed another
747 time by separate tools (cf.\ option \verb|-D| of the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility).
749 The \verb|syms| output is for internal use; it generates lists
750 of symbols that are available without loading additional {\LaTeX}
755 \isamarkupsubsubsection{Examples%
759 \begin{isamarkuptext}%
760 Invoking \verb|isabelle| \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} by hand may be
761 occasionally useful when debugging failed attempts of the automatic
762 document preparation stage of batch-mode Isabelle. The abortive
763 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.
764 This enables users to inspect {\LaTeX} runs in further detail, e.g.\
767 cd ~/isabelle/browser_info/HOL/Test/document
768 isabelle latex -o pdf
778 \isacommand{end}\isamarkupfalse%
789 %%% TeX-master: "root"