wenzelm@4540: berghofe@3753: %% $Id$ wenzelm@3188: wenzelm@10580: \chapter{Presenting theories}\label{ch:present} wenzelm@3188: wenzelm@7849: Isabelle provides several ways to present the outcome of formal developments, wenzelm@7849: including WWW-based browsable libraries or actual printable documents. wenzelm@7849: Presentation is centered around the concept of \emph{logic sessions}. The wenzelm@12464: global session structure is that of a tree, with Isabelle Pure at its root, wenzelm@12464: further object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and wenzelm@12464: application sessions in leaf positions (usually without a separate image). wenzelm@7849: wenzelm@11616: The \texttt{mkdir} (see \S\ref{sec:tool-mkdir}) and \texttt{make} (see wenzelm@11616: \S\ref{sec:tool-make}) tools of Isabelle provide the primary means for wenzelm@11616: managing Isabelle sessions, including proper setup for presentation. Here the wenzelm@12464: \texttt{usedir} (see \S\ref{sec:tool-usedir}) tool takes care to let the wenzelm@12464: \texttt{isabelle} process run any additional stages required for document wenzelm@12464: preparation, notably the tools \texttt{document} (see wenzelm@12464: \S\ref{sec:tool-document}) and \texttt{latex} (see \S\ref{sec:tool-latex}). wenzelm@12464: The complete tool chain for managing batch-mode Isabelle sessions is wenzelm@12464: illustrated in figure~\ref{fig:session-tools}. wenzelm@12464: wenzelm@12464: \begin{figure}[htbp] wenzelm@12464: \begin{center} wenzelm@12464: \begin{tabular}{lp{0.6\textwidth}} wenzelm@12464: \texttt{isatool mkdir} & invoked once by the user to create the initial wenzelm@12464: source setup (common \texttt{IsaMakefile} plus a single session directory); \\ wenzelm@12464: \texttt{isatool make} & invoked repeatedly by the user to wenzelm@12464: keep session output up-to-date (HTML, documents etc.); \\ wenzelm@12464: \texttt{isatool usedir} & part of the standard \texttt{IsaMakefile} entry of a session; \\ wenzelm@12464: \texttt{isabelle} & run through \texttt{isatool usedir}; \\ wenzelm@12464: \texttt{isatool document} & run by the Isabelle process if document preparation is enabled; \\ wenzelm@12464: \texttt{isatool latex} & universal {\LaTeX} tool wrapper invoked multiple times wenzelm@12464: by \texttt{isatool document}; also useful for manual experiments; \\ wenzelm@12464: \end{tabular} wenzelm@12464: \caption{The tool chain of Isabelle session presentation} wenzelm@12464: \label{fig:session-tools} wenzelm@12464: \end{center} wenzelm@12464: \end{figure} wenzelm@7849: wenzelm@7849: wenzelm@12464: \section{Generating theory browser information} \label{sec:info} wenzelm@4540: \index{theory browsing information|bold} wenzelm@3188: wenzelm@7849: As a side-effect of running a logic sessions, Isabelle is able to generate wenzelm@7849: theory browsing information, including HTML documents that show a theory's wenzelm@7849: definition, the theorems proved in its ML file and the relationship with its wenzelm@7849: ancestors and descendants. Besides the HTML file that is generated for every wenzelm@7849: theory, Isabelle stores links to all theories in an index file. These indexes wenzelm@7882: are linked with other indexes to represent the overall tree structure of logic wenzelm@7882: sessions. wenzelm@3188: wenzelm@7258: Isabelle also generates graph files that represent the theory hierarchy of a wenzelm@7258: logic. There is a graph browser Java applet embedded in the generated HTML wenzelm@7258: pages, and also a stand-alone application that allows browsing theory graphs wenzelm@12464: without having to start a WWW client first. The latter version also includes wenzelm@11582: features such as generating Postscript files, which are not available in the wenzelm@11582: applet version. See \S\ref{sec:browse} for further information. berghofe@3753: wenzelm@7258: \medskip wenzelm@7258: wenzelm@12464: The easiest way to let Isabelle generate theory browsing information for wenzelm@12464: existing sessions is to append ``\texttt{-i true}'' to the wenzelm@12464: \settdx{ISABELLE_USEDIR_OPTIONS} before invoking \texttt{isatool make} (or wenzelm@12464: \texttt{./build} in the distribution). For example, add something like this wenzelm@12464: to your Isabelle settings file wenzelm@3188: \begin{ttbox} berghofe@3753: ISABELLE_USEDIR_OPTIONS="-i true" wenzelm@3188: \end{ttbox} wenzelm@7258: and then change into the \texttt{src/FOL} directory of the Isabelle wenzelm@7258: distribution and run \texttt{isatool make}, or even \texttt{isatool make all}. wenzelm@12464: The presentation output will appear in \texttt{\$ISABELLE_BROWSER_INFO/FOL}, wenzelm@12464: which usually refers to \verb,~/isabelle/browser_info/FOL,. Note that option wenzelm@12464: \texttt{-v true} will make the internal runs of \texttt{usedir} more explicit wenzelm@12464: about such details. wenzelm@7258: wenzelm@12464: Many standard Isabelle sessions (such as \texttt{HOL/ex}) also provide actual wenzelm@7882: printable documents. These are prepared automatically as well if enabled like wenzelm@7882: this, using the \texttt{-d} option wenzelm@7849: \begin{ttbox} wenzelm@7849: ISABELLE_USEDIR_OPTIONS="-i true -d dvi" wenzelm@7849: \end{ttbox} wenzelm@12464: Enabling options \texttt{-i} and \texttt{-d} simultaneausly as shown above wenzelm@12464: causes an appropriate ``document'' link to be included in the HTML index. wenzelm@12464: Documents (or raw document sources) may be generated independently of browser wenzelm@12464: information as well, see \S\ref{sec:tool-document} for further details. berghofe@3753: wenzelm@12464: \bigskip The theory browsing information is stored in a sub-directory wenzelm@12464: directory determined by the \settdx{ISABELLE_BROWSER_INFO} setting plus a wenzelm@12464: prefix corresponding to the session identifier (according to the tree wenzelm@12464: structure of sub-sessions by default). A complete WWW view of all standard wenzelm@12464: object-logics and examples of the Isabelle distribution is available at the wenzelm@12464: Cambridge or Munich Isabelle sites: wenzelm@6623: \begin{center}\small wenzelm@6623: \begin{tabular}{l} wenzelm@6623: \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ wenzelm@6623: \url{http://isabelle.in.tum.de/library/} \\ wenzelm@6623: \end{tabular} wenzelm@6623: \end{center} wenzelm@6623: wenzelm@12464: \medskip In order to present your own theories on the web, simply copy the wenzelm@9209: corresponding subdirectory from \texttt{ISABELLE_BROWSER_INFO} to your WWW wenzelm@12464: server, having generated browser info like this: berghofe@7251: \begin{ttbox} wenzelm@7861: isatool usedir -i true HOL Foo berghofe@7251: \end{ttbox} wenzelm@7861: This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file wenzelm@12464: to load all your theories, and HOL is your parent logic image (\texttt{isatool wenzelm@12464: mkdir} assists in setting up Isabelle session directories, see wenzelm@12464: \S\ref{sec:tool-mkdir}). Theory browser information for HOL should have been wenzelm@12464: generated already beforehand. Alternatively, one may specify an external link wenzelm@12464: to an existing body of HTML data by giving \texttt{usedir} a \texttt{-P} wenzelm@12464: option like this: wenzelm@7258: \begin{ttbox} wenzelm@7861: isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo wenzelm@7258: \end{ttbox} wenzelm@7258: wenzelm@8363: \medskip For production use, the \texttt{usedir} tool is usually invoked in an wenzelm@8363: appropriate \texttt{IsaMakefile}, via the Isabelle \texttt{make} utility. wenzelm@8363: There is a separate \texttt{mkdir} tool to provide easy setup of all this, wenzelm@8363: with only minimal manual editing required. wenzelm@8363: \begin{ttbox} wenzelm@12464: isatool mkdir HOL Foo && isatool make wenzelm@8363: \end{ttbox} wenzelm@8363: See \S\ref{sec:tool-mkdir} for more information on preparing Isabelle session wenzelm@8363: directories, including the setup for documents. berghofe@3753: wenzelm@7849: berghofe@3753: \section{Browsing theory graphs} \label{sec:browse} berghofe@3753: \index{theory graph browser|bold} berghofe@3753: wenzelm@12464: The Isabelle graph browser is a general tool for visualizing dependency wenzelm@12464: graphs. Certain nodes of the graph (i.e.~theories) can be grouped together in wenzelm@12464: ``directories'', whose contents may be hidden, thus enabling the user to wenzelm@12464: collapse irrelevant portions of information. The browser is written in Java, wenzelm@12464: it can be used both as a stand-alone application and as an applet. Note that wenzelm@12464: the option \texttt{-g} of \texttt{isatool usedir} (see wenzelm@12464: \S\ref{sec:tool-usedir}) creates graph presentations in batch mode for wenzelm@12464: inclusion in session documents. wenzelm@4540: wenzelm@3188: berghofe@3753: \subsection{Invoking the graph browser} wenzelm@4540: wenzelm@4540: The stand-alone version of the graph browser is wrapped up as an wenzelm@4540: Isabelle tool called \tooldx{browser}: berghofe@3753: \begin{ttbox} wenzelm@9237: Usage: browser [OPTIONS] [GRAPHFILE] wenzelm@9237: wenzelm@9237: Options are: wenzelm@20571: -c cleanup -- remove GRAPHFILE after use wenzelm@12583: -o FILE output to FILE (ps, eps, pdf) berghofe@3753: \end{ttbox} wenzelm@9209: When no filename is specified, the browser automatically changes to the wenzelm@9209: directory \texttt{ISABELLE_BROWSER_INFO}. berghofe@3753: wenzelm@20571: \medskip The \texttt{-c} option causes the input file to be removed after use. wenzelm@12583: wenzelm@12583: The \texttt{-o} option indicates batch-mode operation, with the output written wenzelm@12583: to the indicated file; note that \texttt{pdf} produces an \texttt{eps} copy as wenzelm@12583: well. wenzelm@12583: wenzelm@13047: \medskip The applet version of the browser is part of the standard WWW theory wenzelm@13047: presentation, see the link ``theory dependencies'' within each session index. wenzelm@4540: wenzelm@3188: berghofe@3753: \subsection{Using the graph browser} wenzelm@4540: wenzelm@4540: The browser's main window, which is shown in figure wenzelm@12464: \ref{fig:browserwindow}, consists of two sub-windows: In the left wenzelm@7849: sub-window, the directory tree is displayed. The graph itself is wenzelm@7849: displayed in the right sub-window. wenzelm@7849: \begin{figure}[ht] wenzelm@6623: \includegraphics[width=\textwidth]{browser_screenshot} wenzelm@12464: \caption{\label{fig:browserwindow} Browser main window} berghofe@3753: \end{figure} berghofe@3753: wenzelm@4540: berghofe@3753: \subsubsection*{The directory tree window} wenzelm@4540: wenzelm@7882: We describe the usage of the directory browser and the meaning of the wenzelm@7882: different items in the browser window. berghofe@3753: \begin{itemize} wenzelm@4540: wenzelm@4540: \item A red arrow before a directory name indicates that the directory wenzelm@4540: is currently ``folded'', i.e.~the nodes in this directory are wenzelm@7849: collapsed to one single node. In the right sub-window, the names of wenzelm@4540: nodes corresponding to folded directories are enclosed in square wenzelm@7849: brackets and displayed in red color. wenzelm@4540: wenzelm@4540: \item A green downward arrow before a directory name indicates that wenzelm@4540: the directory is currently ``unfolded''. It can be folded by wenzelm@4540: clicking on the directory name. Clicking on the name for a second wenzelm@4540: time unfolds the directory again. Alternatively, a directory can wenzelm@4540: also be unfolded by clicking on the corresponding node in the right wenzelm@7849: sub-window. wenzelm@4540: wenzelm@7882: \item Blue arrows stand before ordinary node names. When clicking on such a wenzelm@7882: name (i.e.\ that of a theory), the graph display window focuses to the wenzelm@7882: corresponding node. Double clicking invokes a text viewer window in which wenzelm@7882: the contents of the theory file are displayed. wenzelm@4540: berghofe@3753: \end{itemize} wenzelm@3188: wenzelm@4540: berghofe@3753: \subsubsection*{The graph display window} wenzelm@4540: wenzelm@4540: When pointing on an ordinary node, an upward and a downward arrow is wenzelm@4540: shown. Initially, both of these arrows are green. Clicking on the berghofe@3753: upward or downward arrow collapses all predecessor or successor nodes, wenzelm@7849: respectively. The arrow's color then changes to red, indicating that berghofe@3753: the predecessor or successor nodes are currently collapsed. The node wenzelm@4540: corresponding to the collapsed nodes has the name ``{\tt [....]}''. To wenzelm@4540: uncollapse the nodes again, simply click on the red arrow or on the wenzelm@4540: node with the name ``{\tt [....]}''. Similar to the directory browser, wenzelm@4540: the contents of theory files can be displayed by double clicking on wenzelm@4540: the corresponding node. wenzelm@3188: wenzelm@4540: wenzelm@4540: \subsubsection*{The ``File'' menu} wenzelm@4540: wenzelm@4555: Please note that due to Java security restrictions this menu is not wenzelm@4540: available in the applet version. The meaning of the menu items is as wenzelm@4540: follows: berghofe@3753: \begin{description} wenzelm@4540: wenzelm@7882: \item[Open \dots] Open a new graph file. wenzelm@4540: wenzelm@11582: \item[Export to PostScript] Outputs the current graph in Postscript format, wenzelm@12464: appropriately scaled to fit on one single sheet of A4 paper. The resulting wenzelm@11582: file can be printed directly. wenzelm@4540: wenzelm@11582: \item[Export to EPS] Outputs the current graph in Encapsulated Postscript wenzelm@11582: format. The resulting file can be included in other documents. wenzelm@4540: berghofe@3753: \item[Quit] Quit the graph browser. wenzelm@4540: berghofe@3753: \end{description} berghofe@3753: wenzelm@4540: berghofe@3753: \subsection*{*Syntax of graph definition files} wenzelm@4540: berghofe@3753: A graph definition file has the following syntax: berghofe@3753: \begin{eqnarray*} wenzelm@4540: \mbox{\it graph} & = & \{ \: \mbox{\it vertex \tt ;} \: \} ^ + \\ wenzelm@4540: vertex & = & \mbox{\it vertexname} \: \mbox{\it vertexID} \: \mbox{\it dirname} \: [ \mbox{\tt +} ] wenzelm@4540: \: \mbox{\it path} \: [ \mbox{\tt <} | \mbox{\tt >} ] \: \{ \: \mbox{\it vertexID} \: \} ^ * berghofe@3753: \end{eqnarray*} wenzelm@4540: berghofe@3753: The meaning of the items in a vertex description is as follows: berghofe@3753: \begin{description} wenzelm@4540: berghofe@3753: \item[vertexname] The name of the vertex. wenzelm@4540: wenzelm@4540: \item[vertexID] The vertex identifier. Note that there may be two wenzelm@4540: vertices with equal names, whereas identifiers must be unique. wenzelm@4540: wenzelm@4540: \item[dirname] The name of the ``directory'' the vertex should be wenzelm@4540: placed in. A ``{\tt +}'' sign after {\it dirname} indicates that wenzelm@4540: the nodes in the directory are initially visible. Directories are wenzelm@4540: initially invisible by default. wenzelm@4540: wenzelm@4540: \item[path] The path of the corresponding theory file. This is wenzelm@4540: specified relatively to the path of the graph definition file. wenzelm@4540: wenzelm@4540: \item[List of successor/predecessor nodes] A ``{\tt <}'' sign before wenzelm@4540: the list means that successor nodes are listed, a ``{\tt >}'' sign wenzelm@4540: means that predecessor nodes are listed. If neither ``{\tt <}'' nor wenzelm@4540: ``{\tt >}'' is found, the browser assumes that successor nodes are wenzelm@4540: listed. wenzelm@4540: berghofe@3753: \end{description} wenzelm@5364: wenzelm@5364: wenzelm@8363: \section{Creating Isabelle session directories --- \texttt{isatool mkdir}} wenzelm@8363: \label{sec:tool-mkdir} wenzelm@7849: wenzelm@8363: The \tooldx{mkdir} utility prepares Isabelle session source directories, wenzelm@11582: including a sensible default setup of \texttt{IsaMakefile}, \texttt{ROOT.ML}, wenzelm@11582: and a \texttt{document} directory with a minimal \texttt{root.tex} that is wenzelm@13047: sufficient to print all theories of the session (in the order of appearance); wenzelm@13047: see \S\ref{sec:tool-document} for further information on Isabelle document wenzelm@12464: preparation. The usage of \texttt{isatool mkdir} is: wenzelm@8363: \begin{ttbox} wenzelm@9237: Usage: mkdir [OPTIONS] [LOGIC] NAME wenzelm@8363: wenzelm@8363: Options are: wenzelm@8363: -I FILE alternative IsaMakefile output wenzelm@8363: -P include parent logic target wenzelm@8363: -b setup build mode (session outputs heap image) wenzelm@11582: -q quiet mode wenzelm@8363: wenzelm@11582: Prepare session directory, including IsaMakefile and document source, wenzelm@8363: with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC) wenzelm@8363: \end{ttbox} wenzelm@8363: wenzelm@8363: The \texttt{mkdir} tool is conservative in the sense that any existing wenzelm@8363: \texttt{IsaMakefile} etc.\ is left unchanged. Thus it is safe to invoke it wenzelm@12464: multiple times, although later runs may not have the desired effect. wenzelm@8363: wenzelm@8363: Note that \texttt{mkdir} is unable to change \texttt{IsaMakefile} wenzelm@8363: incrementally --- manual changes are required for multiple sub-sessions. On wenzelm@8363: order to get an initial working session, the only editing needed is to add wenzelm@8363: appropriate \texttt{use_thy} calls to the generated \texttt{ROOT.ML} file. wenzelm@8363: wenzelm@8363: wenzelm@8363: \subsection*{Options} wenzelm@8363: wenzelm@8363: The \texttt{-I} option specifies an alternative to \texttt{IsaMakefile} for wenzelm@8363: dependencies. Note that ``\texttt{-}'' refers to \emph{stdout}, i.e.\ wenzelm@8363: ``\texttt{-I-}'' provides an easy way to peek at \texttt{mkdir}'s idea of wenzelm@8363: \texttt{make} setup required for some particular of Isabelle session. wenzelm@8363: wenzelm@8363: \medskip The \texttt{-P} option includes a target for the parent wenzelm@8363: \texttt{LOGIC} session in the generated \texttt{IsaMakefile}. The wenzelm@8363: corresponding sources are assumed to be located within the Isabelle wenzelm@8363: distribution. wenzelm@8363: wenzelm@8363: \medskip The \texttt{-b} option sets up the current directory as the base for wenzelm@8363: a new session that provides an actual logic image, as opposed to one that only wenzelm@8363: runs several theories based on an existing image. Note that in the latter wenzelm@8363: case, everything except \texttt{IsaMakefile} would be placed into a separate wenzelm@8363: directory \texttt{NAME}, rather than the current one. See wenzelm@8363: \S\ref{sec:tool-usedir} for further information on \emph{build mode} vs.\ wenzelm@8363: \emph{example mode} of the \texttt{usedir} utility. wenzelm@8363: wenzelm@11582: \medskip The \texttt{-q} enables quiet mode, suppressing further notes on how wenzelm@11582: to proceed. wenzelm@8363: wenzelm@8363: wenzelm@8363: \subsection*{Examples} wenzelm@8363: wenzelm@8363: The standard setup of a single ``example session'' based on the default logic, wenzelm@8363: with proper document generation is generated like this: wenzelm@8363: \begin{ttbox} wenzelm@12464: isatool mkdir Foo && isatool make wenzelm@8363: \end{ttbox} wenzelm@8363: \noindent The theory sources should be put into the \texttt{Foo} directory, and its wenzelm@8363: \texttt{ROOT.ML} should be edited to load all required theories. Invoking wenzelm@12464: \texttt{isatool make} again would run the whole session, generating browser wenzelm@8363: information and the document automatically. The \texttt{IsaMakefile} is wenzelm@13047: typically tuned manually later, e.g.\ adding source dependencies, or changing wenzelm@13047: the options passed to \texttt{usedir}. wenzelm@8363: wenzelm@12464: \medskip Large projects may demand further sessions, potentially with separate wenzelm@12464: logic images being created. This usually requires manual editing of the wenzelm@12464: generated \texttt{IsaMakefile}, which is meant to cover all of the sub-session wenzelm@12464: directories at the same time (this is the deeper reasong why wenzelm@12464: \texttt{IsaMakefile} is not made part of the initial session directory created wenzelm@12464: by \texttt{isatool mkdir}). See \texttt{src/HOL/IsaMakefile} of the Isabelle wenzelm@12464: distribution for a full-blown example. wenzelm@12464: wenzelm@8363: wenzelm@8363: \section{Running Isabelle sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir} wenzelm@7849: wenzelm@7849: The \tooldx{usedir} utility builds object-logic images, or runs example wenzelm@7849: sessions based on existing logics. Its usage is: wenzelm@7849: \begin{ttbox} wenzelm@11582: wenzelm@9237: Usage: usedir [OPTIONS] LOGIC NAME wenzelm@7849: wenzelm@7849: Options are: wenzelm@17195: -C BOOL copy existing document directory to -D PATH (default true) wenzelm@8363: -D PATH dump generated document sources into PATH wenzelm@24177: -M MAX multithreading: maximum number of worker threads (default 1) wenzelm@7849: -P PATH set path for remote theory browsing information wenzelm@24177: -T LEVEL multithreading: trace level (default 0) wenzelm@17054: -V VERSION declare alternative document VERSION wenzelm@7849: -b build mode (output heap image, using current dir) wenzelm@8363: -c BOOL tell ML system to compress output image (default true) wenzelm@7849: -d FORMAT build document as FORMAT (default false) wenzelm@17054: -f NAME use ML file NAME (default ROOT.ML) wenzelm@12464: -g BOOL generate session graph image for document (default false) wenzelm@10564: -i BOOL generate theory browser information (default false) wenzelm@10564: -m MODE add print mode for output wenzelm@11582: -p LEVEL set level of detail for proof objects wenzelm@7849: -r reset session path wenzelm@7849: -s NAME override session NAME wenzelm@11582: -v BOOL be verbose (default false) wenzelm@7849: wenzelm@7849: Build object-logic or run examples. Also creates browsing wenzelm@7849: information (HTML etc.) according to settings. wenzelm@7849: wenzelm@7849: ISABELLE_USEDIR_OPTIONS= wenzelm@24975: HOL_USEDIR_OPTIONS= wenzelm@7849: \end{ttbox} wenzelm@7849: wenzelm@7849: Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is wenzelm@7849: implicitly prefixed to \emph{any} \texttt{usedir} call. Since the wenzelm@7849: \ttindex{IsaMakefile}s of all object-logics distributed with Isabelle just wenzelm@7849: invoke \texttt{usedir} for the real work, one may control compilation options wenzelm@7849: globally via above variable. In particular, generation of \rmindex{HTML} wenzelm@7882: browsing information and document preparation is controlled here. wenzelm@7849: wenzelm@24975: The \settdx{HOL_USEDIR_OPTIONS} setting is specific to the main wenzelm@24975: Isabelle/HOL image; its value is appended to wenzelm@24975: \verb,ISABELLE_USEDIR_OPTIONS, for that particular session only. wenzelm@24975: wenzelm@7849: wenzelm@7849: \subsection*{Options} wenzelm@7849: wenzelm@7882: Basically, there are two different modes of operation: \emph{build mode} wenzelm@7882: (enabled through the \texttt{-b} option) and \emph{example mode} (default). wenzelm@7849: wenzelm@7849: Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with input wenzelm@7849: image \texttt{LOGIC} and output to \texttt{NAME}, as provided on the command wenzelm@7849: line. This will be a batch session, running \texttt{ROOT.ML} from the current wenzelm@7849: directory and then quitting. It is assumed that \texttt{ROOT.ML} contains all wenzelm@7883: {\ML} commands required to build the logic. wenzelm@7849: wenzelm@7849: In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC} wenzelm@7882: and automatically runs \texttt{ROOT.ML} from within directory \texttt{NAME}. wenzelm@7882: It assumes that this file contains appropriate {\ML} commands to run the wenzelm@7882: desired examples. wenzelm@7849: wenzelm@7882: \medskip The \texttt{-i} option controls theory browser data generation. It wenzelm@7882: may be explicitly turned on or off --- as usual, the last occurrence of wenzelm@10564: \texttt{-i} on the command line wins. wenzelm@10564: wenzelm@10564: The \texttt{-P} option specifies a path (or actual URL) to be prefixed to any wenzelm@10564: \emph{non-local} reference of existing theories. Thus user sessions may wenzelm@10564: easily link to existing Isabelle libraries already present on the WWW. wenzelm@10564: wenzelm@10564: The \texttt{-m} options specifies additional print modes to be activated wenzelm@10564: temporarily while the session is processed. wenzelm@7849: wenzelm@7849: \medskip The \texttt{-d} option controls document preparation. Valid wenzelm@7882: arguments are \texttt{false} (do not prepare any document; this is default), wenzelm@7882: or any of \texttt{dvi}, \texttt{dvi.gz}, \texttt{ps}, \texttt{ps.gz}, wenzelm@7849: \texttt{pdf}. The logic session has to provide a properly setup wenzelm@7849: \texttt{document} directory. See \S\ref{sec:tool-document} and wenzelm@7849: \S\ref{sec:tool-latex} for more details. wenzelm@7849: wenzelm@17099: \medskip The \texttt{-V} option declares alternative document versions, wenzelm@17099: consisting of name/tags pairs (cf.\ options \texttt{-n} and \texttt{-t} of the wenzelm@17099: \texttt{document} tool, \S\ref{sec:tool-document}). The standard document is wenzelm@17099: equivalent to ``\texttt{document=theory,proof,ML}'', which means that all wenzelm@17099: theory begin/end commands, proof body texts, and ML code will be presented wenzelm@17099: faithfully. An alternative version ``\texttt{outline=/proof/ML}'' would fold wenzelm@17099: proof and ML parts, replacing the original text by a short place-holder. The wenzelm@17099: form ``$name$\verb,=-,'' means to remove document $name$ from the list of wenzelm@17099: versions to be processed. Any number of \texttt{-V} options may be given; wenzelm@17099: later declarations have precedence over earlier ones. wenzelm@17054: wenzelm@17054: \medskip The \texttt{-g} option produces images of the theory dependency graph wenzelm@17054: (cf.\ \S\ref{sec:browse}) for inclusion in the generated document, both as wenzelm@12464: \texttt{session_graph.eps} and \texttt{session_graph.pdf} at the same time. wenzelm@13047: To include this in the final {\LaTeX} document one could say wenzelm@13047: \verb,\includegraphics{session_graph}, in \texttt{document/root.tex} (omitting wenzelm@13047: the file-name extension enables {\LaTeX} to select to correct version, either wenzelm@13047: for the DVI or PDF output path). wenzelm@12464: wenzelm@17195: \medskip The \texttt{-D} option causes the generated document sources to be wenzelm@13018: dumped at location \texttt{PATH}; this path is relative to the session's main wenzelm@17195: directory. If the \texttt{-C} option is true, this will include a copy of an wenzelm@17195: existing \texttt{document} directory as provided by the user. For example, wenzelm@17195: \texttt{isatool usedir -D generated HOL Foo} produces a complete set of wenzelm@17195: document sources at \texttt{Foo/generated}. Subsequent invocation of wenzelm@17195: \texttt{isatool document Foo/generated} (see also \S\ref{sec:tool-document}) wenzelm@17195: will process the final result independently of an Isabelle job. This wenzelm@17195: decoupled mode of operation facilitates debugging of serious {\LaTeX} errors, wenzelm@17195: for example. wenzelm@8363: wenzelm@11582: \medskip The \texttt{-p} option determines the level of detail for internal wenzelm@11582: proof objects, see also the \emph{Isabelle Reference wenzelm@11582: Manual}~\cite{isabelle-ref}. wenzelm@11582: wenzelm@11582: \medskip The \texttt{-v} option causes additional information to be printed wenzelm@13047: while running the session, notably the location of prepared documents. wenzelm@11582: wenzelm@24177: \medskip The \texttt{-M} option specifies the maximum number of wenzelm@24177: parallel threads used for processing independent theory files wenzelm@25774: (multithreading only works on suitable ML platforms). The special wenzelm@25774: value of ``\texttt{0}'' or ``\texttt{max}'' refers to the number of wenzelm@25774: actual CPU cores of the underlying machine, which is a good starting wenzelm@25774: point for optimal performance tuning. The \texttt{-T} option wenzelm@25774: determines the level of detail in tracing output concerning the wenzelm@25774: internal locking and scheduling in multithreaded operation. This may wenzelm@25774: be helpful in isolating performance bottle-necks, e.g.\ due to wenzelm@25774: excessive wait states when locking critical code sections. wenzelm@24177: wenzelm@7849: \medskip Any \texttt{usedir} session is named by some \emph{session wenzelm@7882: identifier}. These accumulate, documenting the way sessions depend on wenzelm@7882: others. For example, consider \texttt{Pure/FOL/ex}, which refers to the wenzelm@9695: examples of FOL, which in turn is built upon Pure. wenzelm@7849: wenzelm@7882: The current session's identifier is by default just the base name of the wenzelm@7882: \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME} argument (in wenzelm@7882: example mode). This may be overridden explicitly via the \texttt{-s} option. wenzelm@7849: wenzelm@7849: wenzelm@7849: \subsection*{Examples} wenzelm@7849: wenzelm@7849: Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's wenzelm@7849: object-logics as a model for your own developments. For example, see wenzelm@8363: \texttt{src/FOL/IsaMakefile}. The Isabelle \texttt{mkdir} tool (see wenzelm@8363: \S\ref{sec:tool-mkdir}) creates \texttt{IsaMakefile}s with proper invocation wenzelm@8363: of \texttt{usedir} as well. wenzelm@8363: wenzelm@12464: wenzelm@12464: \section{Preparing Isabelle session documents --- \texttt{isatool document}} wenzelm@12464: \label{sec:tool-document} wenzelm@12464: wenzelm@12464: The \tooldx{document} utility prepares logic session documents, processing the wenzelm@12464: sources both as provided by the user and generated by Isabelle. Its usage is: wenzelm@12464: \begin{ttbox} wenzelm@12464: Usage: document [OPTIONS] [DIR] wenzelm@12464: wenzelm@12464: Options are: wenzelm@12464: -c cleanup -- be aggressive in removing old stuff wenzelm@17054: -n NAME specify document name (default 'document') wenzelm@12464: -o FORMAT specify output format: dvi (default), dvi.gz, ps, wenzelm@12464: ps.gz, pdf wenzelm@17054: -t TAGS specify tagged region markup wenzelm@12464: wenzelm@12464: Prepare the theory session document in DIR (default 'document') wenzelm@12464: producing the specified output format. wenzelm@12464: \end{ttbox} wenzelm@12464: This tool is usually run automatically as part of the corresponding Isabelle wenzelm@12464: batch process, provided document preparation has been enabled (cf.\ the wenzelm@12464: \texttt{-d} option of the \texttt{usedir} utility, \S\ref{sec:tool-usedir}). wenzelm@12464: It may be manually invoked on the generated browser information document wenzelm@12464: output as well, e.g.\ in case of errors encountered in the batch run. wenzelm@12464: wenzelm@17054: \medskip The \texttt{-c} option tells the \texttt{document} tool to dispose wenzelm@17054: the document sources after successful operation. This is the right thing to wenzelm@17054: do for sources generated by an Isabelle process, but take care of your files wenzelm@17054: in manual document preparation! wenzelm@17054: wenzelm@17054: \medskip The \texttt{-n} and \texttt{-o} option specify the final output file wenzelm@17054: name and format, the default is ``\texttt{document.dvi}''. Note that the wenzelm@17054: result will appear in the parent of the target \texttt{DIR}. wenzelm@17054: wenzelm@17054: \medskip The \texttt{-t} option tells {\LaTeX} how to interpret tagged wenzelm@17054: Isabelle command regions. Tags are specified as a comma separated list of wenzelm@17054: modifier/name pairs: ``\verb,+,$foo$'' (or just ``$foo$'') means to keep, wenzelm@17054: ``\verb,-,$foo$'' to drop, and ``\verb,/,$foo$'' to fold text tagged as $foo$. wenzelm@17054: The builtin default is equivalent to the tag specification wenzelm@17054: ``\texttt{/theory,/proof,/ML,+visible,-invisible}''; see also the {\LaTeX} wenzelm@17054: macros \verb,\isakeeptag,, \verb,\isadroptag,, and \verb,\isafoldtag, in wenzelm@17054: \texttt{isabelle.sty}. wenzelm@17054: wenzelm@12464: \medskip Document preparation requires a properly setup ``\texttt{document}'' wenzelm@12464: directory within the logic session sources. This directory is supposed to wenzelm@12464: contain all the files needed to produce the final document --- apart from the wenzelm@12464: actual theories which are generated by Isabelle. wenzelm@12464: wenzelm@12464: \medskip For most practical purposes, the \texttt{document} tool is smart wenzelm@12464: enough to create any of the specified output formats, taking \texttt{root.tex} wenzelm@12464: supplied by the user as a starting point. This even includes multiple runs of wenzelm@12464: {\LaTeX} to accommodate references and bibliographies (the latter assumes wenzelm@12464: \texttt{root.bib} within the same directory). wenzelm@12464: wenzelm@12464: In more complex situations, a separate \texttt{IsaMakefile} for the document wenzelm@12464: sources may be given instead. This should provide targets for any admissible wenzelm@12464: document format; these have to produce corresponding output files named after wenzelm@12464: \texttt{root} as well, e.g.\ \texttt{root.dvi} for target format \texttt{dvi}. wenzelm@12464: wenzelm@12464: \medskip When running the session, Isabelle copies the original wenzelm@12464: \texttt{document} directory into its proper place within wenzelm@12464: \texttt{ISABELLE_BROWSER_INFO} according to the session path. Then, for any wenzelm@12464: processed theory $A$ some {\LaTeX} source is generated and put there as wenzelm@12464: $A$\texttt{.tex}. Furthermore, a list of all generated theory files is put wenzelm@12464: into \texttt{session.tex}. Typically, the root {\LaTeX} file provided by the wenzelm@12464: user would include \texttt{session.tex} to get a document containing all the wenzelm@12464: theories. wenzelm@12464: wenzelm@12464: The {\LaTeX} versions of the theories require some macros defined in wenzelm@12464: \texttt{isabelle.sty} as distributed with Isabelle. Doing wenzelm@13047: \verb,\usepackage{isabelle}, in \texttt{root.tex} should be fine; the wenzelm@13047: underlying Isabelle \texttt{latex} utility already includes an appropriate wenzelm@12464: {\TeX} inputs path. wenzelm@12464: wenzelm@12464: If the text contains any references to Isabelle symbols (such as wenzelm@12464: \verb,\,) then \texttt{isabellesym.sty} should be included as well. wenzelm@12464: This package contains a standard set of {\LaTeX} macro definitions wenzelm@12464: \verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see wenzelm@12464: Appendix~\ref{app:symbols} for a complete list of predefined Isabelle wenzelm@12464: symbols). Users may invent further symbols as well, just by providing wenzelm@12464: {\LaTeX} macros in a similar fashion as in \texttt{isabellesym.sty} of the wenzelm@12464: distribution. wenzelm@12464: wenzelm@26908: For proper setup of PDF documents (with hyperlinks and bookmarks), we wenzelm@26908: recommend to include \verb,pdfsetup.sty, as well. It is safe to do so wenzelm@26908: even without using PDF~\LaTeX. wenzelm@12464: wenzelm@12464: \medskip As a final step of document preparation within Isabelle, wenzelm@12464: \texttt{isatool document -c} is run on the resulting \texttt{document} wenzelm@12464: directory. Thus the actual output document is built and installed in its wenzelm@12464: proper place (as linked by the session's \texttt{index.html} if option wenzelm@12464: \texttt{-i} of \texttt{usedir} has been enabled, cf.\ \S\ref{sec:info}). The wenzelm@12464: generated sources are deleted after successful run of {\LaTeX} and friends. wenzelm@12464: Note that a separate copy of the sources may be retained by passing an option wenzelm@12464: \texttt{-D} to the \texttt{usedir} utility when running the session (see also wenzelm@12464: \S\ref{sec:tool-usedir}). wenzelm@12464: wenzelm@12464: wenzelm@12464: \section{Running {\LaTeX} within the Isabelle environment --- \texttt{isatool latex}} wenzelm@12464: \label{sec:tool-latex} wenzelm@12464: wenzelm@12464: The \tooldx{latex} utility provides the basic interface for Isabelle document wenzelm@12464: preparation. Its usage is: wenzelm@12464: \begin{ttbox} wenzelm@12464: Usage: latex [OPTIONS] [FILE] wenzelm@12464: wenzelm@12464: Options are: wenzelm@12464: -o FORMAT specify output format: dvi (default), dvi.gz, ps, wenzelm@26908: ps.gz, pdf, bbl, idx, sty, syms wenzelm@12464: wenzelm@12464: Run LaTeX (and related tools) on FILE (default root.tex), wenzelm@12464: producing the specified output format. wenzelm@12464: \end{ttbox} wenzelm@26908: Appropriate {\LaTeX}-related programs are run on the input file, wenzelm@26908: according to the given output format: \texttt{latex}, wenzelm@26908: \texttt{pdflatex}, \texttt{dvips}, \texttt{bibtex} (for \texttt{bbl}), wenzelm@26908: and \texttt{makeindex} (for \texttt{idx}). The actual commands are wenzelm@26908: determined from the settings environment (\texttt{ISABELLE_LATEX} wenzelm@26908: etc., see \S\ref{sec:settings}). wenzelm@12464: wenzelm@12464: The \texttt{sty} output format causes the Isabelle style files to be updated wenzelm@12464: from the distribution. This is useful in special situations where the wenzelm@12464: document sources are to be processed another time by separate tools (cf.\ wenzelm@12464: option \texttt{-D} of the \texttt{usedir} utility, see wenzelm@12464: \S\ref{sec:tool-usedir}). wenzelm@12464: wenzelm@14921: The \texttt{syms} output is for internal use; it generates lists of symbols wenzelm@14921: that are available without loading additional {\LaTeX} packages. wenzelm@14921: wenzelm@12464: wenzelm@12464: \subsubsection*{Examples} wenzelm@12464: wenzelm@12464: Invoking \texttt{isatool latex} by hand may be occasionally useful when wenzelm@12464: debugging failed attempts of the automatic document preparation stage of wenzelm@12464: batch-mode Isabelle. The abortive process leaves the sources at a certain wenzelm@12464: place within \texttt{ISABELLE_BROWSER_INFO}, see the runtime error message for wenzelm@12464: details. This enables users to inspect {\LaTeX} runs in further detail, e.g.\ wenzelm@12464: like this: wenzelm@12464: wenzelm@12464: \begin{ttbox} wenzelm@12464: cd ~/isabelle/browser_info/HOL/Test/document wenzelm@12464: isatool latex -o pdf wenzelm@12464: \end{ttbox} wenzelm@12464: wenzelm@12464: wenzelm@5364: %%% Local Variables: wenzelm@5364: %%% mode: latex wenzelm@5364: %%% TeX-master: "system" wenzelm@5364: %%% End: