doc-src/System/misc.tex
author wenzelm
Sat May 17 13:54:30 2008 +0200 (2008-05-17)
changeset 26928 ca87aff1ad2d
parent 26581 ed7f995b3c97
child 27348 ca9fa1844fd6
permissions -rw-r--r--
structure Display: less pervasive operations;
wenzelm@3188
     1
wenzelm@3188
     2
% $Id$
wenzelm@3188
     3
wenzelm@3278
     4
\chapter{Miscellaneous tools} \label{ch:tools}
wenzelm@3188
     5
wenzelm@11031
     6
Subsequently we describe various Isabelle related utilities, given in
wenzelm@3217
     7
alphabetical order.
wenzelm@3217
     8
wenzelm@3217
     9
wenzelm@11031
    10
\section{Converting legacy ML scripts --- \texttt{isatool convert}}
wenzelm@11031
    11
wenzelm@11031
    12
The \tooldx{convert} utility assists in converting legacy ML proof scripts
wenzelm@11031
    13
into the new-style format of Isabelle/Isar:
wenzelm@11031
    14
\begin{ttbox}
wenzelm@11031
    15
Usage: convert [FILES|DIRS...]
wenzelm@11031
    16
wenzelm@11031
    17
  Recursively find .ML files, converting legacy tactic scripts to
wenzelm@11031
    18
  Isabelle/Isar tactic emulation.
wenzelm@11031
    19
  Note: conversion is only approximated, based on some heuristics.
wenzelm@11031
    20
wenzelm@11031
    21
  Renames old versions of FILES by appending "~0~".
wenzelm@11031
    22
  Creates new versions of FILES by appending ".thy".
wenzelm@11031
    23
\end{ttbox}
wenzelm@11031
    24
The resulting theory text uses the tactic emulation facilities of
wenzelm@11031
    25
Isabelle/Isar (see also \cite{isabelle-ref}, especially the ``Conversion
wenzelm@11031
    26
guide'' in the appendix).  Usually there is some manual tuning required to get
wenzelm@12464
    27
an automatically converted script work again --- the success rate is around
wenzelm@12464
    28
99\% for common ML scripts.
wenzelm@11031
    29
wenzelm@11031
    30
wenzelm@14932
    31
\section{Displaying documents --- \texttt{isatool display}}
wenzelm@14932
    32
wenzelm@14932
    33
The \tooldx{display} utility displays documents in DVI format:
wenzelm@14932
    34
\begin{ttbox}
wenzelm@14932
    35
Usage: display [OPTIONS] FILE
wenzelm@14932
    36
wenzelm@14932
    37
  Options are:
wenzelm@14932
    38
    -c           cleanup -- remove FILE after use
wenzelm@14932
    39
wenzelm@14932
    40
  Display document FILE (in DVI format).
wenzelm@14932
    41
\end{ttbox}
wenzelm@14932
    42
wenzelm@20572
    43
\medskip The \texttt{-c} option causes the input file to be removed after use.
wenzelm@20572
    44
The program for viewing \texttt{dvi} files is determined by the
wenzelm@14932
    45
\texttt{DVI_VIEWER} setting.
wenzelm@14932
    46
wenzelm@14932
    47
wenzelm@3217
    48
\section{Viewing documentation --- \texttt{isatool doc}} \label{sec:tool-doc}
wenzelm@3217
    49
wenzelm@3217
    50
The \tooldx{doc} utility displays online documentation:
wenzelm@3217
    51
\begin{ttbox}
wenzelm@13047
    52
Usage: doc [DOC]
wenzelm@3217
    53
wenzelm@3217
    54
  View Isabelle documentation DOC, or show list of available documents.
wenzelm@3217
    55
\end{ttbox}
wenzelm@7882
    56
If called without arguments, it lists all available documents. Each line
wenzelm@7882
    57
starts with an identifier, followed by a short description. Any of these
wenzelm@7882
    58
identifiers may be specified as the first argument in order to have the
wenzelm@7882
    59
corresponding document displayed.
wenzelm@3217
    60
wenzelm@7882
    61
\medskip The \texttt{ISABELLE_DOCS} setting specifies the list of directories
wenzelm@7882
    62
(separated by colons) to be scanned for documentations.  The program for
wenzelm@7882
    63
viewing \texttt{dvi} files is determined by the \texttt{DVI_VIEWER} setting.
wenzelm@3217
    64
