3188
|
1 |
|
|
2 |
% $Id$
|
|
3 |
|
|
4 |
\chapter{Miscellaneous tools}
|
|
5 |
|
3217
|
6 |
Subsequently we describe various Isabelle related utilities --- in
|
|
7 |
alphabetical order.
|
|
8 |
|
|
9 |
|
|
10 |
\section{Viewing documentation --- \texttt{isatool doc}} \label{sec:tool-doc}
|
|
11 |
|
|
12 |
The \tooldx{doc} utility displays online documentation:
|
|
13 |
\begin{ttbox}
|
|
14 |
Usage: isatool doc [DOC]
|
|
15 |
|
|
16 |
View Isabelle documentation DOC, or show list of available documents.
|
|
17 |
\end{ttbox}
|
|
18 |
If called without arguments, it lists all available documents. Each
|
|
19 |
line starts with an identifier, followed by some comment. Any of these
|
|
20 |
identifiers may be specified as the first argument in order to have
|
|
21 |
the corresponding document displayed.
|
|
22 |
|
|
23 |
\medskip The \texttt{ISABELLE_DOCS} setting specifies the list of
|
|
24 |
directories (separated by colons) to be scanned for documentations.
|
|
25 |
The program for viewing \texttt{dvi} files is set in
|
|
26 |
\texttt{DVI_VIEWER}.
|
|
27 |
|
|
28 |
|
|
29 |
\section{Tuning proof scripts --- \texttt{isatool expandshort}}
|
|
30 |
|
|
31 |
The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance
|
|
32 |
readability a bit:
|
|
33 |
\begin{ttbox}
|
|
34 |
Usage: expandshort [FILES ...]
|
|
35 |
|
|
36 |
Expand shorthand goal commands in FILES. Also contracts uses of
|
|
37 |
resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on
|
|
38 |
1-element lists; furthermore expands tabs, since they are now
|
|
39 |
forbidden in ML string constants.
|
|
40 |
|
|
41 |
Renames old versions of FILES by appending "~~".
|
|
42 |
\end{ttbox}
|
|
43 |
In the files supplied as arguments, all occurrences of the shorthand
|
|
44 |
commands \texttt{br}, \texttt{be} etc.\ are replaced with the
|
|
45 |
corresponding full commands. Shorthand commands should appear one per
|
|
46 |
line. The old versions of the files are renamed to have the
|
|
47 |
suffix~\verb'~~'.
|
|
48 |
|
|
49 |
\section{Get logic images --- \texttt{isatool findlogics}}
|
|
50 |
|
|
51 |
The \tooldx{findlogics} utility traverses all directories specified in
|
|
52 |
\texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage
|
|
53 |
is:
|
|
54 |
\begin{ttbox}
|
|
55 |
Usage: isatool findlogics
|
|
56 |
|
|
57 |
Collect heap file names from ISABELLE_PATH.
|
|
58 |
\end{ttbox}
|
|
59 |
The base names of all files found on the path are printed --- sorted
|
|
60 |
and with duplicates removed. Also note that \texttt{ISABELLE_PATH}
|
|
61 |
implicitely depends upon \texttt{ML_SYSTEM}. Thus switching to another
|
|
62 |
{\ML} compiler may change the set of logic images available.
|
|
63 |
|
3188
|
64 |
|
|
65 |
\section{Inspecting the settings environment -- \texttt{isatool getenv}}
|
|
66 |
\label{sec:tool-getenv}
|
|
67 |
|
|
68 |
The Isabelle settings environment --- as provided by the site-default
|
|
69 |
and user-specific settings files --- can be inspected with the
|
|
70 |
\tooldx{getenv} utility:
|
|
71 |
\begin{ttbox}
|
|
72 |
Usage: isatool getenv [OPTIONS] [VARNAMES ...]
|
|
73 |
|
|
74 |
Options are:
|
|
75 |
-a display complete environment
|
|
76 |
-b print values only (doesn't work for -a)
|
|
77 |
|
|
78 |
Get value of VARNAMES from the Isabelle settings.
|
|
79 |
\end{ttbox}
|
|
80 |
|
|
81 |
With the \texttt{-a} option, one may inspect the full process
|
|
82 |
environment that Isabelle related programs are run in. This usually
|
|
83 |
contains much more variables than are actually Isabelle settings.
|
3217
|
84 |
Normally output is a list of lines of the form
|
|
85 |
\mbox{$varname$\texttt{=}$value$}. The \texttt{-b} option causes only
|
|
86 |
the values to be printed.
|
3188
|
87 |
|
|
88 |
|
|
89 |
\subsection*{Examples}
|
|
90 |
|
|
91 |
Get the {\ML} system identifier and the location where the compiler
|
3217
|
92 |
binaries are supposed to reside as follows:
|
3188
|
93 |
\begin{ttbox}
|
|
94 |
isatool getenv ML_SYSTEM ML_HOME
|
3217
|
95 |
{\out ML_SYSTEM=smlnj-1.09}
|
3188
|
96 |
{\out ML_HOME=/usr/local/sml109.27/bin}
|
|
97 |
\end{ttbox}
|
|
98 |
|
3217
|
99 |
The next one peeks at the search path that \texttt{isabelle} uses to
|
3188
|
100 |
locate logic images:
|
|
101 |
\begin{ttbox}
|
|
102 |
isatool getenv -b ISABELLE_PATH
|
3217
|
103 |
{\out /home/me/isabelle/heaps/smlnj-1.09:/proj/isabelle/heaps/smlnj-1.09}
|
3188
|
104 |
\end{ttbox}
|
|
105 |
We used the \texttt{-b} option to suppress the \texttt{ISABELLE_PATH=}
|
|
106 |
prefix. The value above is what became of the following assignment in
|
|
107 |
the default settings file:
|
|
108 |
\begin{ttbox}
|
|
109 |
ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps
|
|
110 |
\end{ttbox}
|
3217
|
111 |
Note how the \texttt{ML_SYSTEM} value got appended automatically to
|
|
112 |
each path component. This is a special feature of
|
|
113 |
\texttt{ISABELLE_PATH} (and also of \texttt{ISABELLE_OUTPUT}).
|
3188
|
114 |
|
|
115 |
|
|
116 |
\section{Isabelle's version of make --- \texttt{isatool make}}
|
|
117 |
|
3217
|
118 |
The Isabelle \tooldx{make} utility is a very simple wrapper for
|
|
119 |
ordinary Unix \texttt{make}:
|
3188
|
120 |
\begin{ttbox}
|
|
121 |
Usage: isatool make [ARGS ...]
|
|
122 |
|
|
123 |
Compiles logic in current directory using IsaMakefile.
|
|
124 |
ARGS are directly passed to the system make program.
|
|
125 |
\end{ttbox}
|
3217
|
126 |
Note that the Isabelle settings environment is also active. Thus one
|
|
127 |
may refer to its values within the \texttt{IsaMakefile}, e.g.\
|
|
128 |
\texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the
|
|
129 |
make file also inherit this environment.
|
|
130 |
|
|
131 |
\medskip You may want to have a look at the \texttt{IsaMakefile}s of
|
|
132 |
the distributed object-logics as examples for your own developements.
|
3188
|
133 |
|
|
134 |
|
3217
|
135 |
\section{Running complete logics --- \texttt{isatool usedir}} \label{sec:tool-usedir}
|
3188
|
136 |
|
3217
|
137 |
FIXME
|
|
138 |
|
|
139 |
%FIXME
|
|
140 |
% -g BOOL generate theory graph data (default false)
|
3188
|
141 |
\begin{ttbox}
|
|
142 |
Usage: isatool usedir LOGIC NAME
|
|
143 |
|
|
144 |
Options are:
|
|
145 |
-b build mode (output heap image, use dir ".")
|
|
146 |
-h BOOL generate theory HTML data (default false)
|
|
147 |
-s NAME override session NAME
|
|
148 |
|
|
149 |
Build object-logic or run examples. Also creates browsing
|
|
150 |
information (HTML etc.) according to settings.
|
|
151 |
\end{ttbox}
|
|
152 |
|
3217
|
153 |
FIXME
|