doc-src/System/misc.tex

proper bootstrap of HOL theory and packages;

% $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{Getting 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} and \texttt{ML_PLATFORM}. 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{$name$\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}
Here we have 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{Installing standalone Isabelle executables -- \texttt{isatool install}}

Usually, the Isabelle binaries (\texttt{isabelle}, \texttt{isatool} etc.) are
just run from their location within the distribution directory, probably
indirectly by the shell through its \texttt{PATH}.  Other schemes of
installation are supported by the \tooldx{install} utility:
\begin{ttbox}
Usage: install [OPTIONS]

  Options are:
    -d DISTDIR   use DISTDIR as Isabelle distribution (default ISABELLE_HOME)
    -k           install KDE application icon on Desktop
    -p DIR       install standalone binaries in DIR

  Install Isabelle executables with absolute references to the current
  distribution directory.
\end{ttbox}

The \texttt{-d} option overrides the current Isabelle distribution directory
as determined by \texttt{ISABELLE_HOME}.

The \texttt{-p} option installs executable wrapper scripts for
\texttt{isabelle}, \texttt{isatool}, \texttt{Isabelle}, containing proper
absolute references to the Isabelle distribution directory.  A typical
\texttt{DIR} specification would be some directory expected to be in the
shell's \texttt{PATH}, such as \texttt{/usr/local/bin}.  It is important to
note that a plain manual copy of the original Isabelle executables just would
not work!

The \texttt{-k} option creates an Isabelle application object for the K
desktop environment.  The icon will appear directly on Desktop.


\section{Creating instances of the Isabelle logo -- \texttt{isatool
    logo}}

The \tooldx{logo} utility creates any instance of the generic Isabelle logo as
an Encapsuled Postscript file (EPS):
\begin{ttbox}
Usage: logo [OPTIONS] NAME

  Create instance NAME of the Isabelle logo (as EPS).

  Options are:
    -o OUTFILE   set output file (default determined from NAME)
    -q           quiet mode
\end{ttbox}
You are encouraged to use this to create a derived logo for your Isabelle
project.  For example, \texttt{isatool logo HOOL} creates
\texttt{isabelle_hool.eps}.


\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 local logic
images, while the \texttt{test} target shall build all related
examples.  The \texttt{all} target shall do \texttt{images} and
\texttt{test}.


\subsection*{Examples}

Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
object-logics as a model for your own developements.  For example, see
\texttt{src/FOL/IsaMakefile}.


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

The \tooldx{makeall} utility applies Isabelle make to all logic
directories of the 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 each
\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 with THIS_IS_ISABELLE_BUILD indication
    -P PATH      set path for remote theory browsing information
    -b           build mode (output heap image, using current dir)
    -i BOOL      generate theory browsing information,
                 i.e. HTML / graph data (default false)
    -r           reset session path
    -s NAME      override session NAME

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

Note that 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.  The \texttt{-B} option is like
\texttt{-b}, but also indicates \texttt{THIS_IS_ISABELLE_BUILD=true} via the
process environment.  This usually causes the \texttt{ISABELLE\_OUTPUT} and
\texttt{ISABELLE_BROWSER_INFO} settings to refer to some location within the
Isabelle distribution directory, rather than the user's home directory.

In example mode, \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}.  It assumes that 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 explicitly turned on or off --- the last occurrence of \texttt{-i} on
the command line wins.  The \texttt{-P} option specifies a path (or actual
URL) to be prefixed to any \emph{non-local} reference of existing theories.
Thus user sessions may easily link to existing Isabelle libraries already
present on the WWW.

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


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "system"
%%% End: