
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,\<forall>,) 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: 




