doc-src/System/misc.tex

modernized specifications and proofs;

% $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 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: