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: