% $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}
\medskip 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{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{Run Isabelle with plain tty interaction --- \texttt{isatool tty}} \label{sec:tool-tty}
The \tooldx{tty} utility runs the Isabelle process interactively
within a plain terminal session:
\begin{ttbox}
Usage: tty [OPTIONS]
Options are:
-l NAME logic image name (default ISABELLE_LOGIC)
-m MODE add print mode for output
-p NAME line editor program name (default ISABELLE_LINE_EDITOR)
Run Isabelle process with plain tty interaction, and optional line editor.
\end{ttbox}
The \texttt{-l} option specifies the logic image. The \texttt{-m}
option specifies additional print modes. The The \texttt{-p} option
specifies an alternative line editor (such as the \texttt{rlwrap}
wrapper for GNU readline); the fall-back is to use raw standard input.
\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 full version string of the
Isabelle distribution being used, e.g.\ ``\texttt{Isabelle2007:
November 2007}''. There are no options nor arguments.
\section{Convert XML to YXML --- \texttt{isatool yxml}}
The \tooldx{yxml} utility converts a standard XML document (stdin) to
the much simpler and more efficient YXML format of Isabelle (stdout).
The YXML format is defined as follows.
\begin{enumerate}
\item The encoding is always UTF-8.
\item Body text is represented verbatim (no escaping, no special
treatment of white space, no named entities, no CDATA chunks, no
comments).
\item Markup elements are represented via ASCII control characters $X
= 5$ and $Y = 6$ as follows:
\begin{tabular}{ll}
XML & YXML \\\hline
\verb,<,\emph{name}~\emph{attribute}\verb,=,\emph{value}~\dots\verb,>, &
\emph{X\,Y\,name\,Y\,attribute}\verb,=,\emph{value}\dots\emph{X} \\
\verb,</,\emph{name}\verb,>, & \emph{X\,Y\,X} \\
\end{tabular}
There is no special case for empty body text, i.e.\ \verb,<foo/>, is
treated like \verb,<foo></foo>,. Also note that \emph{X} and
\emph{Y} may never occur in well-formed XML documents.
\end{enumerate}
Parsing YXML is pretty straight-forward: split the text into chunks separated
by \emph{X}, then split each chunk into sub-chunks separated by \emph{Y}.
Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
indicates close of an element. Any other non-empty chunk consists of plain
text.
YXML documents may be detected quickly by checking that the first two
characters are \emph{X\,Y}.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"
%%% End: