# HG changeset patch # User wenzelm # Date 939836359 -7200 # Node ID 29a2a1d71128f77182b2f293514eccb67153712e # Parent 6ddcc24038e183f5c35381235ce7682d1750c0ac updated; diff -r 6ddcc24038e1 -r 29a2a1d71128 doc-src/System/basics.tex --- a/doc-src/System/basics.tex Wed Oct 13 15:41:24 1999 +0200 +++ b/doc-src/System/basics.tex Wed Oct 13 19:39:19 1999 +0200 @@ -3,21 +3,21 @@ \chapter{Basic concepts} -The \emph{Isabelle System Manual} describes Isabelle together with -related tools and user interfaces as seen from an outside (operating -system oriented) view. See the \emph{Isabelle Reference Manual} for -all internal {\ML} level user commands, on the other hand. +The \emph{Isabelle System Manual} describes Isabelle together with related +tools and user interfaces as seen from an outside, operating system oriented +view. See the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} and the +\emph{Isabelle Isar Reference Manual}~\cite{isabelle-isar-ref} for the +internal user commands, on the other hand. -\medskip The Isabelle system level environment is based on a few -general concepts: +\medskip The Isabelle system environment is based on a few general elements: \begin{itemize} \item The \emph{Isabelle settings mechanism}, which provides environment variables to all Isabelle programs (including tools and user interfaces). -\item \emph{Isabelle proper} (\ttindex{isabelle}), which runs logic +\item \emph{Isabelle proper} (\ttindex{isabelle}), which invokes logic sessions, both interactively or in batch mode. In particular, - \texttt{isabelle} abstracts over the invocation of the actual {\ML} - system to be used. + \texttt{isabelle} abstracts over the invocation of the actual {\ML} system + to be used. \item The \emph{Isabelle tools wrapper} (\ttindex{isatool}), which provides a generic startup platform for Isabelle related utilities. Thus tools automatically benefit from the settings mechanism. @@ -84,11 +84,11 @@ sensible defaults for most variables. When installing the system, only a few of these have to be adapted (most likely \texttt{ML_SYSTEM} etc.). - -\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it - exists) is run the same way as the site default settings. The - variable \texttt{ISABELLE_HOME_USER} has already been set before --- - usually to \texttt{\~\relax/isabelle}. + +\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it exists) is + run the same way as the site default settings. Note that the variable + \texttt{ISABELLE_HOME_USER} has already been set before --- usually to + \texttt{\~\relax/isabelle}. Thus individual users may override the site-wide defaults. See also file \texttt{etc/user-settings.sample} in the distribution. @@ -186,6 +186,10 @@ options for object-logics --- \texttt{usedir} is the basic utility that builds them (cf.\ the \texttt{IsaMakefile}s in the distribution). + +\item[\settdx{ISABELLE_LATEX}, \settdx{ISABELLE_PDFLATEX}, + \settdx{ISABELLE_BIBTEX}, \settdx{ISABELLE_DVIPS}] refer to {\LaTeX} related + tools for Isabelle document preparation (see also \S\ref{sec:tool-latex}). \item[\settdx{ISABELLE_TOOLS}] is a colon separated list of directories that are scanned by \texttt{isatool} for utility @@ -238,12 +242,12 @@ If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system. \end{ttbox} Input files without path specifications are looked up in the -\texttt{ISABELLE_PATH} setting, which may consist of multiple -components separated by colons --- these are tried in order. -Likewise, base names are relative to the directory specified by -\texttt{ISABELLE_OUTPUT}. In any case, actual file locations may also -be given by including at least one \texttt{/} in the name (hint: use -\texttt{./} to refer to the current directory). +\texttt{ISABELLE_PATH} setting, which may consist of multiple components +separated by colons --- these are tried in order. Likewise, base names are +relative to the directory specified by \texttt{ISABELLE_OUTPUT}. In any case, +actual file locations may also be given by including at least one slash +(\texttt{/}) in the name (hint: use \texttt{./} to refer to the current +directory). \subsection*{Options} @@ -283,9 +287,8 @@ providing a pure batch mode facility. \medskip The \texttt{-I} option makes Isabelle enter Isar interaction mode on -startup, instead of the primitive {\ML} top-level. This flag is usually -enabled by default when running Isabelle via some user interface, but it is -\emph{not} for the basic \texttt{isabelle} program. +startup, instead of the primitive {\ML} top-level. Usually some user +interface (such Proof~General) takes care of this flag. \subsection*{Examples} @@ -317,13 +320,17 @@ isabelle -r Foo \end{ttbox} -\medskip The next example demonstrates batch execution of Isabelle. We -print a certain theorem of \texttt{FOL}: +\medskip Note that manual session management like this does \emph{not} provide +proper setup for theory presentation. This would require the \texttt{usedir} +utility, see \S\ref{sec:tool-usedir}. + +\bigskip The next example demonstrates batch execution of Isabelle. We print a +certain theorem of \texttt{FOL}: \begin{ttbox} isabelle -e "prth allE;" -q -r FOL \end{ttbox} -Note that the output text will be usually interspersed with some -garbage produced by the {\ML} compiler. +The output text will be usually interspersed with additional junk messages by +the {\ML} runtime environment. \section{The Isabelle tools wrapper --- \texttt{isatool}} \label{sec:isatool} @@ -362,48 +369,56 @@ way for end-users to invoke a certain interface; which one to start actually is determined by the \settdx{ISABELLE_INTERFACE} setting variable. -Basically, there are two ways to specify an interface: either by giving an -identifier that the Isabelle distribution knows about, or specifying an actual -path name (containing a slash ``\texttt{/}'') of some executable. Currently, -the following interface identifiers are recognized: -\begin{ttdescription} -\item[none] is just a pass-through to \texttt{isabelle}. Thus +An interface may be specified either by giving an identifier that the Isabelle +distribution knows about, or by specifying an actual path name (containing a +slash ``\texttt{/}'') of some executable. Currently, the following interfaces +are available: + +\begin{itemize} +\item \texttt{none} is just a pass-through to \texttt{isabelle}. Thus \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}. - -\item[xterm] refers to a simple xterm based interface which is part of + +\item \texttt{xterm} refers to a simple xterm based interface which is part of the Isabelle distribution. -\item[emacs] refers to David Aspinall's \emph{Isamode}\index{user +\item \texttt{emacs} refers to David Aspinall's \emph{Isamode}\index{user interface!Isamode} for emacs. Isabelle just provides a wrapper for this, the actual Isamode distribution is available elsewhere \cite{isamode}. -\end{ttdescription} + +\item Proof~General~\cite{proofgeneral}\index{user interface!Proof General} of + LFCS Edinburgh is distributed with separate interface wrapper scripts for + Isabelle. See below for more details. +\end{itemize} -The factory default for \texttt{ISABELLE_INTERFACE} is \texttt{xterm}. -This interface runs \texttt{isabelle} within its own xterm window. -Usually, display of mathematical symbols from the Isabelle font is -also enabled (see \S\ref{sec:tool-installfonts} for font configuration -issues). Furthermore, different kinds of identifiers in logical terms -are highlighted appropriately, e.g.\ free variables in bold and bound -variables underlined. - +The factory default for \texttt{ISABELLE_INTERFACE} is \texttt{xterm}. This +interface runs \texttt{isabelle} within its own \textsl{xterm} window. +Usually, display of mathematical symbols from the Isabelle font is also +enabled (see \S\ref{sec:tool-installfonts} for font configuration issues). +Furthermore, different kinds of identifiers in logical terms are highlighted +appropriately, e.g.\ free variables in bold and bound variables underlined. There are some more options available. Just pass \texttt{-?} to the \texttt{xterm} interface to have its usage printed. -\medskip - -Proof~General\index{user interface!Proof General} of LFCS Edinburgh is -another, much more advanced interface. It supports both classic Isabelle (as +\medskip Proof~General\index{user interface!Proof General} is a much more +advanced interface. It supports both classic Isabelle (as \texttt{ProofGeneral/isa}) and Isabelle/Isar (as \texttt{ProofGeneral/isar}). Note that the latter is slightly better supported, and more robust. -Proof~General already ships with appropriate executable scripts to be run as -Isabelle interface. Thus a typical setup of Proof~General for Isabelle/Isar -would be like this: + +Using the Isabelle interface wrapper scripts as provided by the Proof~General +distribution, a typical setup for Isabelle/Isar would be like this: \begin{ttbox} ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface -PROOFGENERAL_OPTIONS="-p emacs -u true" +PROOFGENERAL_OPTIONS="" \end{ttbox} -See \cite{proofgeneral} for more information on Proof~General. +Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of +the Proof~General Lisp packages. There are some options available, such as +\texttt{-l} for passing the logic image to be used. +\medskip Note that the world may be also seen the other way round: Emacs may +be started first (with proper Proof~General mode setup), before running +\texttt{isabelle} from within. This requires further Emacs Lisp +configuration, see the Proof~General documentation \cite{proofgeneral} for +more information. %%% Local Variables: %%% mode: latex diff -r 6ddcc24038e1 -r 29a2a1d71128 doc-src/System/fonts.tex --- a/doc-src/System/fonts.tex Wed Oct 13 15:41:24 1999 +0200 +++ b/doc-src/System/fonts.tex Wed Oct 13 19:39:19 1999 +0200 @@ -52,8 +52,7 @@ same machine. In this case, most X11 display servers should be happy by being told about the Isabelle fonts directory as follows: \begin{ttbox} -ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash" - +ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"%$ \end{ttbox} The same also works for remote X11 sessions in a somewhat homogeneous network, where any X11 display machine also mounts the Isabelle @@ -134,7 +133,6 @@ scripts are just left in plain \textsc{ascii}. Thus users with \textsc{ascii}-only facilities will still be able to read your files. - %%% Local Variables: %%% mode: latex %%% TeX-master: "system" diff -r 6ddcc24038e1 -r 29a2a1d71128 doc-src/System/misc.tex --- a/doc-src/System/misc.tex Wed Oct 13 15:41:24 1999 +0200 +++ b/doc-src/System/misc.tex Wed Oct 13 19:39:19 1999 +0200 @@ -210,84 +210,6 @@ \texttt{make} invocation. -\section{Running complete logics --- \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 LOGIC NAME - - Options are: - -B build mode with THIS_IS_ISABELLE_BUILD indication - -P PATH set path for remote theory browsing information - -b build mode (output heap image, using current dir) - -i BOOL generate theory browsing information, - i.e. HTML / graph data (default false) - -r reset session path - -s NAME override session NAME - - Build object-logic or run examples. Also creates browsing - information (HTML etc.) according to settings. - - ISABELLE_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 is enabled or -disabled this way. - - -\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. The \texttt{-B} option is like -\texttt{-b}, but also indicates \texttt{THIS_IS_ISABELLE_BUILD=true} via the -process environment. This usually causes the \texttt{ISABELLE\_OUTPUT} and -\texttt{ISABELLE_BROWSER_INFO} settings to refer to some location within the -Isabelle distribution directory, rather than the user's home directory. - -In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC} -(typically just built before) and automatically runs \texttt{ROOT.ML} from -within directory \texttt{NAME}. It assumes that file \texttt{ROOT.ML} in -directory \texttt{NAME} contains appropriate {\ML} commands to run the desired -examples. - -\medskip The \texttt{-i} option controls theory browsing data generation. It -may be explicitly turned on or off --- 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. - -\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 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 explicitely 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 developements. For example, see -\texttt{src/FOL/IsaMakefile}. - - %%% Local Variables: %%% mode: latex %%% TeX-master: "system" diff -r 6ddcc24038e1 -r 29a2a1d71128 doc-src/System/present.tex --- a/doc-src/System/present.tex Wed Oct 13 15:41:24 1999 +0200 +++ b/doc-src/System/present.tex Wed Oct 13 19:39:19 1999 +0200 @@ -3,15 +3,28 @@ \chapter{Presenting theories} +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 +structure of sessions is that of a tree, with Isabelle \texttt{Pure} at its +root, further derived object-logics (e.g.\ \texttt{HOLCF} from \texttt{HOL}, +and \texttt{HOL} from \texttt{Pure}), and application sessions at its leaves. +The latter usually do not have a separate {\ML} image. + +The \texttt{usedir} utility (see \S\ref{sec:tool-usedir}) provides the prime +means for managing Isabelle sessions, including proper setup for presentation. + + \section{Generating theory browsing information} \label{sec:info} \index{theory browsing information|bold} -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 -hierarchic structure of Isabelle's logics. +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 tree structure of Isabelle's +logics. 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 @@ -22,24 +35,31 @@ \medskip -To generate theory browsing information for logics that are part of the -Isabelle distribution, simply append ``\texttt{-i true}'' to the -\settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic. For example, -in order to do this for {\FOL}, first add something like this to your Isabelle -settings file +In order to let Isabelle generate theory browsing information for logics that +are part of the Isabelle distribution, simply append ``\texttt{-i true}'' to +the \settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic. For +example, in order to do this for {\FOL}, 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}. -\medskip +Some sessions (such as \texttt{HOL/Isar_examples}) even provide actual +printable documents. These are prepared automatically as well if enabled by +giving an appropriate \texttt{-d} option, e.g.\ +\begin{ttbox} +ISABELLE_USEDIR_OPTIONS="-i true -d dvi" +\end{ttbox} +See \S\ref{sec:tool-document} for further information on Isabelle document +preparation. -The theory browsing information is stored within the directory determined by -the \settdx{ISABELLE_BROWSER_INFO} setting. The \texttt{index.html} file -located there provides an entry point to all standard Isabelle logics. A -complete HTML version of all object-logics and examples of the Isabelle -distribution is available at +\bigskip The theory browsing information is stored within the directory +determined by the \settdx{ISABELLE_BROWSER_INFO} setting. The +\texttt{index.html} file located there provides an entry point to all standard +Isabelle logics. A complete HTML version of all object-logics and examples of +the Isabelle distribution is available at \begin{center}\small \begin{tabular}{l} \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ @@ -51,9 +71,9 @@ The generated HTML document of any theory includes all theorems proved in the corresponding {\ML} file, provided these have been stored properly via -\ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm}, or -\ttindex{store_thm}. Section headings may be included in the presentation via -the {\ML} function +\ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm}, +\ttindex{bind_thms} or \ttindex{store_thm}. Section headings may be included +in the presentation via the {\ML} function \begin{ttbox}\index{*section} section: string -> unit \end{ttbox} @@ -78,6 +98,7 @@ \end{ttbox} + \section{Browsing theory graphs} \label{sec:browse} \index{theory graph browser|bold} @@ -99,20 +120,20 @@ When no filename is specified, the browser automatically changes to the directory \texttt{ISABELLE_BROWSER_INFO/graph/data}. -\medskip The applet version of the browser can be invoked by opening -the {\tt index.html} file in the directory -\texttt{ISABELLE_BROWSER_INFO} from your Web browser and selecting -``version for Java capable browsers''. There is also a link to the -corresponding theory graph in every logic's {\tt index.html} file. +\medskip The applet version of the browser can be invoked by opening the {\tt + index.html} file in the directory \texttt{ISABELLE_BROWSER_INFO} from your +Web browser and selecting ``version for Java capable browsers''. There is +also a link to the corresponding theory graph in every logic's {\tt + index.html} file. \subsection{Using the graph browser} The browser's main window, which is shown in figure -\ref{browserwindow}, consists of two subwindows: In the left -subwindow, the directory tree is displayed. The graph itself is -displayed in the right subwindow. -\begin{figure}[h] +\ref{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{browserwindow} Browser main window} \end{figure} @@ -126,16 +147,16 @@ \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 subwindow, the names of + 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 colour. + 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 - subwindow. + sub-window. \item Blue arrows stand before ordinary node (i.e.~theory) names. When clicking on such a name, the graph display window focuses to the @@ -150,7 +171,7 @@ 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 colour then changes to red, indicating that +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 @@ -215,6 +236,181 @@ \end{description} +\section{Preparing Isabelle session documents --- \texttt{isatool document}} +\label{sec:tool-document} + +The \tooldx{document} utility prepares logic session documents, processing the +combined sources as provided by the user and generated by Isabelle. Its usage is: +\begin{ttbox} +Usage: document [OPTIONS] [DIR] + + Options are: + -o FORMAT specify output format: dvi (default), dvi.gz, ps, + ps.gz, pdf + + Prepare the theory session document in DIR (default '.') + producing the specified output format. +\end{ttbox} +This tool is usually run automatically as part of the corresponding session, +provided document preparation is 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. + +\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 actual document, apart from the +actual theories as generated by Isabelle. + +\medskip For simple documents, the \texttt{document} tool is smart enough to +create any of the 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). + +For complex documents, a separate \texttt{IsaMakefile} may be given instead. +It 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}, somewhere in \texttt{root.tex} should work fine; +the underlying Isabelle \texttt{latex} utility already includes an appropriate +{\TeX} inputs path. For proper setup of hyperlinks and bookmarks in PDF +documents we recommend to include \verb,pdfsetup.sty, as well.\footnote{It is + safe to do so even without using PDF~\LaTeX.} + +\medskip As a final step, \texttt{isatool document} 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}). Note that the generated sources are left as is. While +they may be safely deleted afterwards, this is \emph{not} done automatically. + + +\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, or bbl + + 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{bibtex}, +\texttt{dvips}. The actual commands are determined from the settings +environment (see \texttt{ISABELLE_LATEX} etc.). + +It is important to note that the {\LaTeX} inputs file space has to be properly +setup to include the Isabelle styles. Usually, this may be done by modifying +the \settdx{TEXINPUTS} variable in settings like this: +\begin{ttbox} +TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS" +\end{ttbox} +This is known to work with recent versions of the \textsl{teTeX} distribution. + + + +\section{Managing logic 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 LOGIC NAME + + Options are: + -B build mode with THIS_IS_ISABELLE_BUILD indication + -P PATH set path for remote theory browsing information + -b build mode (output heap image, using current dir) + -d FORMAT build document as FORMAT (default false) + -i BOOL generate theory browsing information, + i.e. HTML / graph data (default false) + -r reset session path + -s NAME override session NAME + + Build object-logic or run examples. Also creates browsing + information (HTML etc.) according to settings. + + ISABELLE_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 this way. + + +\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. The \texttt{-B} option is like +\texttt{-b}, but also indicates \texttt{THIS_IS_ISABELLE_BUILD=true} via the +process environment. This usually causes the \texttt{ISABELLE\_OUTPUT} and +\texttt{ISABELLE_BROWSER_INFO} settings to refer to some location within the +Isabelle distribution directory, rather than the user's home directory. + +In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC} +(typically just built before) and automatically runs \texttt{ROOT.ML} from +within directory \texttt{NAME}. It assumes that file \texttt{ROOT.ML} in +directory \texttt{NAME} contains appropriate {\ML} commands to run the desired +examples. + +\medskip The \texttt{-i} option controls theory browsing data generation. It +may be explicitly turned on or off --- 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. + +\medskip The \texttt{-d} option controls document preparation. Valid +arguments are \texttt{false} (do not prepare 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 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 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 explicitely 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}. + + %%% Local Variables: %%% mode: latex %%% TeX-master: "system" diff -r 6ddcc24038e1 -r 29a2a1d71128 doc-src/System/system.tex --- a/doc-src/System/system.tex Wed Oct 13 15:41:24 1999 +0200 +++ b/doc-src/System/system.tex Wed Oct 13 19:39:19 1999 +0200 @@ -26,9 +26,9 @@ \pagenumbering{roman} \tableofcontents \clearfirst \include{basics} -\include{misc} +\include{present} \include{fonts} -\include{present} +\include{misc} \begingroup \bibliographystyle{plain} \small\raggedright\frenchspacing