diff -r 52e4de17734e -r f9d3c92eae4d doc-src/System/present.tex --- a/doc-src/System/present.tex Tue Dec 11 15:04:17 2001 +0100 +++ b/doc-src/System/present.tex Tue Dec 11 15:36:28 2001 +0100 @@ -6,21 +6,40 @@ 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 \texttt{Pure} at its -root, further object-logics derived (e.g.\ \texttt{HOLCF} from \texttt{HOL}, -and \texttt{HOL} from \texttt{Pure}), and application sessions in leaf -positions. The latter usually do not have a separate {\ML} image. +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 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}). +\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 browsing information} \label{sec:info} +\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 @@ -34,36 +53,44 @@ 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 browser first. The latter version also includes +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 -In order to let Isabelle generate theory browsing information, 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 this to your -Isabelle settings file +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. -Some sessions (such as \texttt{HOL/Isar_examples}) even provide actual +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} -See \S\ref{sec:tool-document} for further information on Isabelle document -preparation. +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 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 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/} \\ @@ -71,31 +98,19 @@ \end{tabular} \end{center} -\medskip - -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}, -\ttindex{bind_thms} or \ttindex{store_thm} (see also \cite{isabelle-ref}). -Section headings may be included in the presentation via the {\ML} function -\begin{ttbox}\index{*section} -section: string -> unit -\end{ttbox} - -\medskip - -In order to present your own theories on the web, simply copy the +\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, after having generated browser info like this: +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. Ideally, -theory browser information would have been generated for HOL already. - -Alternatively, one may specify an external link to an existing body of HTML -data by giving \texttt{usedir} a \texttt{-P} option like this: +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} @@ -105,8 +120,7 @@ There is a separate \texttt{mkdir} tool to provide easy setup of all this, with only minimal manual editing required. \begin{ttbox} -isatool mkdir Foo -isatool make +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. @@ -115,11 +129,14 @@ \section{Browsing theory graphs} \label{sec:browse} \index{theory graph browser|bold} -The graph browser is a 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 filter out irrelevant -information. The browser is written in Java, it can be used both as a -stand-alone application and as an applet. +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} @@ -145,12 +162,12 @@ \subsection{Using the graph browser} The browser's main window, which is shown in figure -\ref{browserwindow}, consists of two sub-windows: In the left +\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{browserwindow} Browser main window} + \caption{\label{fig:browserwindow} Browser main window} \end{figure} @@ -205,7 +222,7 @@ \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 paper. The resulting + 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 @@ -250,115 +267,6 @@ \end{description} -\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 - -o FORMAT specify output format: dvi (default), dvi.gz, ps, - ps.gz, pdf - -v be verbose - - 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 session, -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. - -\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 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. - -If the text contains any references to Isabelle symbols (such as -\verb,\,) then \texttt{isabellesym.sty} should be included as well. -This package contains a standard set of {\LaTeX} macro definitions -\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see -Appendix~\ref{app:symbols} for a complete list). The user may refer to -further symbols as well, simply by providing {\LaTeX} macros of the same sort. - -For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail -images), 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, \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}). The generated sources are deleted after successful run -of {\LaTeX} and friends. Note that a 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, png, sty - - 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{thumbpdf} (for \texttt{png}). -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}). - -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{Creating Isabelle session directories --- \texttt{isatool mkdir}} \label{sec:tool-mkdir} @@ -367,7 +275,7 @@ and a \texttt{document} directory with a minimal \texttt{root.tex} that is sufficient 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{mkdir} is: +preparation. The usage of \texttt{isatool mkdir} is: \begin{ttbox} Usage: mkdir [OPTIONS] [LOGIC] NAME @@ -383,7 +291,7 @@ 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 -experimentally, with varying options. +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 @@ -420,16 +328,23 @@ 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 +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} would now run the whole session, generating browser +\texttt{isatool make} again would run the whole session, generating browser information and the document automatically. The \texttt{IsaMakefile} is -usually tuned manually later, e.g.\ adding actual source dependencies, or +typically tuned manually later, e.g.\ adding actual 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} @@ -445,6 +360,7 @@ -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) + -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 @@ -500,6 +416,14 @@ \texttt{document} directory. See \S\ref{sec:tool-document} and \S\ref{sec:tool-latex} for more details. +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. +In order to make this appear the final {\LaTeX} document one would typically +say \verb,\includegraphics{session_graph}, in the \texttt{document/root.tex} +file. (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}, which is relative to the session's main directory. For example, \texttt{-D document} would leave a copy of the @@ -533,6 +457,135 @@ \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 + -o FORMAT specify output format: dvi (default), dvi.gz, ps, + ps.gz, pdf + + 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 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}, somewhere in \texttt{root.tex} should work fine; +the underlying Isabelle \texttt{latex} utility already includes an appropriate +{\TeX} inputs path. + +If the text contains any references to Isabelle symbols (such as +\verb,\,) then \texttt{isabellesym.sty} should be included as well. +This package contains a standard set of {\LaTeX} macro definitions +\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see +Appendix~\ref{app:symbols} for a complete list of predefined Isabelle +symbols). Users may invent further symbols as well, just by providing +{\LaTeX} macros in a similar fashion as in \texttt{isabellesym.sty} of the +distribution. + +For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail +images), 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, png, sty + + 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{thumbpdf} (for \texttt{png}). +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}). + +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 the Isabelle settings like this: +\begin{ttbox} +TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS" +\end{ttbox} +This is known to work with \textsl{teTeX} (version 1.0 or later). + + +\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"