% $Id$
\chapter{Miscellaneous tools} \label{ch:tools}
Subsequently we describe various Isabelle related utilities, given in
alphabetical order.
\section{Converting legacy ML scripts --- \texttt{isatool convert}}
The \tooldx{convert} utility assists in converting legacy ML proof scripts
into the new-style format of Isabelle/Isar:
\begin{ttbox}
Usage: convert [FILES|DIRS...]
Recursively find .ML files, converting legacy tactic scripts to
Isabelle/Isar tactic emulation.
Note: conversion is only approximated, based on some heuristics.
Renames old versions of FILES by appending "~0~".
Creates new versions of FILES by appending ".thy".
\end{ttbox}
The resulting theory text uses the tactic emulation facilities of
Isabelle/Isar (see also \cite{isabelle-ref}, especially the ``Conversion
guide'' in the appendix). Usually there is some manual tuning required to get
an automatically converted script work again --- the success rate is around
99\% for common ML scripts.
\section{Displaying documents --- \texttt{isatool display}}
The \tooldx{display} utility displays documents in DVI format:
\begin{ttbox}
Usage: display [OPTIONS] FILE
Options are:
-c cleanup -- remove FILE after use
Display document FILE (in DVI format).
\end{ttbox}
The \texttt{-c} option causes the input file to be removed after use. The
program for viewing \texttt{dvi} files is determined by the
\texttt{DVI_VIEWER} setting.
\section{Viewing documentation --- \texttt{isatool doc}} \label{sec:tool-doc}
The \tooldx{doc} utility displays online documentation:
\begin{ttbox}
Usage: 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 a short description. 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,
forward_tac, rewrite_goals_tac on 1-element lists; furthermore
expands tabs, which are forbidden in SML 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: 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 lookup in \texttt{ISABELLE_PATH} includes
the current values of \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: 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 name and the location where the compiler binaries are
supposed to reside as follows:
\begin{ttbox}
isatool getenv ML_SYSTEM ML_HOME
{\out ML_SYSTEM=polyml}
{\out ML_HOME=/usr/share/polyml/x86-linux}
\end{ttbox}
The next one peeks at the output directory for \texttt{isabelle} logic images:
\begin{ttbox}
isatool getenv -b ISABELLE_OUTPUT
{\out /home/me/isabelle/heaps/polyml_x86-linux}
\end{ttbox}
Here we have used the \texttt{-b} option to suppress the
\texttt{ISABELLE_OUTPUT=} prefix. The value above is what became of the
following assignment in the default settings file:
\begin{ttbox}
ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps"
\end{ttbox}
Note how the \texttt{ML_IDENTIFIER} value got appended automatically to each
path component. This is a special feature of \texttt{ISABELLE_OUTPUT}.
\section{Installing standalone Isabelle executables --- \texttt{isatool install}}
\label{sec:tool-install}
By default, 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)
-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!
\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 Bali} creates
\texttt{isabelle_bali.eps}.
\section{Isabelle's version of make --- \texttt{isatool make}}
\label{sec:tool-make}
The Isabelle \tooldx{make} utility is a very simple wrapper for
ordinary Unix \texttt{make}:
\begin{ttbox}
Usage: make [ARGS ...]
Compile the 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 developments. 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{Printing documents --- \texttt{isatool print}}
The \tooldx{print} utility prints documents:
\begin{ttbox}
Usage: print [OPTIONS] FILE
Options are:
-c cleanup -- remove FILE after use
Print document FILE.
\end{ttbox}
The \texttt{-c} option causes the input file to be removed after use. The
printer spool command is determined by the \texttt{PRINT_COMMAND} setting.
\section{Remove awkward symbol names from theory sources --- \texttt{isatool unsymbolize}}
The \tooldx{unsymbolize} utility tunes Isabelle theory sources to improve
readability for plain ASCII output (e.g.\ in email communication). Most
notably, \texttt{unsymbolize} replaces awkward arrow symbols such as
\verb|\<Longrightarrow>| by \verb|==>|.
\begin{ttbox}
Usage: unsymbolize [FILES|DIRS...]
Recursively find .thy/.ML files, removing unreadable symbol names.
Note: this is an ad-hoc script; there is no systematic way to replace
symbols independently of the inner syntax of a theory!
Renames old versions of FILES by appending "~~".
\end{ttbox}
\section{Output the version identifier of the Isabelle distribution --- \texttt{isatool version}}
The \tooldx{version} utility outputs the version identifier of the Isabelle
distribution being used, e.g.\ \texttt{Isabelle2005}. There are no options
nor arguments.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"
%%% End: