doc-src/System/misc.tex

lin_arith_prover splits certain operators (e.g. min, max, abs)

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