# HG changeset patch # User wenzelm # Date 952533916 -3600 # Node ID 242dab4f164a831c78374bc67c7485c5878d8c7a # Parent f1dd226f5956a6760ff230a20bf1f07b3a0c248f added isatool mkdir; isatool document -c; isatool usedir -D -c; diff -r f1dd226f5956 -r 242dab4f164a doc-src/System/present.tex --- 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