doc-src/System/misc.tex

under construction;

% $Id$

\chapter{Miscellaneous 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 set in
\texttt{DVI_VIEWER}.


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

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

  Expand shorthand goal commands in FILES.  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 supplied as arguments, all occurrences of the shorthand
commands \texttt{br}, \texttt{be} etc.\ are replaced with the
corresponding full commands.  Shorthand commands should appear one per
line.  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-1.09}
{\out ML_HOME=/usr/local/sml109.27/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-1.09:/proj/isabelle/heaps/smlnj-1.09}
\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}.



\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:
%FIXME
%    -g BOOL      generate theory graph data (default false)
\begin{ttbox}
Usage: isatool usedir LOGIC NAME

  Options are:
    -b           build mode (output heap image, use dir ".")
    -h BOOL      generate theory HTML 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
implicitely 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}

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

Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with
input image \texttt{LOGIC} and output to \texttt{NAME}, as provided as
arguments. This will be a batch session, executing just
\texttt{use_dir".";}\index{*use_dir}, and then quitting. It is assumed
that there is a file \texttt{ROOT.ML} in the current directory
containing 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 does an
automatic \texttt{use_dir"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{-h} option controls HTML browsing data
generation. It may be explicitely turned on or off --- the last
occurrence of some \texttt{-h} on the command line wins.

\medskip Any \texttt{usedir} session is named by some \emph{session
  identifier}. These may accumulate, documenting the way sessions
depend on others. For example, consider \texttt{Pure/FOL/ZF/ex}, which
refers 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 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.