doc-src/System/misc.tex

added isatool logo;

% $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}. 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 binaries -- \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}.
In some cases, though, another more traditional installation scheme
might be preferably where executables are put into some global system
directory (like \texttt{/usr/local/bin}).

Doing a plain copy of the Isabelle executables just would not work,
though.  One should use the \tooldx{install} utility instead:
\begin{ttbox}
Usage: install BINDIR

  Options are:
    -d DISTDIR   use DISTDIR as Isabelle distribution
                 (default ISABELLE_HOME)

  Install standalone Isabelle binaries in directory BINDIR with absolute
  references to DISTDIR/bin, which becomes non-relocatable this way.
\end{ttbox}

This installs standalone executables in \texttt{BINDIR} containing
absolute references to \texttt{DISTDIR} (the default is
\texttt{ISABELLE_HOME} as figured out by the current \texttt{isatool}
invocation).  While the generated scripts themselves may be relocated
afterwards, they cease working if the referenced Isabelle distribution
is moved somewhere else.  Here is an example use of \texttt{install}:
\begin{ttbox}
  isatool install /usr/local/bin
\end{ttbox}


\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 (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}

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.

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}.  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 explicitely turned on or off --- the last
occurrence of \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/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: