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