--- a/doc-src/System/present.tex Wed Mar 08 17:44:53 2000 +0100
+++ b/doc-src/System/present.tex Wed Mar 08 17:45:16 2000 +0100
@@ -8,11 +8,12 @@
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 leave
+and \texttt{HOL} from \texttt{Pure}), and application sessions in leaf
positions. 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.
+The \texttt{usedir} and \texttt{mkdir} utilities provide the prime means for
+managing Isabelle sessions, including proper setup for presentation (see
+\S\ref{sec:tool-usedir} and \S\ref{sec:tool-mkdir}).
\section{Generating theory browsing information} \label{sec:info}
@@ -95,6 +96,17 @@
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 -d Foo
+edit Foo/ROOT.ML
+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}
@@ -242,10 +254,11 @@
Usage: document [OPTIONS] [DIR]
Options are:
+ -c remove DIR after succesful run (!)
-o FORMAT specify output format: dvi (default), dvi.gz, ps,
ps.gz, pdf
- Prepare the theory session document in DIR (default '.')
+ 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,
@@ -295,11 +308,13 @@
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} is run on the resulting
+\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}). Note that the generated sources are left as is. While
-they may be safely deleted afterwards, this is \emph{not} done automatically.
+\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}}
@@ -332,8 +347,77 @@
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}
-\section{Managing Isabelle logic sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir}
+The \tooldx{mkdir} utility prepares Isabelle session source directories,
+including a sensible default setup of \texttt{IsaMakefile}, \texttt{ROOT.ML}
+and an optional \texttt{document} directory. Its usage is:
+\begin{ttbox}
+Usage: mkdir [LOGIC] NAME
+
+ Options are:
+ -I FILE alternative IsaMakefile output
+ -P include parent logic target
+ -b setup build mode (session outputs heap image)
+ -d setup document
+
+ Prepare session directory, including IsaMakefile, document etc.
+ 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
+experimentally, with varying options.
+
+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{-d} option creates a \texttt{document} directory with a
+minimal \texttt{root.tex} file, which is sufficient to get all theories pretty
+printed in the order of appearance. See \S\ref{sec:tool-document} for further
+information on Isabelle document preparation.
+
+
+\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 -d Foo
+\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
+information and the document automatically. The \texttt{IsaMakefile} is
+usually tuned manually later, e.g.\ adding actual source dependencies, or
+changing the options passed to \texttt{usedir}.
+
+
+\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:
@@ -341,8 +425,10 @@
Usage: usedir LOGIC NAME
Options are:
+ -D PATH dump generated document sources into PATH
-P PATH set path for remote theory browsing information
-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)
-i BOOL generate theory browsing information,
i.e. HTML / graph data (default false)
@@ -393,6 +479,13 @@
\texttt{document} directory. See \S\ref{sec:tool-document} and
\S\ref{sec:tool-latex} for more details.
+\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
+{\LaTeX} sources in the actual document directory. Thus the Isabelle
+\texttt{document} or \texttt{latex} tools may be run later, facilitating much
+easier debugging of {\LaTeX} errors, for example.
+
\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
@@ -407,7 +500,10 @@
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}.
+\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.
+
%%% Local Variables:
%%% mode: latex