wenzelm@3217
    65
wenzelm@5366
    66
\section{Getting logic images --- \texttt{isatool findlogics}}
wenzelm@3217
    67
wenzelm@3217
    68
The \tooldx{findlogics} utility traverses all directories specified in
wenzelm@7882
    69
\texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage is:
wenzelm@3217
    70
\begin{ttbox}
wenzelm@13047
    71
Usage: findlogics
wenzelm@3217
    72
wenzelm@3217
    73
  Collect heap file names from ISABELLE_PATH.
wenzelm@3217
    74
\end{ttbox}
wenzelm@6414
    75
The base names of all files found on the path are printed --- sorted and with
wenzelm@9790
    76
duplicates removed. Also note that lookup in \texttt{ISABELLE_PATH} includes
wenzelm@9790
    77
the current values of \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM}. Thus
wenzelm@9790
    78
switching to another {\ML} compiler may change the set of logic images
wenzelm@9790
    79
available.
wenzelm@3217
    80
wenzelm@3188
    81
wenzelm@12464
    82
\section{Inspecting the settings environment --- \texttt{isatool getenv}}
wenzelm@3188
    83
\label{sec:tool-getenv}
wenzelm@3188
    84
wenzelm@7882
    85
The Isabelle settings environment --- as provided by the site-default and
wenzelm@7882
    86
user-specific settings files --- can be inspected with the \tooldx{getenv}
wenzelm@7882
    87
utility:
wenzelm@3188
    88
\begin{ttbox}
wenzelm@13047
    89
Usage: getenv [OPTIONS] [VARNAMES ...]
wenzelm@3188
    90
wenzelm@3188
    91
  Options are:
wenzelm@3188
    92
    -a           display complete environment
