doc-src/System/misc.tex

updated to Isabelle98;

% $Id$

\chapter{Miscellaneous tools} \label{ch:tools}

Subsequently we describe various Isabelle related utilities --- in
alphabetical order.


\section{Viewing documentation --- \texttt{isatool doc}} \label{sec:tool-doc}

The \tooldx{doc} utility displays online documentation:
\begin{ttbox}
Usage: isatool doc [DOC]

  View Isabelle documentation DOC, or show list of available documents.
\end{ttbox}
If called without arguments, it lists all available documents. Each
line starts with an identifier, followed by some comment. Any of these
identifiers may be specified as the first argument in order to have
the corresponding document displayed.

\medskip The \texttt{ISABELLE_DOCS} setting specifies the list of
directories (separated by colons) to be scanned for documentations.
The program for viewing \texttt{dvi} files is determined by the
\texttt{DVI_VIEWER} setting.


\section{Tuning proof scripts --- \texttt{isatool expandshort}}

The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance
readability:
\begin{ttbox}
Usage: expandshort [FILES|DIRS...]

  Recursively find .ML files, expand shorthand goal commands.
  Also contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
  rewrite_goals_tac on 1-element lists; furthermore expands tabs,
  since they are now forbidden in ML string constants.

  Renames old versions of files by appending "~~".
\end{ttbox}
In the files or directories supplied as arguments, all occurrences of
the shorthand commands \texttt{br}, \texttt{be} etc.\ in proof scripts
are replaced with the corresponding full commands.  The old versions
of the files are renamed to have the suffix~\verb'~~'.


\section{Get logic images --- \texttt{isatool findlogics}}

The \tooldx{findlogics} utility traverses all directories specified in
\texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage
is:
\begin{ttbox}
Usage: isatool findlogics

  Collect heap file names from ISABELLE_PATH.
\end{ttbox}
The base names of all files found on the path are printed --- sorted
and with duplicates removed. Also note that \texttt{ISABELLE_PATH}
implicitly depends upon \texttt{ML_SYSTEM}. Thus switching to another
{\ML} compiler may change the set of logic images available.


\section{Inspecting the settings environment -- \texttt{isatool getenv}}
\label{sec:tool-getenv}

The Isabelle settings environment --- as provided by the site-default
and user-specific settings files --- can be inspected with the
\tooldx{getenv} utility:
\begin{ttbox}
Usage: isatool getenv [OPTIONS] [VARNAMES ...]

  Options are:
    -a           display complete environment
    -b           print values only (doesn't work for -a)

  Get value of VARNAMES from the Isabelle settings.
\end{ttbox}

With the \texttt{-a} option, one may inspect the full process
environment that Isabelle related programs are run in. This usually
contains much more variables than are actually Isabelle settings.
Normally, output is a list of lines of the form
\mbox{$varname$\texttt{=}$value$}. The \texttt{-b} option causes only
the values to be printed.


\subsection*{Examples}

Get the {\ML} system identifier and the location where the compiler
binaries are supposed to reside as follows:
\begin{ttbox}
isatool getenv ML_SYSTEM ML_HOME
{\out ML_SYSTEM=smlnj-110}
{\out ML_HOME=/usr/local/smlnj-110/bin}
\end{ttbox}

The next one peeks at the search path that \texttt{isabelle} uses to
locate logic images:
\begin{ttbox}
isatool getenv -b ISABELLE_PATH
{\out /home/me/isabelle/heaps/smlnj-110:/usr/local/isabelle/heaps/smlnj-110}
\end{ttbox}
We used the \texttt{-b} option to suppress the \texttt{ISABELLE_PATH=}
prefix.  The value above is what became of the following assignment in
the default settings file:
\begin{ttbox}
ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps
\end{ttbox}
Note how the \texttt{ML_SYSTEM} value got appended automatically to
each path component. This is a special feature of
\texttt{ISABELLE_PATH} (and also of \texttt{ISABELLE_OUTPUT}).


\section{Isabelle's version of make --- \texttt{isatool make}}

The Isabelle \tooldx{make} utility is a very simple wrapper for
ordinary Unix \texttt{make}:
\begin{ttbox}
Usage: isatool make [ARGS ...]

  Compiles logic in current directory using IsaMakefile.
  ARGS are directly passed to the system make program.
\end{ttbox}
Note that the Isabelle settings environment is also active. Thus one
may refer to its values within the \ttindex{IsaMakefile}, e.g.\ 
\texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the
make file also inherit this environment.  Typically,
\texttt{IsaMakefile}s defer the real work to the \texttt{usedir}
utility, see \S\ref{sec:tool-usedir}.

\medskip The basic \texttt{IsaMakefile} convention is that the default
target builds the actual logic, including its parents if appropriate.
The \texttt{images} target is intended to build all logic images,
while the \texttt{test} target shall build all related examples.  The
\texttt{all} target shall build the images and run the examples.


\subsection*{Examples}

Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
object-logics as a model for your own developements.


\section{Make all logics -- \texttt{isatool makeall}}

The \tooldx{makeall} utility applies Isabelle make to all logic
directories of the Isabelle distribution:
\begin{ttbox}
Usage: makeall [ARGS ...]

  Apply isatool make to all logics (passing ARGS).
\end{ttbox}
The arguments \texttt{ARGS} are just passed verbatim to any
\texttt{make} invocation.


\section{Running complete logics --- \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:
\begin{ttbox}
Usage: usedir LOGIC NAME

  Options are:
    -b           build mode (output heap image, use dir ".")
    -i BOOL      generate theory browsing information,
                 i.e. HTML / graph data (default false)
    -s NAME      override session NAME

  Build object-logic or run examples. Also creates browsing
  information (HTML etc.) according to settings.
\end{ttbox}

The value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
implicitly prefixed to \emph{any} \texttt{usedir} call. Since the
\ttindex{IsaMakefile}s of all object-logics distributed with Isabelle
just invoke \texttt{usedir} for the real work, one may control
compilation options globally via above variable. In particular,
generation of \rmindex{HTML} browsing information is enabled or
disabled this way.


\subsection*{Options}

Basically, there are two different modes of operation: \emph{build
  mode} (enabled through the \texttt{-b} option) and \emph{example
  mode} (default).

Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with
input image \texttt{LOGIC} and output to \texttt{NAME}, as provided on
the command line. This will be a batch session, running
\texttt{ROOT.ML} from the current directory and then quitting.  It is
assumed that \texttt{ROOT.ML} contains all {\ML} commands required to
build the logic.

In example mode, on the other hand, \texttt{usedir} runs a read-only
session of \texttt{LOGIC} (typically just built before) and
automatically runs \texttt{ROOT.ML} from within directory
\texttt{NAME}.  I.e.\ it assumes that some file \texttt{ROOT.ML} in
directory \texttt{NAME} contains appropriate {\ML} commands to run the
desired examples.

\medskip The \texttt{-i} option controls theory browsing data
generation. It may be explicitely turned on or off --- the last
occurrence of some \texttt{-i} on the command line wins.

\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/ZF/ex}, which refers
to the examples of {\ZF} set theory, built upon {\FOL}, built upon
{\Pure}.

The current session's identifier is by default just the base name of
the \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME}
argument (in example mode). This may be overridden explicitely via the
\texttt{-s} option.


\subsection*{Examples}

Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
object-logics as a model for your own developements.