# HG changeset patch # User wenzelm # Date 1221500542 -7200 # Node ID ca9fdab0f97106062657e20622e162fdfb3e84f3 # Parent 889e5b7e006ceb5ef57b0a498541c1c53bfb0055 converted present.tex; diff -r 889e5b7e006c -r ca9fdab0f971 doc-src/System/IsaMakefile --- a/doc-src/System/IsaMakefile Mon Sep 15 17:32:12 2008 +0200 +++ b/doc-src/System/IsaMakefile Mon Sep 15 19:42:22 2008 +0200 @@ -22,7 +22,7 @@ Pure-System: $(LOG)/Pure-System.gz $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \ - Thy/Basics.thy + Thy/Basics.thy Thy/Presentation.thy @$(USEDIR) -s System Pure Thy diff -r 889e5b7e006c -r ca9fdab0f971 doc-src/System/Makefile --- a/doc-src/System/Makefile Mon Sep 15 17:32:12 2008 +0200 +++ b/doc-src/System/Makefile Mon Sep 15 19:42:22 2008 +0200 @@ -12,8 +12,9 @@ include ../Makefile.in NAME = system -FILES = system.tex Thy/document/Basics.tex misc.tex present.tex symbols.tex \ - ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib +FILES = system.tex Thy/document/Basics.tex misc.tex \ + Thy/document/Presentation.tex symbols.tex ../iman.sty \ + ../extra.sty ../ttbox.sty ../manual.bib OUTPUT = syms.tex diff -r 889e5b7e006c -r ca9fdab0f971 doc-src/System/Thy/Presentation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/Presentation.thy Mon Sep 15 19:42:22 2008 +0200 @@ -0,0 +1,759 @@ +(* $Id$ *) + +theory Presentation +imports Pure +begin + +chapter {* Presenting theories \label{ch:present} *} + +text {* + Isabelle provides several ways to present the outcome of formal + developments, including WWW-based browsable libraries or actual + printable documents. Presentation is centered around the concept of + \emph{logic sessions}. The global session structure is that of a + tree, with Isabelle Pure at its root, further object-logics derived + (e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions + in leaf positions (usually without a separate image). + + The Isabelle tools @{tool_ref mkdir} and @{tool_ref make} provide + the primary means for managing Isabelle sessions, including proper + setup for presentation. Here the @{tool_ref usedir} tool takes care + to let @{executable_ref "isabelle-process"} process run any + additional stages required for document preparation, notably the + tools @{tool_ref document} and @{tool_ref latex}. The complete tool + chain for managing batch-mode Isabelle sessions is illustrated in + \figref{fig:session-tools}. + + \begin{figure}[htbp] + \begin{center} + \begin{tabular}{lp{0.6\textwidth}} + + @{verbatim "isatool mkdir"} & invoked once by the user to create + the initial source setup (common @{verbatim IsaMakefile} plus a + single session directory); \\ + + @{verbatim "isatool make"} & invoked repeatedly by the user to + keep session output up-to-date (HTML, documents etc.); \\ + + @{verbatim "isatool usedir"} & part of the standard @{verbatim + IsaMakefile} entry of a session; \\ + + @{verbatim "isabelle-process"} & run through @{verbatim "isatool + usedir"}; \\ + + @{verbatim "isatool document"} & run by the Isabelle process if + document preparation is enabled; \\ + + @{verbatim "isatool latex"} & universal {\LaTeX} tool wrapper + invoked multiple times by @{verbatim "isatool document"}; also + useful for manual experiments; \\ + + \end{tabular} + \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools} + \end{center} + \end{figure} +*} + + +section {* Generating theory browser information \label{sec:info} *} + +text {* + \index{theory browsing information|bold} + + As a side-effect of running a logic sessions, Isabelle is able to + generate theory browsing information, including HTML documents that + show a theory's definition, the theorems proved in its ML file and + the relationship with its ancestors and descendants. Besides the + HTML file that is generated for every theory, Isabelle stores links + to all theories in an index file. These indexes are linked with + other indexes to represent the overall tree structure of logic + sessions. + + Isabelle also generates graph files that represent the theory + hierarchy of a logic. There is a graph browser Java applet embedded + in the generated HTML pages, and also a stand-alone application that + allows browsing theory graphs without having to start a WWW client + first. The latter version also includes features such as generating + Postscript files, which are not available in the applet version. + See \secref{sec:browse} for further information. + + \medskip + + The easiest way to let Isabelle generate theory browsing information + for existing sessions is to append ``@{verbatim "-i true"}'' to the + @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim + "isatool make"} (or @{verbatim "./build"} in the distribution). For + example, add something like this to your Isabelle settings file + +\begin{ttbox} +ISABELLE_USEDIR_OPTIONS="-i true" +\end{ttbox} + + and then change into the @{verbatim "src/FOL"} directory of the + Isabelle distribution and run @{verbatim "isatool make"}, or even + @{verbatim "isatool make all"}. The presentation output will appear + in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to + @{verbatim "~/isabelle/browser_info/FOL"}. Note that option + @{verbatim "-v true"} will make the internal runs of @{tool usedir} + more explicit about such details. + + Many standard Isabelle sessions (such as @{verbatim "HOL/ex"}) also + provide actual printable documents. These are prepared + automatically as well if enabled like this, using the @{verbatim + "-d"} option +\begin{ttbox} +ISABELLE_USEDIR_OPTIONS="-i true -d dvi" +\end{ttbox} + Enabling options @{verbatim "-i"} and @{verbatim "-d"} + simultaneausly as shown above causes an appropriate ``document'' + link to be included in the HTML index. Documents (or raw document + sources) may be generated independently of browser information as + well, see \secref{sec:tool-document} for further details. + + \bigskip The theory browsing information is stored in a + sub-directory directory determined by the @{setting_ref + ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the + session identifier (according to the tree structure of sub-sessions + by default). A complete WWW view of all standard object-logics and + examples of the Isabelle distribution is available at the Cambridge + or Munich Isabelle sites: + \begin{center}\small + \begin{tabular}{l} + \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ + \url{http://isabelle.in.tum.de/library/} \\ + \end{tabular} + \end{center} + + \medskip In order to present your own theories on the web, simply + copy the corresponding subdirectory from @{setting + ISABELLE_BROWSER_INFO} to your WWW server, having generated browser + info like this: +\begin{ttbox} +isatool usedir -i true HOL Foo +\end{ttbox} + + This assumes that directory @{verbatim Foo} contains some @{verbatim + ROOT.ML} file to load all your theories, and HOL is your parent + logic image (@{verbatim isatool}~@{tool_ref mkdir} assists in + setting up Isabelle session directories. Theory browser information + for HOL should have been generated already beforehand. + Alternatively, one may specify an external link to an existing body + of HTML data by giving @{tool usedir} a @{verbatim "-P"} option like + this: +\begin{ttbox} +isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo +\end{ttbox} + + \medskip For production use, the @{tool usedir} tool is usually + invoked in an appropriate @{verbatim IsaMakefile}, via the Isabelle + @{tool make} tool. There is a separate @{tool mkdir} tool to + provide easy setup of all this, with only minimal manual editing + required. +\begin{ttbox} +isatool mkdir HOL Foo && isatool make +\end{ttbox} + See \secref{sec:tool-mkdir} for more information on preparing + Isabelle session directories, including the setup for documents. +*} + + +section {* Browsing theory graphs \label{sec:browse} *} + +text {* + \index{theory graph browser|bold} + + The Isabelle graph browser is a general tool for visualizing + dependency graphs. Certain nodes of the graph (i.e.~theories) can + be grouped together in ``directories'', whose contents may be + hidden, thus enabling the user to collapse irrelevant portions of + information. The browser is written in Java, it can be used both as + a stand-alone application and as an applet. Note that the option + @{verbatim "-g"} of @{verbatim isatool}~@{tool_ref usedir} creates + graph presentations in batch mode for inclusion in session + documents. +*} + + +subsection {* Invoking the graph browser *} + +text {* + The stand-alone version of the graph browser is wrapped up as an + Isabelle tool called @{tool_def browser}: + +\begin{ttbox} +Usage: browser [OPTIONS] [GRAPHFILE] + + Options are: + -c cleanup -- remove GRAPHFILE after use + -o FILE output to FILE (ps, eps, pdf) +\end{ttbox} + When no filename is specified, the browser automatically changes to + the directory @{setting ISABELLE_BROWSER_INFO}. + + \medskip The @{verbatim "-c"} option causes the input file to be + removed after use. + + The @{verbatim "-o"} option indicates batch-mode operation, with the + output written to the indicated file; note that @{verbatim pdf} + produces an @{verbatim eps} copy as well. + + \medskip The applet version of the browser is part of the standard + WWW theory presentation, see the link ``theory dependencies'' within + each session index. +*} + + +subsection {* Using the graph browser *} + +text {* + The browser's main window, which is shown in + \figref{fig:browserwindow}, consists of two sub-windows. In the + left sub-window, the directory tree is displayed. The graph itself + is displayed in the right sub-window. + + \begin{figure}[ht] + \includegraphics[width=\textwidth]{browser_screenshot} + \caption{\label{fig:browserwindow} Browser main window} + \end{figure} +*} + + +subsubsection {* The directory tree window *} + +text {* + We describe the usage of the directory browser and the meaning of + the different items in the browser window. + + \begin{itemize} + + \item A red arrow before a directory name indicates that the + directory is currently ``folded'', i.e.~the nodes in this directory + are collapsed to one single node. In the right sub-window, the names + of nodes corresponding to folded directories are enclosed in square + brackets and displayed in red color. + + \item A green downward arrow before a directory name indicates that + the directory is currently ``unfolded''. It can be folded by + clicking on the directory name. Clicking on the name for a second + time unfolds the directory again. Alternatively, a directory can + also be unfolded by clicking on the corresponding node in the right + sub-window. + + \item Blue arrows stand before ordinary node names. When clicking on + such a name (i.e.\ that of a theory), the graph display window + focuses to the corresponding node. Double clicking invokes a text + viewer window in which the contents of the theory file are + displayed. + + \end{itemize} +*} + + +subsubsection {* The graph display window *} + +text {* + When pointing on an ordinary node, an upward and a downward arrow is + shown. Initially, both of these arrows are green. Clicking on the + upward or downward arrow collapses all predecessor or successor + nodes, respectively. The arrow's color then changes to red, + indicating that the predecessor or successor nodes are currently + collapsed. The node corresponding to the collapsed nodes has the + name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply + click on the red arrow or on the node with the name ``@{verbatim + "[....]"}''. Similar to the directory browser, the contents of + theory files can be displayed by double clicking on the + corresponding node. +*} + + +subsubsection {* The ``File'' menu *} + +text {* + Due to Java Applet security restrictions this menu is only available + in the full application version. The meaning of the menu items is as + follows: + + \begin{description} + + \item[Open \dots] Open a new graph file. + + \item[Export to PostScript] Outputs the current graph in Postscript + format, appropriately scaled to fit on one single sheet of A4 paper. + The resulting file can be printed directly. + + \item[Export to EPS] Outputs the current graph in Encapsulated + Postscript format. The resulting file can be included in other + documents. + + \item[Quit] Quit the graph browser. + + \end{description} +*} + + +subsection {* Syntax of graph definition files *} + +text {* + A graph definition file has the following syntax: + + \begin{tabular}{rcl} + @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\ + @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"} + \end{tabular} + + The meaning of the items in a vertex description is as follows: + + \begin{description} + + \item[@{text vertex_name}] The name of the vertex. + + \item[@{text vertex_ID}] The vertex identifier. Note that there may + be several vertices with equal names, whereas identifiers must be + unique. + + \item[@{text dir_name}] The name of the ``directory'' the vertex + should be placed in. A ``@{verbatim "+"}'' sign after @{text + dir_name} indicates that the nodes in the directory are initially + visible. Directories are initially invisible by default. + + \item[@{text path}] The path of the corresponding theory file. This + is specified relatively to the path of the graph definition file. + + \item[List of successor/predecessor nodes] A ``@{verbatim "<"}'' + sign before the list means that successor nodes are listed, a + ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If + neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the + browser assumes that successor nodes are listed. + + \end{description} +*} + + +section {* Creating Isabelle session directories + \label{sec:tool-mkdir} *} + +text {* + The @{tool_def mkdir} utility prepares Isabelle session source + directories, including a sensible default setup of @{verbatim + IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document} + directory with a minimal @{verbatim root.tex} that is sufficient to + print all theories of the session (in the order of appearance); see + \secref{sec:tool-document} for further information on Isabelle + document preparation. The usage of @{verbatim "isatool mkdir"} is: + +\begin{ttbox} +Usage: mkdir [OPTIONS] [LOGIC] NAME + + Options are: + -I FILE alternative IsaMakefile output + -P include parent logic target + -b setup build mode (session outputs heap image) + -q quiet mode + + Prepare session directory, including IsaMakefile and document source, + with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC) +\end{ttbox} + + The @{tool mkdir} tool is conservative in the sense that any + existing @{verbatim IsaMakefile} etc.\ is left unchanged. Thus it + is safe to invoke it multiple times, although later runs may not + have the desired effect. + + Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile} + incrementally --- manual changes are required for multiple + sub-sessions. On order to get an initial working session, the only + editing needed is to add appropriate @{ML use_thy} calls to the + generated @{verbatim ROOT.ML} file. +*} + + +subsubsection {* Options *} + +text {* + The @{verbatim "-I"} option specifies an alternative to @{verbatim + IsaMakefile} for dependencies. Note that ``@{verbatim "-"}'' refers + to \emph{stdout}, i.e.\ ``@{verbatim "-I-"}'' provides an easy way + to peek at @{tool mkdir}'s idea of @{tool make} setup required for + some particular of Isabelle session. + + \medskip The @{verbatim "-P"} option includes a target for the + parent @{verbatim LOGIC} session in the generated @{verbatim + IsaMakefile}. The corresponding sources are assumed to be located + within the Isabelle distribution. + + \medskip The @{verbatim "-b"} option sets up the current directory + as the base for a new session that provides an actual logic image, + as opposed to one that only runs several theories based on an + existing image. Note that in the latter case, everything except + @{verbatim IsaMakefile} would be placed into a separate directory + @{verbatim NAME}, rather than the current one. See + \secref{sec:tool-usedir} for further information on \emph{build + mode} vs.\ \emph{example mode} of the @{tool usedir} utility. + + \medskip The @{verbatim "-q"} option enables quiet mode, suppressing + further notes on how to proceed. +*} + + +subsubsection {* Examples *} + +text {* + The standard setup of a single ``example session'' based on the + default logic, with proper document generation is generated like + this: +\begin{ttbox} +isatool mkdir Foo && isatool make +\end{ttbox} + + \noindent The theory sources should be put into the @{verbatim Foo} + directory, and its @{verbatim ROOT.ML} should be edited to load all + required theories. Invoking @{verbatim "isatool make"} again would + run the whole session, generating browser information and the + document automatically. The @{verbatim IsaMakefile} is typically + tuned manually later, e.g.\ adding source dependencies, or changing + the options passed to @{tool usedir}. + + \medskip Large projects may demand further sessions, potentially + with separate logic images being created. This usually requires + manual editing of the generated @{verbatim IsaMakefile}, which is + meant to cover all of the sub-session directories at the same time + (this is the deeper reasong why @{verbatim IsaMakefile} is not made + part of the initial session directory created by @{verbatim "isatool + mkdir"}). See @{verbatim "src/HOL/IsaMakefile"} of the Isabelle + distribution for a full-blown example. +*} + + +section {* Running Isabelle sessions \label{sec:tool-usedir} *} + +text {* + The @{tool_def usedir} utility builds object-logic images, or runs + example sessions based on existing logics. Its usage is: +\begin{ttbox} + +Usage: usedir [OPTIONS] LOGIC NAME + + Options are: + -C BOOL copy existing document directory to -D PATH (default true) + -D PATH dump generated document sources into PATH + -M MAX multithreading: maximum number of worker threads (default 1) + -P PATH set path for remote theory browsing information + -T LEVEL multithreading: trace level (default 0) + -V VERSION declare alternative document VERSION + -b build mode (output heap image, using current dir) + -c BOOL tell ML system to compress output image (default true) + -d FORMAT build document as FORMAT (default false) + -f NAME use ML file NAME (default ROOT.ML) + -g BOOL generate session graph image for document (default false) + -i BOOL generate theory browser information (default false) + -m MODE add print mode for output + -p LEVEL set level of detail for proof objects + -r reset session path + -s NAME override session NAME + -v BOOL be verbose (default false) + + Build object-logic or run examples. Also creates browsing + information (HTML etc.) according to settings. + + ISABELLE_USEDIR_OPTIONS= + HOL_USEDIR_OPTIONS= +\end{ttbox} + + Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS} + setting is implicitly prefixed to \emph{any} @{tool usedir} + call. Since the @{verbatim IsaMakefile}s of all object-logics + distributed with Isabelle just invoke \texttt{usedir} for the real + work, one may control compilation options globally via above + variable. In particular, generation of \rmindex{HTML} browsing + information and document preparation is controlled here. + + The @{setting_ref HOL_USEDIR_OPTIONS} setting is specific to the + plain and main Isabelle/HOL images; its value is appended to + @{setting ISABELLE_USEDIR_OPTIONS} for these particular sessions + only. +*} + + +subsubsection {* Options *} + +text {* + Basically, there are two different modes of operation: \emph{build + mode} (enabled through the @{verbatim "-b"} option) and + \emph{example mode} (default). + + Calling @{tool usedir} with @{verbatim "-b"} runs @{executable + "isabelle-process"} with input image @{verbatim LOGIC} and output to + @{verbatim NAME}, as provided on the command line. This will be a + batch session, running @{verbatim ROOT.ML} from the current + directory and then quitting. It is assumed that @{verbatim ROOT.ML} + contains all ML commands required to build the logic. + + In example mode, @{verbatim usedir} runs a read-only session of + @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from + within directory @{verbatim NAME}. It assumes that this file + contains appropriate ML commands to run the desired examples. + + \medskip The @{verbatim "-i"} option controls theory browser data + generation. It may be explicitly turned on or off --- as usual, the + last occurrence of @{verbatim "-i"} on the command line wins. + + The @{verbatim "-P"} option specifies a path (or actual URL) to be + prefixed to any \emph{non-local} reference of existing theories. + Thus user sessions may easily link to existing Isabelle libraries + already present on the WWW. + + The @{verbatim "-m"} options specifies additional print modes to be + activated temporarily while the session is processed. + + \medskip The @{verbatim "-d"} option controls document preparation. + Valid arguments are @{verbatim false} (do not prepare any document; + this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz}, + @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}. The logic + session has to provide a properly setup @{verbatim document} + directory. See \secref{sec:tool-document} and + \secref{sec:tool-latex} for more details. + + \medskip The @{verbatim "-V"} option declares alternative document + versions, consisting of name/tags pairs (cf.\ options @{verbatim + "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool). The + standard document is equivalent to ``@{verbatim + "document=theory,proof,ML"}'', which means that all theory begin/end + commands, proof body texts, and ML code will be presented + faithfully. An alternative version ``@{verbatim + "outline=/proof/ML"}'' would fold proof and ML parts, replacing the + original text by a short place-holder. The form ``@{text + name}@{verbatim "=-"},'' means to remove document @{text name} from + the list of versions to be processed. Any number of @{verbatim + "-V"} options may be given; later declarations have precedence over + earlier ones. + + \medskip The @{verbatim "-g"} option produces images of the theory + dependency graph (cf.\ \secref{sec:browse}) for inclusion in the + generated document, both as @{verbatim session_graph.eps} and + @{verbatim session_graph.pdf} at the same time. To include this in + the final {\LaTeX} document one could say @{verbatim + "\\includegraphics{session_graph}"} in @{verbatim + "document/root.tex"} (omitting the file-name extension enables + {\LaTeX} to select to correct version, either for the DVI or PDF + output path). + + \medskip The @{verbatim "-D"} option causes the generated document + sources to be dumped at location @{verbatim PATH}; this path is + relative to the session's main directory. If the @{verbatim "-C"} + option is true, this will include a copy of an existing @{verbatim + document} directory as provided by the user. For example, + @{verbatim "isatool usedir -D generated HOL Foo"} produces a + complete set of document sources at @{verbatim "Foo/generated"}. + Subsequent invocation of @{verbatim "isatool document + Foo/generated"} (see also \secref{sec:tool-document}) will process + the final result independently of an Isabelle job. This decoupled + mode of operation facilitates debugging of serious {\LaTeX} errors, + for example. + + \medskip The @{verbatim "-p"} option determines the level of detail + for internal proof objects, see also the \emph{Isabelle Reference + Manual}~\cite{isabelle-ref}. + + \medskip The @{verbatim "-v"} option causes additional information + to be printed while running the session, notably the location of + prepared documents. + + \medskip The @{verbatim "-M"} option specifies the maximum number of + parallel threads used for processing independent tasks when checking + theory sources (multithreading only works on suitable ML platforms). + The special value of ``@{verbatim 0}'' or ``@{verbatim max}'' refers + to the number of actual CPU cores of the underlying machine, which + is a good starting point for optimal performance tuning. The + @{verbatim "-T"} option determines the level of detail in tracing + output concerning the internal locking and scheduling in + multithreaded operation. This may be helpful in isolating + performance bottle-necks, e.g.\ due to excessive wait states when + locking critical code sections. + + \medskip Any @{tool usedir} session is named by some \emph{session + identifier}. These accumulate, documenting the way sessions depend + on others. For example, consider @{verbatim "Pure/FOL/ex"}, which + refers to the examples of FOL, which in turn is built upon Pure. + + The current session's identifier is by default just the base name of + the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim + NAME} argument (in example mode). This may be overridden explicitly + via the @{verbatim "-s"} option. +*} + + +subsubsection {* Examples *} + +text {* + Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's + object-logics as a model for your own developments. For example, + see @{verbatim "src/FOL/IsaMakefile"}. The Isabelle @{tool_ref + mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation + of @{tool usedir} as well. +*} + + +section {* Preparing Isabelle session documents + \label{sec:tool-document} *} + +text {* + The @{tool_def document} utility prepares logic session documents, + processing the sources both as provided by the user and generated by + Isabelle. Its usage is: +\begin{ttbox} +Usage: document [OPTIONS] [DIR] + + Options are: + -c cleanup -- be aggressive in removing old stuff + -n NAME specify document name (default 'document') + -o FORMAT specify output format: dvi (default), dvi.gz, ps, + ps.gz, pdf + -t TAGS specify tagged region markup + + Prepare the theory session document in DIR (default 'document') + producing the specified output format. +\end{ttbox} + This tool is usually run automatically as part of the corresponding + Isabelle batch process, provided document preparation has been + enabled (cf.\ the @{verbatim "-d"} option of the @{tool_ref usedir} + tool). It may be manually invoked on the generated browser + information document output as well, e.g.\ in case of errors + encountered in the batch run. + + \medskip The @{verbatim "-c"} option tells the @{tool document} tool + to dispose the document sources after successful operation. This is + the right thing to do for sources generated by an Isabelle process, + but take care of your files in manual document preparation! + + \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify + the final output file name and format, the default is ``@{verbatim + document.dvi}''. Note that the result will appear in the parent of + the target @{verbatim DIR}. + + \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret + tagged Isabelle command regions. Tags are specified as a comma + separated list of modifier/name pairs: ``@{verbatim "+"}@{text + foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim + "-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to + fold text tagged as @{text foo}. The builtin default is equivalent + to the tag specification ``@{verbatim + "/theory,/proof,/ML,+visible,-invisible"}''; see also the {\LaTeX} + macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and + @{verbatim "\\isafoldtag"}, in @{verbatim isabelle.sty}. + + \medskip Document preparation requires a properly setup ``@{verbatim + document}'' directory within the logic session sources. This + directory is supposed to contain all the files needed to produce the + final document --- apart from the actual theories which are + generated by Isabelle. + + \medskip For most practical purposes, the @{tool document} tool is + smart enough to create any of the specified output formats, taking + @{verbatim root.tex} supplied by the user as a starting point. This + even includes multiple runs of {\LaTeX} to accommodate references + and bibliographies (the latter assumes @{verbatim root.bib} within + the same directory). + + In more complex situations, a separate @{verbatim IsaMakefile} for + the document sources may be given instead. This should provide + targets for any admissible document format; these have to produce + corresponding output files named after @{verbatim root} as well, + e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}. + + \medskip When running the session, Isabelle copies the original + @{verbatim document} directory into its proper place within + @{verbatim ISABELLE_BROWSER_INFO} according to the session path. + Then, for any processed theory @{text A} some {\LaTeX} source is + generated and put there as @{text A}@{verbatim ".tex"}. + Furthermore, a list of all generated theory files is put into + @{verbatim session.tex}. Typically, the root {\LaTeX} file provided + by the user would include @{verbatim session.tex} to get a document + containing all the theories. + + The {\LaTeX} versions of the theories require some macros defined in + @{verbatim isabelle.sty} as distributed with Isabelle. Doing + @{verbatim "\\usepackage{isabelle}"} in @{verbatim root.tex} should + be fine; the underlying Isabelle @{tool latex} tool already includes + an appropriate path specification for {\TeX} inputs. + + If the text contains any references to Isabelle symbols (such as + @{verbatim "\\"}@{verbatim ""}) then @{verbatim + isabellesym.sty} should be included as well. This package contains + a standard set of {\LaTeX} macro definitions @{verbatim + "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim + "<"}@{text foo}@{verbatim ">"}, (see \appref{app:symbols} for a + complete list of predefined Isabelle symbols). Users may invent + further symbols as well, just by providing {\LaTeX} macros in a + similar fashion as in @{verbatim isabellesym.sty} of the + distribution. + + For proper setup of DVI and PDF documents (with hyperlinks and + bookmarks), we recommend to include @{verbatim pdfsetup.sty} as + well. + + \medskip As a final step of document preparation within Isabelle, + @{verbatim "isatool document -c"} is run on the resulting @{verbatim + document} directory. Thus the actual output document is built and + installed in its proper place (as linked by the session's @{verbatim + index.html} if option @{verbatim "-i"} of @{tool_ref usedir} has + been enabled, cf.\ \secref{sec:info}). The generated sources are + deleted after successful run of {\LaTeX} and friends. Note that a + separate copy of the sources may be retained by passing an option + @{verbatim "-D"} to the @{tool usedir} utility when running the + session. +*} + + +section {* Running {\LaTeX} within the Isabelle environment + \label{sec:tool-latex} *} + +text {* + The @{tool_def latex} utility provides the basic interface for + Isabelle document preparation. Its usage is: +\begin{ttbox} +Usage: latex [OPTIONS] [FILE] + + Options are: + -o FORMAT specify output format: dvi (default), dvi.gz, ps, + ps.gz, pdf, bbl, idx, sty, syms + + Run LaTeX (and related tools) on FILE (default root.tex), + producing the specified output format. +\end{ttbox} + + Appropriate {\LaTeX}-related programs are run on the input file, + according to the given output format: @{executable latex}, + @{executable pdflatex}, @{executable dvips}, @{executable bibtex} + (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim + idx}). The actual commands are determined from the settings + environment (@{setting ISABELLE_LATEX} etc.). + + The @{verbatim sty} output format causes the Isabelle style files to + be updated from the distribution. This is useful in special + situations where the document sources are to be processed another + time by separate tools (cf.\ option @{verbatim "-D"} of the @{tool + usedir} utility). + + The @{verbatim syms} output is for internal use; it generates lists + of symbols that are available without loading additional {\LaTeX} + packages. +*} + + +subsubsection {* Examples *} + +text {* + Invoking @{verbatim "isatool latex"} by hand may be occasionally + useful when debugging failed attempts of the automatic document + preparation stage of batch-mode Isabelle. The abortive process + leaves the sources at a certain place within @{setting + ISABELLE_BROWSER_INFO}, see the runtime error message for details. + This enables users to inspect {\LaTeX} runs in further detail, e.g.\ + like this: +\begin{ttbox} + cd ~/isabelle/browser_info/HOL/Test/document + isatool latex -o pdf +\end{ttbox} +*} + +end \ No newline at end of file diff -r 889e5b7e006c -r ca9fdab0f971 doc-src/System/Thy/ROOT.ML --- a/doc-src/System/Thy/ROOT.ML Mon Sep 15 17:32:12 2008 +0200 +++ b/doc-src/System/Thy/ROOT.ML Mon Sep 15 19:42:22 2008 +0200 @@ -5,3 +5,4 @@ use "../../antiquote_setup.ML"; use_thy "Basics"; +use_thy "Presentation"; diff -r 889e5b7e006c -r ca9fdab0f971 doc-src/System/present.tex --- a/doc-src/System/present.tex Mon Sep 15 17:32:12 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,647 +0,0 @@ - -%% $Id$ - -\chapter{Presenting theories}\label{ch:present} - -Isabelle provides several ways to present the outcome of formal developments, -including WWW-based browsable libraries or actual printable documents. -Presentation is centered around the concept of \emph{logic sessions}. The -global session structure is that of a tree, with Isabelle Pure at its root, -further object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and -application sessions in leaf positions (usually without a separate image). - -The \texttt{mkdir} (see \S\ref{sec:tool-mkdir}) and \texttt{make} (see -\S\ref{sec:tool-make}) tools of Isabelle provide the primary means for -managing Isabelle sessions, including proper setup for presentation. Here the -\texttt{usedir} (see \S\ref{sec:tool-usedir}) tool takes care to let the -\texttt{isabelle} process run any additional stages required for document -preparation, notably the tools \texttt{document} (see -\S\ref{sec:tool-document}) and \texttt{latex} (see \S\ref{sec:tool-latex}). -The complete tool chain for managing batch-mode Isabelle sessions is -illustrated in figure~\ref{fig:session-tools}. - -\begin{figure}[htbp] - \begin{center} - \begin{tabular}{lp{0.6\textwidth}} - \texttt{isatool mkdir} & invoked once by the user to create the initial - source setup (common \texttt{IsaMakefile} plus a single session directory); \\ - \texttt{isatool make} & invoked repeatedly by the user to - keep session output up-to-date (HTML, documents etc.); \\ - \texttt{isatool usedir} & part of the standard \texttt{IsaMakefile} entry of a session; \\ - \texttt{isabelle} & run through \texttt{isatool usedir}; \\ - \texttt{isatool document} & run by the Isabelle process if document preparation is enabled; \\ - \texttt{isatool latex} & universal {\LaTeX} tool wrapper invoked multiple times - by \texttt{isatool document}; also useful for manual experiments; \\ - \end{tabular} - \caption{The tool chain of Isabelle session presentation} - \label{fig:session-tools} - \end{center} -\end{figure} - - -\section{Generating theory browser information} \label{sec:info} -\index{theory browsing information|bold} - -As a side-effect of running a logic sessions, Isabelle is able to generate -theory browsing information, including HTML documents that show a theory's -definition, the theorems proved in its ML file and the relationship with its -ancestors and descendants. Besides the HTML file that is generated for every -theory, Isabelle stores links to all theories in an index file. These indexes -are linked with other indexes to represent the overall tree structure of logic -sessions. - -Isabelle also generates graph files that represent the theory hierarchy of a -logic. There is a graph browser Java applet embedded in the generated HTML -pages, and also a stand-alone application that allows browsing theory graphs -without having to start a WWW client first. The latter version also includes -features such as generating Postscript files, which are not available in the -applet version. See \S\ref{sec:browse} for further information. - -\medskip - -The easiest way to let Isabelle generate theory browsing information for -existing sessions is to append ``\texttt{-i true}'' to the -\settdx{ISABELLE_USEDIR_OPTIONS} before invoking \texttt{isatool make} (or -\texttt{./build} in the distribution). For example, add something like this -to your Isabelle settings file -\begin{ttbox} -ISABELLE_USEDIR_OPTIONS="-i true" -\end{ttbox} -and then change into the \texttt{src/FOL} directory of the Isabelle -distribution and run \texttt{isatool make}, or even \texttt{isatool make all}. -The presentation output will appear in \texttt{\$ISABELLE_BROWSER_INFO/FOL}, -which usually refers to \verb,~/isabelle/browser_info/FOL,. Note that option -\texttt{-v true} will make the internal runs of \texttt{usedir} more explicit -about such details. - -Many standard Isabelle sessions (such as \texttt{HOL/ex}) also provide actual -printable documents. These are prepared automatically as well if enabled like -this, using the \texttt{-d} option -\begin{ttbox} -ISABELLE_USEDIR_OPTIONS="-i true -d dvi" -\end{ttbox} -Enabling options \texttt{-i} and \texttt{-d} simultaneausly as shown above -causes an appropriate ``document'' link to be included in the HTML index. -Documents (or raw document sources) may be generated independently of browser -information as well, see \S\ref{sec:tool-document} for further details. - -\bigskip The theory browsing information is stored in a sub-directory -directory determined by the \settdx{ISABELLE_BROWSER_INFO} setting plus a -prefix corresponding to the session identifier (according to the tree -structure of sub-sessions by default). A complete WWW view of all standard -object-logics and examples of the Isabelle distribution is available at the -Cambridge or Munich Isabelle sites: -\begin{center}\small - \begin{tabular}{l} - \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ - \url{http://isabelle.in.tum.de/library/} \\ - \end{tabular} -\end{center} - -\medskip In order to present your own theories on the web, simply copy the -corresponding subdirectory from \texttt{ISABELLE_BROWSER_INFO} to your WWW -server, having generated browser info like this: -\begin{ttbox} -isatool usedir -i true HOL Foo -\end{ttbox} -This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file -to load all your theories, and HOL is your parent logic image (\texttt{isatool - mkdir} assists in setting up Isabelle session directories, see -\S\ref{sec:tool-mkdir}). Theory browser information for HOL should have been -generated already beforehand. Alternatively, one may specify an external link -to an existing body of HTML data by giving \texttt{usedir} a \texttt{-P} -option like this: -\begin{ttbox} -isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo -\end{ttbox} - -\medskip For production use, the \texttt{usedir} tool is usually invoked in an -appropriate \texttt{IsaMakefile}, via the Isabelle \texttt{make} utility. -There is a separate \texttt{mkdir} tool to provide easy setup of all this, -with only minimal manual editing required. -\begin{ttbox} -isatool mkdir HOL Foo && isatool make -\end{ttbox} -See \S\ref{sec:tool-mkdir} for more information on preparing Isabelle session -directories, including the setup for documents. - - -\section{Browsing theory graphs} \label{sec:browse} -\index{theory graph browser|bold} - -The Isabelle graph browser is a general tool for visualizing dependency -graphs. Certain nodes of the graph (i.e.~theories) can be grouped together in -``directories'', whose contents may be hidden, thus enabling the user to -collapse irrelevant portions of information. The browser is written in Java, -it can be used both as a stand-alone application and as an applet. Note that -the option \texttt{-g} of \texttt{isatool usedir} (see -\S\ref{sec:tool-usedir}) creates graph presentations in batch mode for -inclusion in session documents. - - -\subsection{Invoking the graph browser} - -The stand-alone version of the graph browser is wrapped up as an -Isabelle tool called \tooldx{browser}: -\begin{ttbox} -Usage: browser [OPTIONS] [GRAPHFILE] - - Options are: - -c cleanup -- remove GRAPHFILE after use - -o FILE output to FILE (ps, eps, pdf) -\end{ttbox} -When no filename is specified, the browser automatically changes to the -directory \texttt{ISABELLE_BROWSER_INFO}. - -\medskip The \texttt{-c} option causes the input file to be removed after use. - -The \texttt{-o} option indicates batch-mode operation, with the output written -to the indicated file; note that \texttt{pdf} produces an \texttt{eps} copy as -well. - -\medskip The applet version of the browser is part of the standard WWW theory -presentation, see the link ``theory dependencies'' within each session index. - - -\subsection{Using the graph browser} - -The browser's main window, which is shown in figure -\ref{fig:browserwindow}, consists of two sub-windows: In the left -sub-window, the directory tree is displayed. The graph itself is -displayed in the right sub-window. -\begin{figure}[ht] - \includegraphics[width=\textwidth]{browser_screenshot} - \caption{\label{fig:browserwindow} Browser main window} -\end{figure} - - -\subsubsection*{The directory tree window} - -We describe the usage of the directory browser and the meaning of the -different items in the browser window. -\begin{itemize} - -\item A red arrow before a directory name indicates that the directory - is currently ``folded'', i.e.~the nodes in this directory are - collapsed to one single node. In the right sub-window, the names of - nodes corresponding to folded directories are enclosed in square - brackets and displayed in red color. - -\item A green downward arrow before a directory name indicates that - the directory is currently ``unfolded''. It can be folded by - clicking on the directory name. Clicking on the name for a second - time unfolds the directory again. Alternatively, a directory can - also be unfolded by clicking on the corresponding node in the right - sub-window. - -\item Blue arrows stand before ordinary node names. When clicking on such a - name (i.e.\ that of a theory), the graph display window focuses to the - corresponding node. Double clicking invokes a text viewer window in which - the contents of the theory file are displayed. - -\end{itemize} - - -\subsubsection*{The graph display window} - -When pointing on an ordinary node, an upward and a downward arrow is -shown. Initially, both of these arrows are green. Clicking on the -upward or downward arrow collapses all predecessor or successor nodes, -respectively. The arrow's color then changes to red, indicating that -the predecessor or successor nodes are currently collapsed. The node -corresponding to the collapsed nodes has the name ``{\tt [....]}''. To -uncollapse the nodes again, simply click on the red arrow or on the -node with the name ``{\tt [....]}''. Similar to the directory browser, -the contents of theory files can be displayed by double clicking on -the corresponding node. - - -\subsubsection*{The ``File'' menu} - -Please note that due to Java security restrictions this menu is not -available in the applet version. The meaning of the menu items is as -follows: -\begin{description} - -\item[Open \dots] Open a new graph file. - -\item[Export to PostScript] Outputs the current graph in Postscript format, - appropriately scaled to fit on one single sheet of A4 paper. The resulting - file can be printed directly. - -\item[Export to EPS] Outputs the current graph in Encapsulated Postscript - format. The resulting file can be included in other documents. - -\item[Quit] Quit the graph browser. - -\end{description} - - -\subsection*{*Syntax of graph definition files} - -A graph definition file has the following syntax: -\begin{eqnarray*} - \mbox{\it graph} & = & \{ \: \mbox{\it vertex \tt ;} \: \} ^ + \\ - vertex & = & \mbox{\it vertexname} \: \mbox{\it vertexID} \: \mbox{\it dirname} \: [ \mbox{\tt +} ] - \: \mbox{\it path} \: [ \mbox{\tt <} | \mbox{\tt >} ] \: \{ \: \mbox{\it vertexID} \: \} ^ * -\end{eqnarray*} - -The meaning of the items in a vertex description is as follows: -\begin{description} - -\item[vertexname] The name of the vertex. - -\item[vertexID] The vertex identifier. Note that there may be two - vertices with equal names, whereas identifiers must be unique. - -\item[dirname] The name of the ``directory'' the vertex should be - placed in. A ``{\tt +}'' sign after {\it dirname} indicates that - the nodes in the directory are initially visible. Directories are - initially invisible by default. - -\item[path] The path of the corresponding theory file. This is - specified relatively to the path of the graph definition file. - -\item[List of successor/predecessor nodes] A ``{\tt <}'' sign before - the list means that successor nodes are listed, a ``{\tt >}'' sign - means that predecessor nodes are listed. If neither ``{\tt <}'' nor - ``{\tt >}'' is found, the browser assumes that successor nodes are - listed. - -\end{description} - - -\section{Creating Isabelle session directories --- \texttt{isatool mkdir}} -\label{sec:tool-mkdir} - -The \tooldx{mkdir} utility prepares Isabelle session source directories, -including a sensible default setup of \texttt{IsaMakefile}, \texttt{ROOT.ML}, -and a \texttt{document} directory with a minimal \texttt{root.tex} that is -sufficient to print all theories of the session (in the order of appearance); -see \S\ref{sec:tool-document} for further information on Isabelle document -preparation. The usage of \texttt{isatool mkdir} is: -\begin{ttbox} -Usage: mkdir [OPTIONS] [LOGIC] NAME - - Options are: - -I FILE alternative IsaMakefile output - -P include parent logic target - -b setup build mode (session outputs heap image) - -q quiet mode - - Prepare session directory, including IsaMakefile and document source, - with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC) -\end{ttbox} - -The \texttt{mkdir} tool is conservative in the sense that any existing -\texttt{IsaMakefile} etc.\ is left unchanged. Thus it is safe to invoke it -multiple times, although later runs may not have the desired effect. - -Note that \texttt{mkdir} is unable to change \texttt{IsaMakefile} -incrementally --- manual changes are required for multiple sub-sessions. On -order to get an initial working session, the only editing needed is to add -appropriate \texttt{use_thy} calls to the generated \texttt{ROOT.ML} file. - - -\subsection*{Options} - -The \texttt{-I} option specifies an alternative to \texttt{IsaMakefile} for -dependencies. Note that ``\texttt{-}'' refers to \emph{stdout}, i.e.\ -``\texttt{-I-}'' provides an easy way to peek at \texttt{mkdir}'s idea of -\texttt{make} setup required for some particular of Isabelle session. - -\medskip The \texttt{-P} option includes a target for the parent -\texttt{LOGIC} session in the generated \texttt{IsaMakefile}. The -corresponding sources are assumed to be located within the Isabelle -distribution. - -\medskip The \texttt{-b} option sets up the current directory as the base for -a new session that provides an actual logic image, as opposed to one that only -runs several theories based on an existing image. Note that in the latter -case, everything except \texttt{IsaMakefile} would be placed into a separate -directory \texttt{NAME}, rather than the current one. See -\S\ref{sec:tool-usedir} for further information on \emph{build mode} vs.\ -\emph{example mode} of the \texttt{usedir} utility. - -\medskip The \texttt{-q} enables quiet mode, suppressing further notes on how -to proceed. - - -\subsection*{Examples} - -The standard setup of a single ``example session'' based on the default logic, -with proper document generation is generated like this: -\begin{ttbox} -isatool mkdir Foo && isatool make -\end{ttbox} -\noindent The theory sources should be put into the \texttt{Foo} directory, and its -\texttt{ROOT.ML} should be edited to load all required theories. Invoking -\texttt{isatool make} again would run the whole session, generating browser -information and the document automatically. The \texttt{IsaMakefile} is -typically tuned manually later, e.g.\ adding source dependencies, or changing -the options passed to \texttt{usedir}. - -\medskip Large projects may demand further sessions, potentially with separate -logic images being created. This usually requires manual editing of the -generated \texttt{IsaMakefile}, which is meant to cover all of the sub-session -directories at the same time (this is the deeper reasong why -\texttt{IsaMakefile} is not made part of the initial session directory created -by \texttt{isatool mkdir}). See \texttt{src/HOL/IsaMakefile} of the Isabelle -distribution for a full-blown example. - - -\section{Running Isabelle sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir} - -The \tooldx{usedir} utility builds object-logic images, or runs example -sessions based on existing logics. Its usage is: -\begin{ttbox} - -Usage: usedir [OPTIONS] LOGIC NAME - - Options are: - -C BOOL copy existing document directory to -D PATH (default true) - -D PATH dump generated document sources into PATH - -M MAX multithreading: maximum number of worker threads (default 1) - -P PATH set path for remote theory browsing information - -T LEVEL multithreading: trace level (default 0) - -V VERSION declare alternative document VERSION - -b build mode (output heap image, using current dir) - -c BOOL tell ML system to compress output image (default true) - -d FORMAT build document as FORMAT (default false) - -f NAME use ML file NAME (default ROOT.ML) - -g BOOL generate session graph image for document (default false) - -i BOOL generate theory browser information (default false) - -m MODE add print mode for output - -p LEVEL set level of detail for proof objects - -r reset session path - -s NAME override session NAME - -v BOOL be verbose (default false) - - Build object-logic or run examples. Also creates browsing - information (HTML etc.) according to settings. - - ISABELLE_USEDIR_OPTIONS= - HOL_USEDIR_OPTIONS= -\end{ttbox} - -Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is -implicitly prefixed to \emph{any} \texttt{usedir} call. Since the -\ttindex{IsaMakefile}s of all object-logics distributed with Isabelle just -invoke \texttt{usedir} for the real work, one may control compilation options -globally via above variable. In particular, generation of \rmindex{HTML} -browsing information and document preparation is controlled here. - -The \settdx{HOL_USEDIR_OPTIONS} setting is specific to the main -Isabelle/HOL image; its value is appended to -\verb,ISABELLE_USEDIR_OPTIONS, for that particular session only. - - -\subsection*{Options} - -Basically, there are two different modes of operation: \emph{build mode} -(enabled through the \texttt{-b} option) and \emph{example mode} (default). - -Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with input -image \texttt{LOGIC} and output to \texttt{NAME}, as provided on the command -line. This will be a batch session, running \texttt{ROOT.ML} from the current -directory and then quitting. It is assumed that \texttt{ROOT.ML} contains all -{\ML} commands required to build the logic. - -In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC} -and automatically runs \texttt{ROOT.ML} from within directory \texttt{NAME}. -It assumes that this file contains appropriate {\ML} commands to run the -desired examples. - -\medskip The \texttt{-i} option controls theory browser data generation. It -may be explicitly turned on or off --- as usual, the last occurrence of -\texttt{-i} on the command line wins. - -The \texttt{-P} option specifies a path (or actual URL) to be prefixed to any -\emph{non-local} reference of existing theories. Thus user sessions may -easily link to existing Isabelle libraries already present on the WWW. - -The \texttt{-m} options specifies additional print modes to be activated -temporarily while the session is processed. - -\medskip The \texttt{-d} option controls document preparation. Valid -arguments are \texttt{false} (do not prepare any document; this is default), -or any of \texttt{dvi}, \texttt{dvi.gz}, \texttt{ps}, \texttt{ps.gz}, -\texttt{pdf}. The logic session has to provide a properly setup -\texttt{document} directory. See \S\ref{sec:tool-document} and -\S\ref{sec:tool-latex} for more details. - -\medskip The \texttt{-V} option declares alternative document versions, -consisting of name/tags pairs (cf.\ options \texttt{-n} and \texttt{-t} of the -\texttt{document} tool, \S\ref{sec:tool-document}). The standard document is -equivalent to ``\texttt{document=theory,proof,ML}'', which means that all -theory begin/end commands, proof body texts, and ML code will be presented -faithfully. An alternative version ``\texttt{outline=/proof/ML}'' would fold -proof and ML parts, replacing the original text by a short place-holder. The -form ``$name$\verb,=-,'' means to remove document $name$ from the list of -versions to be processed. Any number of \texttt{-V} options may be given; -later declarations have precedence over earlier ones. - -\medskip The \texttt{-g} option produces images of the theory dependency graph -(cf.\ \S\ref{sec:browse}) for inclusion in the generated document, both as -\texttt{session_graph.eps} and \texttt{session_graph.pdf} at the same time. -To include this in the final {\LaTeX} document one could say -\verb,\includegraphics{session_graph}, in \texttt{document/root.tex} (omitting -the file-name extension enables {\LaTeX} to select to correct version, either -for the DVI or PDF output path). - -\medskip The \texttt{-D} option causes the generated document sources to be -dumped at location \texttt{PATH}; this path is relative to the session's main -directory. If the \texttt{-C} option is true, this will include a copy of an -existing \texttt{document} directory as provided by the user. For example, -\texttt{isatool usedir -D generated HOL Foo} produces a complete set of -document sources at \texttt{Foo/generated}. Subsequent invocation of -\texttt{isatool document Foo/generated} (see also \S\ref{sec:tool-document}) -will process the final result independently of an Isabelle job. This -decoupled mode of operation facilitates debugging of serious {\LaTeX} errors, -for example. - -\medskip The \texttt{-p} option determines the level of detail for internal -proof objects, see also the \emph{Isabelle Reference - Manual}~\cite{isabelle-ref}. - -\medskip The \texttt{-v} option causes additional information to be printed -while running the session, notably the location of prepared documents. - -\medskip The \texttt{-M} option specifies the maximum number of -parallel threads used for processing independent theory files -(multithreading only works on suitable ML platforms). The special -value of ``\texttt{0}'' or ``\texttt{max}'' refers to the number of -actual CPU cores of the underlying machine, which is a good starting -point for optimal performance tuning. The \texttt{-T} option -determines the level of detail in tracing output concerning the -internal locking and scheduling in multithreaded operation. This may -be helpful in isolating performance bottle-necks, e.g.\ due to -excessive wait states when locking critical code sections. - -\medskip Any \texttt{usedir} session is named by some \emph{session - identifier}. These accumulate, documenting the way sessions depend on -others. For example, consider \texttt{Pure/FOL/ex}, which refers to the -examples of FOL, which in turn is built upon Pure. - -The current session's identifier is by default just the base name of the -\texttt{LOGIC} argument (in build mode), or of the \texttt{NAME} argument (in -example mode). This may be overridden explicitly via the \texttt{-s} option. - - -\subsection*{Examples} - -Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's -object-logics as a model for your own developments. For example, see -\texttt{src/FOL/IsaMakefile}. The Isabelle \texttt{mkdir} tool (see -\S\ref{sec:tool-mkdir}) creates \texttt{IsaMakefile}s with proper invocation -of \texttt{usedir} as well. - - -\section{Preparing Isabelle session documents --- \texttt{isatool document}} -\label{sec:tool-document} - -The \tooldx{document} utility prepares logic session documents, processing the -sources both as provided by the user and generated by Isabelle. Its usage is: -\begin{ttbox} -Usage: document [OPTIONS] [DIR] - - Options are: - -c cleanup -- be aggressive in removing old stuff - -n NAME specify document name (default 'document') - -o FORMAT specify output format: dvi (default), dvi.gz, ps, - ps.gz, pdf - -t TAGS specify tagged region markup - - Prepare the theory session document in DIR (default 'document') - producing the specified output format. -\end{ttbox} -This tool is usually run automatically as part of the corresponding Isabelle -batch process, provided document preparation has been enabled (cf.\ the -\texttt{-d} option of the \texttt{usedir} utility, \S\ref{sec:tool-usedir}). -It may be manually invoked on the generated browser information document -output as well, e.g.\ in case of errors encountered in the batch run. - -\medskip The \texttt{-c} option tells the \texttt{document} tool to dispose -the document sources after successful operation. This is the right thing to -do for sources generated by an Isabelle process, but take care of your files -in manual document preparation! - -\medskip The \texttt{-n} and \texttt{-o} option specify the final output file -name and format, the default is ``\texttt{document.dvi}''. Note that the -result will appear in the parent of the target \texttt{DIR}. - -\medskip The \texttt{-t} option tells {\LaTeX} how to interpret tagged -Isabelle command regions. Tags are specified as a comma separated list of -modifier/name pairs: ``\verb,+,$foo$'' (or just ``$foo$'') means to keep, -``\verb,-,$foo$'' to drop, and ``\verb,/,$foo$'' to fold text tagged as $foo$. -The builtin default is equivalent to the tag specification -``\texttt{/theory,/proof,/ML,+visible,-invisible}''; see also the {\LaTeX} -macros \verb,\isakeeptag,, \verb,\isadroptag,, and \verb,\isafoldtag, in -\texttt{isabelle.sty}. - -\medskip Document preparation requires a properly setup ``\texttt{document}'' -directory within the logic session sources. This directory is supposed to -contain all the files needed to produce the final document --- apart from the -actual theories which are generated by Isabelle. - -\medskip For most practical purposes, the \texttt{document} tool is smart -enough to create any of the specified output formats, taking \texttt{root.tex} -supplied by the user as a starting point. This even includes multiple runs of -{\LaTeX} to accommodate references and bibliographies (the latter assumes -\texttt{root.bib} within the same directory). - -In more complex situations, a separate \texttt{IsaMakefile} for the document -sources may be given instead. This should provide targets for any admissible -document format; these have to produce corresponding output files named after -\texttt{root} as well, e.g.\ \texttt{root.dvi} for target format \texttt{dvi}. - -\medskip When running the session, Isabelle copies the original -\texttt{document} directory into its proper place within -\texttt{ISABELLE_BROWSER_INFO} according to the session path. Then, for any -processed theory $A$ some {\LaTeX} source is generated and put there as -$A$\texttt{.tex}. Furthermore, a list of all generated theory files is put -into \texttt{session.tex}. Typically, the root {\LaTeX} file provided by the -user would include \texttt{session.tex} to get a document containing all the -theories. - -The {\LaTeX} versions of the theories require some macros defined in -\texttt{isabelle.sty} as distributed with Isabelle. Doing -\verb,\usepackage{isabelle}, in \texttt{root.tex} should be fine; the -underlying Isabelle \texttt{latex} utility already includes an appropriate -{\TeX} inputs path. - -If the text contains any references to Isabelle symbols (such as -\verb,\,) then \texttt{isabellesym.sty} should be included as well. -This package contains a standard set of {\LaTeX} macro definitions -\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see -Appendix~\ref{app:symbols} for a complete list of predefined Isabelle -symbols). Users may invent further symbols as well, just by providing -{\LaTeX} macros in a similar fashion as in \texttt{isabellesym.sty} of the -distribution. - -For proper setup of PDF documents (with hyperlinks and bookmarks), we -recommend to include \verb,pdfsetup.sty, as well. It is safe to do so -even without using PDF~\LaTeX. - -\medskip As a final step of document preparation within Isabelle, -\texttt{isatool document -c} is run on the resulting \texttt{document} -directory. Thus the actual output document is built and installed in its -proper place (as linked by the session's \texttt{index.html} if option -\texttt{-i} of \texttt{usedir} has been enabled, cf.\ \S\ref{sec:info}). The -generated sources are deleted after successful run of {\LaTeX} and friends. -Note that a separate copy of the sources may be retained by passing an option -\texttt{-D} to the \texttt{usedir} utility when running the session (see also -\S\ref{sec:tool-usedir}). - - -\section{Running {\LaTeX} within the Isabelle environment --- \texttt{isatool latex}} -\label{sec:tool-latex} - -The \tooldx{latex} utility provides the basic interface for Isabelle document -preparation. Its usage is: -\begin{ttbox} -Usage: latex [OPTIONS] [FILE] - - Options are: - -o FORMAT specify output format: dvi (default), dvi.gz, ps, - ps.gz, pdf, bbl, idx, sty, syms - - Run LaTeX (and related tools) on FILE (default root.tex), - producing the specified output format. -\end{ttbox} -Appropriate {\LaTeX}-related programs are run on the input file, -according to the given output format: \texttt{latex}, -\texttt{pdflatex}, \texttt{dvips}, \texttt{bibtex} (for \texttt{bbl}), -and \texttt{makeindex} (for \texttt{idx}). The actual commands are -determined from the settings environment (\texttt{ISABELLE_LATEX} -etc., see \S\ref{sec:settings}). - -The \texttt{sty} output format causes the Isabelle style files to be updated -from the distribution. This is useful in special situations where the -document sources are to be processed another time by separate tools (cf.\ -option \texttt{-D} of the \texttt{usedir} utility, see -\S\ref{sec:tool-usedir}). - -The \texttt{syms} output is for internal use; it generates lists of symbols -that are available without loading additional {\LaTeX} packages. - - -\subsubsection*{Examples} - -Invoking \texttt{isatool latex} by hand may be occasionally useful when -debugging failed attempts of the automatic document preparation stage of -batch-mode Isabelle. The abortive process leaves the sources at a certain -place within \texttt{ISABELLE_BROWSER_INFO}, see the runtime error message for -details. This enables users to inspect {\LaTeX} runs in further detail, e.g.\ -like this: - -\begin{ttbox} - cd ~/isabelle/browser_info/HOL/Test/document - isatool latex -o pdf -\end{ttbox} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "system" -%%% End: diff -r 889e5b7e006c -r ca9fdab0f971 doc-src/System/system.tex --- a/doc-src/System/system.tex Mon Sep 15 17:32:12 2008 +0200 +++ b/doc-src/System/system.tex Mon Sep 15 19:42:22 2008 +0200 @@ -26,7 +26,7 @@ \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual} \author{\emph{Makarius Wenzel} and \emph{Stefan Berghofer} \\ - TU M\"unchen} + TU München} \makeindex @@ -37,7 +37,7 @@ \pagenumbering{roman} \tableofcontents \clearfirst \input{Thy/document/Basics} -\input{present} +\input{Thy/document/Presentation} \input{misc} \appendix