wenzelm@3188
    93
    -b           print values only (doesn't work for -a)
wenzelm@3188
    94
wenzelm@3188
    95
  Get value of VARNAMES from the Isabelle settings.
wenzelm@3188
    96
\end{ttbox}
wenzelm@3188
    97
wenzelm@7882
    98
With the \texttt{-a} option, one may inspect the full process environment that
wenzelm@7882
    99
Isabelle related programs are run in. This usually contains much more
wenzelm@7882
   100
variables than are actually Isabelle settings.  Normally, output is a list of
wenzelm@7882
   101
lines of the form \mbox{$name$\texttt{=}$value$}. The \texttt{-b} option
wenzelm@7882
   102
causes only the values to be printed.
wenzelm@3188
   103
wenzelm@3188
   104
wenzelm@3188
   105
\subsection*{Examples}
wenzelm@3188
   106
wenzelm@9790
   107
Get the {\ML} system name and the location where the compiler binaries are
wenzelm@9790
   108
supposed to reside as follows:
wenzelm@3188
   109
\begin{ttbox}
wenzelm@3188
   110
isatool getenv ML_SYSTEM ML_HOME
wenzelm@9790
   111
{\out ML_SYSTEM=polyml}
wenzelm@9790
   112
{\out ML_HOME=/usr/share/polyml/x86-linux}
wenzelm@3188
   113
\end{ttbox}
wenzelm@3188
   114
wenzelm@9790
   115
The next one peeks at the output directory for \texttt{isabelle} logic images:
wenzelm@3188
   116
\begin{ttbox}
wenzelm@9790
   117
isatool getenv -b ISABELLE_OUTPUT
wenzelm@9790
   118
{\out /home/me/isabelle/heaps/polyml_x86-linux}
wenzelm@3188
   119
\end{ttbox}
wenzelm@4555
   120
Here we have used the \texttt{-b} option to suppress the
wenzelm@9790
   121
\texttt{ISABELLE_OUTPUT=} prefix.  The value above is what became of the
wenzelm@4555
   122
following assignment in the default settings file:
wenzelm@3188
   123
\begin{ttbox}
wenzelm@9790
   124
ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps"
wenzelm@3188
   125
\end{ttbox}
wenzelm@9790
   126
Note how the \texttt{ML_IDENTIFIER} value got appended automatically to each
wenzelm@9790
   127
path component. This is a special feature of \texttt{ISABELLE_OUTPUT}.
wenzelm@3188
   128
wenzelm@3188
   129
wenzelm@12464
   130
\section{Installing standalone Isabelle executables --- \texttt{isatool install}}
wenzelm@7882
   131
\label{sec:tool-install}
wenzelm@5366
   132
wenzelm@7882
   133
By default, the Isabelle binaries (\texttt{isabelle}, \texttt{isatool} etc.)
wenzelm@7882
   134
are just run from their location within the distribution directory, probably
wenzelm@6418
   135
indirectly by the shell through its \texttt{PATH}.  Other schemes of
wenzelm@6418
   136
installation are supported by the \tooldx{install} utility:
wenzelm@5366
   137
\begin{ttbox}
wenzelm@6418
   138
Usage: install [OPTIONS]
wenzelm@5366
   139
wenzelm@5405
   140
  Options are:
wenzelm@7883
   141
    -d DISTDIR   use DISTDIR as Isabelle distribution
wenzelm@7883
   142
                 (default ISABELLE_HOME)
wenzelm@6418
   143
    -p DIR       install standalone binaries in DIR
wenzelm@5405
   144
wenzelm@6418
   145
  Install Isabelle executables with absolute references to the current
wenzelm@6418
   146
  distribution directory.
wenzelm@5366
   147
\end{ttbox}
wenzelm@5366
   148
wenzelm@6418
   149
The \texttt{-d} option overrides the current Isabelle distribution directory
wenzelm@6418
   150
as determined by \texttt{ISABELLE_HOME}.
wenzelm@6418
   151
wenzelm@6418
   152
The \texttt{-p} option installs executable wrapper scripts for
wenzelm@6418
   153
\texttt{isabelle}, \texttt{isatool}, \texttt{Isabelle}, containing proper
wenzelm@6418
   154
absolute references to the Isabelle distribution directory.  A typical
wenzelm@6418
   155
\texttt{DIR} specification would be some directory expected to be in the
wenzelm@6418
   156
shell's \texttt{PATH}, such as \texttt{/usr/local/bin}.  It is important to
wenzelm@6418
   157
note that a plain manual copy of the original Isabelle executables just would
wenzelm@6418
   158
not work!
wenzelm@6418
   159
wenzelm@5366
   160
wenzelm@12464
   161
\section{Creating instances of the Isabelle logo --- \texttt{isatool
wenzelm@5571
   162
    logo}}
wenzelm@5571
   163
wenzelm@5571
   164
The \tooldx{logo} utility creates any instance of the generic Isabelle logo as
wenzelm@5571
   165
an Encapsuled Postscript file (EPS):
wenzelm@5571
   166
\begin{ttbox}
wenzelm@5571
   167
Usage: logo [OPTIONS] NAME
wenzelm@5571
   168
wenzelm@5571
   169
  Create instance NAME of the Isabelle logo (as EPS).
wenzelm@5571
   170
wenzelm@5571
   171
  Options are:
wenzelm@5571
   172
    -o OUTFILE   set output file (default determined from NAME)
wenzelm@5571
   173
    -q           quiet mode
wenzelm@5571
   174
\end{ttbox}
wenzelm@5571
   175
You are encouraged to use this to create a derived logo for your Isabelle
wenzelm@13047
   176
project.  For example, \texttt{isatool logo Bali} creates
wenzelm@13047
   177
\texttt{isabelle_bali.eps}.
wenzelm@5571
   178
wenzelm@5571
   179
wenzelm@3188
   180
\section{Isabelle's version of make --- \texttt{isatool make}}
wenzelm@11616
   181
\label{sec:tool-make}
wenzelm@3188
   182
wenzelm@3217
   183
The Isabelle \tooldx{make} utility is a very simple wrapper for
wenzelm@3217
   184
ordinary Unix \texttt{make}:
wenzelm@3188
   185
\begin{ttbox}
wenzelm@13047
   186
Usage: make [ARGS ...]
wenzelm@3188
   187
wenzelm@7801
   188
  Compile the logic in current directory using IsaMakefile.
wenzelm@3188
   189
  ARGS are directly passed to the system make program.
wenzelm@3188
   190
\end{ttbox}
wenzelm@3217
   191
Note that the Isabelle settings environment is also active. Thus one
wenzelm@3278
   192
may refer to its values within the \ttindex{IsaMakefile}, e.g.\ 
wenzelm@3217
   193
\texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the
wenzelm@3278
   194
make file also inherit this environment.  Typically,
wenzelm@3278
   195
\texttt{IsaMakefile}s defer the real work to the \texttt{usedir}
wenzelm@3278
   196
utility, see \S\ref{sec:tool-usedir}.
wenzelm@3217
   197
wenzelm@3278
   198
\medskip The basic \texttt{IsaMakefile} convention is that the default
wenzelm@4540
   199
target builds the actual logic, including its parents if appropriate.
wenzelm@4555
   200
The \texttt{images} target is intended to build all local logic
wenzelm@4555
   201
images, while the \texttt{test} target shall build all related
wenzelm@4555
   202
examples.  The \texttt{all} target shall do \texttt{images} and
wenzelm@4555
   203
\texttt{test}.
wenzelm@4540
   204
wenzelm@4540
   205
wenzelm@4540
   206
\subsection*{Examples}
wenzelm@4540
   207
wenzelm@4540
   208
Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
wenzelm@13047
   209
object-logics as a model for your own developments.  For example, see
wenzelm@4555
   210
\texttt{src/FOL/IsaMakefile}.
wenzelm@4540
   211
wenzelm@4540
   212
wenzelm@12464
   213
\section{Make all logics --- \texttt{isatool makeall}}
wenzelm@4540
   214
wenzelm@4540
   215
The \tooldx{makeall} utility applies Isabelle make to all logic
wenzelm@4555
   216
directories of the distribution:
wenzelm@4540
   217
\begin{ttbox}
wenzelm@4540
   218
Usage: makeall [ARGS ...]
wenzelm@4540
   219
wenzelm@4540
   220
  Apply isatool make to all logics (passing ARGS).
wenzelm@4540
   221
\end{ttbox}
wenzelm@4555
   222
The arguments \texttt{ARGS} are just passed verbatim to each
wenzelm@4540
   223
\texttt{make} invocation.
wenzelm@3188
   224
wenzelm@12464
   225
wenzelm@14932
   226
\section{Printing documents --- \texttt{isatool print}}
wenzelm@14932
   227
wenzelm@14932
   228
The \tooldx{print} utility prints documents:
wenzelm@14932
   229
\begin{ttbox}
wenzelm@14932
   230
Usage: print [OPTIONS] FILE
wenzelm@14932
   231
wenzelm@14932
   232
  Options are:
wenzelm@14932
   233
    -c           cleanup -- remove FILE after use
wenzelm@14932
   234
wenzelm@14932
   235
  Print document FILE.
wenzelm@14932
   236
\end{ttbox}
wenzelm@14932
   237
wenzelm@14932
   238
The \texttt{-c} option causes the input file to be removed after use.  The
wenzelm@14932
   239
printer spool command is determined by the \texttt{PRINT_COMMAND} setting.
wenzelm@14932
   240
wenzelm@14932
   241
wenzelm@25629
   242
\section{Run Isabelle with plain tty interaction --- \texttt{isatool tty}} \label{sec:tool-tty}
wenzelm@25629
   243
wenzelm@25629
   244
The \tooldx{tty} utility runs the Isabelle process interactively
wenzelm@25629
   245
within a plain terminal session:
wenzelm@25629
   246
\begin{ttbox}
wenzelm@25629
   247
Usage: tty [OPTIONS]
wenzelm@25629
   248
wenzelm@25629
   249
  Options are:
wenzelm@25629
   250
    -l NAME      logic image name (default ISABELLE_LOGIC)
wenzelm@25629
   251
    -m MODE      add print mode for output
wenzelm@25629
   252
    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
wenzelm@25629
   253
wenzelm@25629
   254
  Run Isabelle process with plain tty interaction, and optional line editor.
wenzelm@25629
   255
\end{ttbox}
wenzelm@25629
   256
wenzelm@25629
   257
The \texttt{-l} option specifies the logic image.  The \texttt{-m}
wenzelm@25629
   258
option specifies additional print modes.  The The \texttt{-p} option
wenzelm@25629
   259
specifies an alternative line editor (such as the \texttt{rlwrap}
wenzelm@25629
   260
wrapper for GNU readline); the fall-back is to use raw standard input.
wenzelm@25629
   261
wenzelm@25629
   262
wenzelm@12464
   263
\section{Remove awkward symbol names from theory sources --- \texttt{isatool unsymbolize}}
wenzelm@12464
   264
wenzelm@12464
   265
The \tooldx{unsymbolize} utility tunes Isabelle theory sources to improve
wenzelm@12464
   266
readability for plain ASCII output (e.g.\ in email communication).  Most
wenzelm@12464
   267
notably, \texttt{unsymbolize} replaces awkward arrow symbols such as
wenzelm@12464
   268
\verb|\<Longrightarrow>| by \verb|==>|.
wenzelm@12464
   269
\begin{ttbox}
wenzelm@12464
   270
Usage: unsymbolize [FILES|DIRS...]
wenzelm@12464
   271
wenzelm@12464
   272
  Recursively find .thy/.ML files, removing unreadable symbol names.
wenzelm@12464
   273
  Note: this is an ad-hoc script; there is no systematic way to replace
wenzelm@12464
   274
  symbols independently of the inner syntax of a theory!
wenzelm@12464
   275
wenzelm@12464
   276
  Renames old versions of FILES by appending "~~".
wenzelm@12464
   277
\end{ttbox}
wenzelm@12464
   278
wenzelm@12464
   279
wenzelm@16257
   280
\section{Output the version identifier of the Isabelle distribution --- \texttt{isatool version}}
wenzelm@16257
   281
wenzelm@25435
   282
The \tooldx{version} utility outputs the full version string of the
wenzelm@25435
   283
Isabelle distribution being used, e.g.\ ``\texttt{Isabelle2007:
wenzelm@25435
   284
  November 2007}''.  There are no options nor arguments.
wenzelm@16257
   285
wenzelm@25629
   286
wenzelm@26578
   287
\section{Convert XML to YXML --- \texttt{isatool yxml}}
wenzelm@26578
   288
wenzelm@26578
   289
The \tooldx{yxml} utility converts a standard XML document (stdin) to
wenzelm@26578
   290
the much simpler and more efficient YXML format of Isabelle (stdout).
wenzelm@26578
   291
The YXML format is defined as follows.
wenzelm@26578
   292
wenzelm@26578
   293
\begin{enumerate}
wenzelm@26578
   294
wenzelm@26578
   295
\item The encoding is always UTF-8.
wenzelm@26578
   296
wenzelm@26578
   297
\item Body text is represented verbatim (no escaping, no named
wenzelm@26578
   298
  entities, no CDATA chunks, no comments).
wenzelm@26578
   299
wenzelm@26578
   300
\item Markup elements are represented via ASCII control characters $X
wenzelm@26578
   301
  = 5$ and $Y = 6$ as follows:
wenzelm@26578
   302
wenzelm@26578
   303
  \begin{tabular}{ll}
wenzelm@26578
   304
    XML & YXML \\\hline
wenzelm@26578
   305
    \verb,<,\emph{name}~\emph{attribute}\verb,=,\emph{value}~\dots\verb,>, &
wenzelm@26578
   306
    \emph{X\,Y\,name\,Y\,attribute}\verb,=,\emph{value}\dots\emph{X} \\
wenzelm@26578
   307
    \verb,</,\emph{name}\verb,>, & \emph{X\,Y\,X} \\
wenzelm@26578
   308
  \end{tabular}
wenzelm@26578
   309
wenzelm@26578
   310
  There is no special case for empty body text, i.e.\ \verb,<foo/>, is
wenzelm@26578
   311
  treated like \verb,<foo></foo>,.  Also note that \emph{X} and
wenzelm@26578
   312
  \emph{Y} may never occur in well-formed XML documents.
wenzelm@26578
   313
wenzelm@26578
   314
\end{enumerate}
wenzelm@26578
   315
wenzelm@26581
   316
Parsing YXML is pretty straight-forward: split the text into chunks separated
wenzelm@26581
   317
by \emph{X}, then split each chunk into sub-chunks separated by \emph{Y}.
wenzelm@26581
   318
Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
wenzelm@26581
   319
indicates close of an element.  Any other non-empty chunk consists of plain
wenzelm@26581
   320
text.
wenzelm@26578
   321
wenzelm@26578
   322
YXML documents may be detected quickly by checking that the first two
wenzelm@26578
   323
characters are \emph{X\,Y}.
wenzelm@26578
   324
wenzelm@5366
   325
%%% Local Variables: 
wenzelm@5366
   326
%%% mode: latex
wenzelm@5366
   327
%%% TeX-master: "system"
wenzelm@5366
   328
%%% End: