author | wenzelm |
Thu, 15 Nov 2007 11:49:03 +0100 | |
changeset 25435 | bafaea364a66 |
parent 20572 | 2b88de40da57 |
child 25629 | f7c6ca73a8bd |
permissions | -rw-r--r-- |
3188 | 1 |
|
2 |
% $Id$ |
|
3 |
||
3278 | 4 |
\chapter{Miscellaneous tools} \label{ch:tools} |
3188 | 5 |
|
11031 | 6 |
Subsequently we describe various Isabelle related utilities, given in |
3217 | 7 |
alphabetical order. |
8 |
||
9 |
||
11031 | 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 |
|
12464 | 27 |
an automatically converted script work again --- the success rate is around |
28 |
99\% for common ML scripts. |
|
11031 | 29 |
|
30 |
||
14932 | 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 |
||
20572 | 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 |
|
14932 | 45 |
\texttt{DVI_VIEWER} setting. |
46 |
||
47 |
||
3217 | 48 |
\section{Viewing documentation --- \texttt{isatool doc}} \label{sec:tool-doc} |
49 |
||
50 |
The \tooldx{doc} utility displays online documentation: |
|
51 |
\begin{ttbox} |
|
13047 | 52 |
Usage: doc [DOC] |
3217 | 53 |
|
54 |
View Isabelle documentation DOC, or show list of available documents. |
|
55 |
\end{ttbox} |
|
7882 | 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. |
|
3217 | 60 |
|
7882 | 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. |
|
3217 | 64 |
|
65 |
||
66 |
\section{Tuning proof scripts --- \texttt{isatool expandshort}} |
|
67 |
||
68 |
The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance |
|
4540 | 69 |
readability: |
3217 | 70 |
\begin{ttbox} |
4540 | 71 |
Usage: expandshort [FILES|DIRS...] |
3217 | 72 |
|
7498 | 73 |
Recursively find .ML files, expand shorthand goal commands. Also |
74 |
contracts uses of resolve_tac, dresolve_tac, eresolve_tac, |
|
7883 | 75 |
forward_tac, rewrite_goals_tac on 1-element lists; furthermore |
76 |
expands tabs, which are forbidden in SML string constants. |
|
3217 | 77 |
|
4540 | 78 |
Renames old versions of files by appending "~~". |
3217 | 79 |
\end{ttbox} |
7882 | 80 |
In the files or directories supplied as arguments, all occurrences of the |
81 |
shorthand commands \texttt{br}, \texttt{be} etc.\ in proof scripts are |
|
82 |
replaced with the corresponding full commands. The old versions of the files |
|
13047 | 83 |
are renamed to have the suffix ``\verb'~~'''. |
4540 | 84 |
|
3217 | 85 |
|
5366 | 86 |
\section{Getting logic images --- \texttt{isatool findlogics}} |
3217 | 87 |
|
88 |
The \tooldx{findlogics} utility traverses all directories specified in |
|
7882 | 89 |
\texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage is: |
3217 | 90 |
\begin{ttbox} |
13047 | 91 |
Usage: findlogics |
3217 | 92 |
|
93 |
Collect heap file names from ISABELLE_PATH. |
|
94 |
\end{ttbox} |
|
6414 | 95 |
The base names of all files found on the path are printed --- sorted and with |
9790 | 96 |
duplicates removed. Also note that lookup in \texttt{ISABELLE_PATH} includes |
97 |
the current values of \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM}. Thus |
|
98 |
switching to another {\ML} compiler may change the set of logic images |
|
99 |
available. |
|
3217 | 100 |
|
3188 | 101 |
|
12464 | 102 |
\section{Inspecting the settings environment --- \texttt{isatool getenv}} |
3188 | 103 |
\label{sec:tool-getenv} |
104 |
||
7882 | 105 |
The Isabelle settings environment --- as provided by the site-default and |
106 |
user-specific settings files --- can be inspected with the \tooldx{getenv} |
|
107 |
utility: |
|
3188 | 108 |
\begin{ttbox} |
13047 | 109 |
Usage: getenv [OPTIONS] [VARNAMES ...] |
3188 | 110 |
|
111 |
Options are: |
|
112 |
-a display complete environment |
|
113 |
-b print values only (doesn't work for -a) |
|
114 |
||
115 |
Get value of VARNAMES from the Isabelle settings. |
|
116 |
\end{ttbox} |
|
117 |
||
7882 | 118 |
With the \texttt{-a} option, one may inspect the full process environment that |
119 |
Isabelle related programs are run in. This usually contains much more |
|
120 |
variables than are actually Isabelle settings. Normally, output is a list of |
|
121 |
lines of the form \mbox{$name$\texttt{=}$value$}. The \texttt{-b} option |
|
122 |
causes only the values to be printed. |
|
3188 | 123 |
|
124 |
||
125 |
\subsection*{Examples} |
|
126 |
||
9790 | 127 |
Get the {\ML} system name and the location where the compiler binaries are |
128 |
supposed to reside as follows: |
|
3188 | 129 |
\begin{ttbox} |
130 |
isatool getenv ML_SYSTEM ML_HOME |
|
9790 | 131 |
{\out ML_SYSTEM=polyml} |
132 |
{\out ML_HOME=/usr/share/polyml/x86-linux} |
|
3188 | 133 |
\end{ttbox} |
134 |
||
9790 | 135 |
The next one peeks at the output directory for \texttt{isabelle} logic images: |
3188 | 136 |
\begin{ttbox} |
9790 | 137 |
isatool getenv -b ISABELLE_OUTPUT |
138 |
{\out /home/me/isabelle/heaps/polyml_x86-linux} |
|
3188 | 139 |
\end{ttbox} |
4555 | 140 |
Here we have used the \texttt{-b} option to suppress the |
9790 | 141 |
\texttt{ISABELLE_OUTPUT=} prefix. The value above is what became of the |
4555 | 142 |
following assignment in the default settings file: |
3188 | 143 |
\begin{ttbox} |
9790 | 144 |
ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps" |
3188 | 145 |
\end{ttbox} |
9790 | 146 |
Note how the \texttt{ML_IDENTIFIER} value got appended automatically to each |
147 |
path component. This is a special feature of \texttt{ISABELLE_OUTPUT}. |
|
3188 | 148 |
|
149 |
||
12464 | 150 |
\section{Installing standalone Isabelle executables --- \texttt{isatool install}} |
7882 | 151 |
\label{sec:tool-install} |
5366 | 152 |
|
7882 | 153 |
By default, the Isabelle binaries (\texttt{isabelle}, \texttt{isatool} etc.) |
154 |
are just run from their location within the distribution directory, probably |
|
6418 | 155 |
indirectly by the shell through its \texttt{PATH}. Other schemes of |
156 |
installation are supported by the \tooldx{install} utility: |
|
5366 | 157 |
\begin{ttbox} |
6418 | 158 |
Usage: install [OPTIONS] |
5366 | 159 |
|
5405 | 160 |
Options are: |
7883 | 161 |
-d DISTDIR use DISTDIR as Isabelle distribution |
162 |
(default ISABELLE_HOME) |
|
6418 | 163 |
-p DIR install standalone binaries in DIR |
5405 | 164 |
|
6418 | 165 |
Install Isabelle executables with absolute references to the current |
166 |
distribution directory. |
|
5366 | 167 |
\end{ttbox} |
168 |
||
6418 | 169 |
The \texttt{-d} option overrides the current Isabelle distribution directory |
170 |
as determined by \texttt{ISABELLE_HOME}. |
|
171 |
||
172 |
The \texttt{-p} option installs executable wrapper scripts for |
|
173 |
\texttt{isabelle}, \texttt{isatool}, \texttt{Isabelle}, containing proper |
|
174 |
absolute references to the Isabelle distribution directory. A typical |
|
175 |
\texttt{DIR} specification would be some directory expected to be in the |
|
176 |
shell's \texttt{PATH}, such as \texttt{/usr/local/bin}. It is important to |
|
177 |
note that a plain manual copy of the original Isabelle executables just would |
|
178 |
not work! |
|
179 |
||
5366 | 180 |
|
12464 | 181 |
\section{Creating instances of the Isabelle logo --- \texttt{isatool |
5571 | 182 |
logo}} |
183 |
||
184 |
The \tooldx{logo} utility creates any instance of the generic Isabelle logo as |
|
185 |
an Encapsuled Postscript file (EPS): |
|
186 |
\begin{ttbox} |
|
187 |
Usage: logo [OPTIONS] NAME |
|
188 |
||
189 |
Create instance NAME of the Isabelle logo (as EPS). |
|
190 |
||
191 |
Options are: |
|
192 |
-o OUTFILE set output file (default determined from NAME) |
|
193 |
-q quiet mode |
|
194 |
\end{ttbox} |
|
195 |
You are encouraged to use this to create a derived logo for your Isabelle |
|
13047 | 196 |
project. For example, \texttt{isatool logo Bali} creates |
197 |
\texttt{isabelle_bali.eps}. |
|
5571 | 198 |
|
199 |
||
3188 | 200 |
\section{Isabelle's version of make --- \texttt{isatool make}} |
11616 | 201 |
\label{sec:tool-make} |
3188 | 202 |
|
3217 | 203 |
The Isabelle \tooldx{make} utility is a very simple wrapper for |
204 |
ordinary Unix \texttt{make}: |
|
3188 | 205 |
\begin{ttbox} |
13047 | 206 |
Usage: make [ARGS ...] |
3188 | 207 |
|
7801 | 208 |
Compile the logic in current directory using IsaMakefile. |
3188 | 209 |
ARGS are directly passed to the system make program. |
210 |
\end{ttbox} |
|
3217 | 211 |
Note that the Isabelle settings environment is also active. Thus one |
3278 | 212 |
may refer to its values within the \ttindex{IsaMakefile}, e.g.\ |
3217 | 213 |
\texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the |
3278 | 214 |
make file also inherit this environment. Typically, |
215 |
\texttt{IsaMakefile}s defer the real work to the \texttt{usedir} |
|
216 |
utility, see \S\ref{sec:tool-usedir}. |
|
3217 | 217 |
|
3278 | 218 |
\medskip The basic \texttt{IsaMakefile} convention is that the default |
4540 | 219 |
target builds the actual logic, including its parents if appropriate. |
4555 | 220 |
The \texttt{images} target is intended to build all local logic |
221 |
images, while the \texttt{test} target shall build all related |
|
222 |
examples. The \texttt{all} target shall do \texttt{images} and |
|
223 |
\texttt{test}. |
|
4540 | 224 |
|
225 |
||
226 |
\subsection*{Examples} |
|
227 |
||
228 |
Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's |
|
13047 | 229 |
object-logics as a model for your own developments. For example, see |
4555 | 230 |
\texttt{src/FOL/IsaMakefile}. |
4540 | 231 |
|
232 |
||
12464 | 233 |
\section{Make all logics --- \texttt{isatool makeall}} |
4540 | 234 |
|
235 |
The \tooldx{makeall} utility applies Isabelle make to all logic |
|
4555 | 236 |
directories of the distribution: |
4540 | 237 |
\begin{ttbox} |
238 |
Usage: makeall [ARGS ...] |
|
239 |
||
240 |
Apply isatool make to all logics (passing ARGS). |
|
241 |
\end{ttbox} |
|
4555 | 242 |
The arguments \texttt{ARGS} are just passed verbatim to each |
4540 | 243 |
\texttt{make} invocation. |
3188 | 244 |
|
12464 | 245 |
|
14932 | 246 |
\section{Printing documents --- \texttt{isatool print}} |
247 |
||
248 |
The \tooldx{print} utility prints documents: |
|
249 |
\begin{ttbox} |
|
250 |
Usage: print [OPTIONS] FILE |
|
251 |
||
252 |
Options are: |
|
253 |
-c cleanup -- remove FILE after use |
|
254 |
||
255 |
Print document FILE. |
|
256 |
\end{ttbox} |
|
257 |
||
258 |
The \texttt{-c} option causes the input file to be removed after use. The |
|
259 |
printer spool command is determined by the \texttt{PRINT_COMMAND} setting. |
|
260 |
||
261 |
||
12464 | 262 |
\section{Remove awkward symbol names from theory sources --- \texttt{isatool unsymbolize}} |
263 |
||
264 |
The \tooldx{unsymbolize} utility tunes Isabelle theory sources to improve |
|
265 |
readability for plain ASCII output (e.g.\ in email communication). Most |
|
266 |
notably, \texttt{unsymbolize} replaces awkward arrow symbols such as |
|
267 |
\verb|\<Longrightarrow>| by \verb|==>|. |
|
268 |
\begin{ttbox} |
|
269 |
Usage: unsymbolize [FILES|DIRS...] |
|
270 |
||
271 |
Recursively find .thy/.ML files, removing unreadable symbol names. |
|
272 |
Note: this is an ad-hoc script; there is no systematic way to replace |
|
273 |
symbols independently of the inner syntax of a theory! |
|
274 |
||
275 |
Renames old versions of FILES by appending "~~". |
|
276 |
\end{ttbox} |
|
277 |
||
278 |
||
16257 | 279 |
\section{Output the version identifier of the Isabelle distribution --- \texttt{isatool version}} |
280 |
||
25435
bafaea364a66
isatool version: clarify that this is the *long* form;
wenzelm
parents:
20572
diff
changeset
|
281 |
The \tooldx{version} utility outputs the full version string of the |
bafaea364a66
isatool version: clarify that this is the *long* form;
wenzelm
parents:
20572
diff
changeset
|
282 |
Isabelle distribution being used, e.g.\ ``\texttt{Isabelle2007: |
bafaea364a66
isatool version: clarify that this is the *long* form;
wenzelm
parents:
20572
diff
changeset
|
283 |
November 2007}''. There are no options nor arguments. |
16257 | 284 |
|
5366 | 285 |
%%% Local Variables: |
286 |
%%% mode: latex |
|
287 |
%%% TeX-master: "system" |
|
288 |
%%% End: |