--- 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
--- 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
--- /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 "<forall>"}) 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
--- 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";
--- 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,\<forall>,) 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:
--- 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