--- 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"