some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
%
\begin{isabellebody}%
\def\isabellecontext{Presentation}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Presentation\isanewline
\isakeyword{imports}\ Base\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Presenting theories \label{ch:present}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
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{sessions} (\chref{ch:session}). 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 further on in the hierarchy.
The tools \indexref{}{tool}{mkroot}\hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} and \indexref{}{tool}{build}\hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}} provide the
primary means for managing Isabelle sessions, including proper setup
for presentation; \hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}} takes care to have \indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} run any additional stages required for document
preparation, notably the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}} and \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatool{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}}
\indexref{}{tool}{mkroot}\hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} & invoked once by the user to initialize the
session \verb|ROOT| with optional \verb|document|
directory; \\
\indexref{}{tool}{build}\hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}} & invoked repeatedly by the user to keep
session output up-to-date (HTML, documents etc.); \\
\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} & run through \indexref{}{tool}{build}\hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}}; \\
\indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}} & run by the Isabelle process if document
preparation is enabled; \\
\indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}} & universal {\LaTeX} tool wrapper invoked
multiple times by \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\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}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Generating theory browser information \label{sec:info}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\index{theory browsing information|bold}
As a side-effect of building sessions, Isabelle is able to generate
theory browsing information, including HTML documents that show the
theory sources 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 the sessions.
Isabelle also generates graph files that represent the theory
dependencies within a session. 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 invoke \hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}} with suitable
options:
\begin{ttbox}
isabelle build -o browser_info -v -c FOL
\end{ttbox}
The presentation output will appear in \verb|$ISABELLE_BROWSER_INFO/FOL| as reported by the above verbose
invocation of the build process.
Many Isabelle sessions (such as \verb|HOL-Library| in \verb|~~/src/HOL/Library|) also provide actual printable documents.
These are prepared automatically as well if enabled like this:
\begin{ttbox}
isabelle build -o browser_info -o document=pdf -v -c HOL-Library
\end{ttbox}
Enabling both browser info and document preparation simultaneously
causes an appropriate ``document'' link to be included in the HTML
index. Documents 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 \indexref{}{setting}{ISABELLE\_BROWSER\_INFO}\hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}} setting plus a prefix corresponding to the
session identifier (according to the tree structure of sub-sessions
by default). In order to present Isabelle applications on the web,
the corresponding subdirectory from \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}
can be put on a WWW server.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Preparing session root directories \label{sec:tool-mkroot}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{mkroot}\hypertarget{tool.mkroot}{\hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}}} tool configures a given directory as
session root, with some \verb|ROOT| file and optional document
source directory. Its usage is:
\begin{ttbox}
Usage: isabelle mkroot [OPTIONS] [DIR]
Options are:
-d enable document preparation
-n NAME alternative session name (default: DIR base name)
Prepare session root DIR (default: current directory).
\end{ttbox}
The results are placed in the given directory \isa{dir}, which
refers to the current directory by default. The \hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} tool
is conservative in the sense that it does not overwrite existing
files or directories. Earlier attempts to generate a session root
need to be deleted manually.
\medskip Option \verb|-d| indicates that the session shall be
accompanied by a formal document, with \isa{dir}\verb|/document/root.tex| as its {\LaTeX} entry point (see also
\chref{ch:present}).
Option \verb|-n| allows to specify an alternative session
name; otherwise the base name of the given directory is used.
\medskip The implicit Isabelle settings variable \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LOGIC}}}} specifies the parent session, and \hyperlink{setting.ISABELLE-DOCUMENT-FORMAT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DOCUMENT{\isaliteral{5F}{\isacharunderscore}}FORMAT}}}} the document format to be filled filled
into the generated \verb|ROOT| file.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Examples%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Produce session \verb|Test| (with document preparation)
within a separate directory of the same name:
\begin{ttbox}
isabelle mkroot -d Test && isabelle build -D Test
\end{ttbox}
\medskip Upgrade the current directory into a session ROOT with
document preparation, and build it:
\begin{ttbox}
isabelle mkroot -d && isabelle build -D .
\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Preparing Isabelle session documents
\label{sec:tool-document}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{document}\hypertarget{tool.document}{\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}} tool prepares logic session
documents, processing the sources both as provided by the user and
generated by Isabelle. Its usage is:
\begin{ttbox}
Usage: isabelle 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 Isabelle build
process, provided document preparation has been enabled via suitable
options. 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 \verb|-c| option tells \hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}} 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 \verb|-n| and \verb|-o| option specify
the final output file name and format, the default is ``\verb|document.dvi|''. Note that the result will appear in the parent of
the target \verb|DIR|.
\medskip The \verb|-t| option tells {\LaTeX} how to interpret
tagged Isabelle command regions. Tags are specified as a comma
separated list of modifier/name pairs: ``\verb|+|\isa{foo}'' (or just ``\isa{foo}'') means to keep, ``\verb|-|\isa{foo}'' to drop, and ``\verb|/|\isa{foo}'' to
fold text tagged as \isa{foo}. The builtin default is equivalent
to the tag specification ``\verb|+theory,+proof,+ML,+visible,-invisible|''; see also the {\LaTeX}
macros \verb|\isakeeptag|, \verb|\isadroptag|, and
\verb|\isafoldtag|, in \verb|~~/lib/texinputs/isabelle.sty|.
\medskip Document preparation requires a \verb|document|
directory within the 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, \hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}} is smart
enough to create any of the specified output formats, taking
\verb|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 \verb|root.bib| within
the same directory).
In more complex situations, a separate \verb|build| script for
the document sources may be given. It is invoked with command-line
arguments for the document format and the document variant name.
The script needs to produce corresponding output files, e.g.\
\verb|root.pdf| for target format \verb|pdf| (and default
default variants). The main work can be again delegated to \hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}}, but it is also possible to harvest generated {\LaTeX}
sources and copy them elsewhere, for example.
\medskip When running the session, Isabelle copies the content of
the original \verb|document| directory into its proper place
within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}, according to the session
path and document variant. Then, for any processed theory \isa{A}
some {\LaTeX} source is generated and put there as \isa{A}\verb|.tex|. Furthermore, a list of all generated theory
files is put into \verb|session.tex|. Typically, the root
{\LaTeX} file provided by the user would include \verb|session.tex| to get a document containing all the theories.
The {\LaTeX} versions of the theories require some macros defined in
\verb|~~/lib/texinputs/isabelle.sty|. Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
the underlying \hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}} already includes an appropriate path
specification for {\TeX} inputs.
If the text contains any references to Isabelle symbols (such as
\verb|\|\verb|<forall>|) then \verb|isabellesym.sty| should be included as well. This package
contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, see \cite{isabelle-implementation} 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 \verb|~~/lib/texinputs/isabellesym.sty| of
the distribution.
For proper setup of DVI and PDF documents (with hyperlinks and
bookmarks), we recommend to include \verb|~~/lib/texinputs/pdfsetup.sty| as well.
\medskip As a final step of Isabelle document preparation, \hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}~\verb|-c| is run on the resulting copy of the
\verb|document| directory. Thus the actual output document is
built and installed in its proper place. The generated sources are
deleted after successful run of {\LaTeX} and friends.
Some care is needed if the document output location is configured
differently, say within a directory whose content is still required
afterwards!%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Running {\LaTeX} within the Isabelle environment
\label{sec:tool-latex}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{latex}\hypertarget{tool.latex}{\hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}}} tool provides the basic interface for
Isabelle document preparation. Its usage is:
\begin{ttbox}
Usage: isabelle 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: \hyperlink{executable.latex}{\mbox{\isa{\isatt{latex}}}},
\hyperlink{executable.pdflatex}{\mbox{\isa{\isatt{pdflatex}}}}, \hyperlink{executable.dvips}{\mbox{\isa{\isatt{dvips}}}}, \hyperlink{executable.bibtex}{\mbox{\isa{\isatt{bibtex}}}}
(for \verb|bbl|), and \hyperlink{executable.makeindex}{\mbox{\isa{\isatt{makeindex}}}} (for \verb|idx|). The actual commands are determined from the settings
environment (\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LATEX}}}} etc.).
The \verb|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.
The \verb|syms| output is for internal use; it generates lists
of symbols that are available without loading additional {\LaTeX}
packages.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Examples%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Invoking \hyperlink{tool.latex}{\mbox{\isa{\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 \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}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/IsabelleXXXX/browser_info/HOL/Test/document
isabelle latex -o pdf
\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: