author | haftmann |
Tue, 07 Oct 2008 16:07:50 +0200 | |
changeset 28524 | 644b62cf678f |
parent 28504 | 7ad7d7d6df47 |
child 28916 | 0a802cdda340 |
permissions | -rw-r--r-- |
28224 | 1 |
(* $Id$ *) |
2 |
||
3 |
theory Misc |
|
4 |
imports Pure |
|
5 |
begin |
|
6 |
||
7 |
chapter {* Miscellaneous tools \label{ch:tools} *} |
|
8 |
||
9 |
text {* |
|
10 |
Subsequently we describe various Isabelle related utilities, given |
|
11 |
in alphabetical order. |
|
12 |
*} |
|
13 |
||
14 |
||
28248 | 15 |
section {* The Proof General / Emacs interface *} |
16 |
||
17 |
text {* |
|
28253 | 18 |
The @{tool_def emacs} tool invokes a version of Emacs and Proof |
28248 | 19 |
General within the regular Isabelle settings environment |
20 |
(\secref{sec:settings}). This is more robust than starting Emacs |
|
21 |
separately, loading the Proof General lisp files, and then |
|
22 |
attempting to start Isabelle with dynamic @{setting PATH} lookup |
|
23 |
etc. |
|
24 |
||
25 |
The actual interface script is part of the Proof General |
|
26 |
distribution~\cite{proofgeneral}; its usage depends on the |
|
27 |
particular version. There are some options available, such as |
|
28 |
@{verbatim "-l"} for passing the logic image to be used by default, |
|
28253 | 29 |
or @{verbatim "-m"} to tune the standard print mode. The following |
30 |
Isabelle settings are particularly important for Proof General: |
|
28248 | 31 |
|
32 |
\begin{description} |
|
33 |
||
34 |
\item[@{setting_def PROOFGENERAL_HOME}] points to the main |
|
35 |
installation directory of the Proof General distribution. The |
|
36 |
default settings try to locate this in a number of standard places, |
|
37 |
notably @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}. |
|
38 |
||
39 |
\item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to |
|
40 |
the command line of any invocation of the Proof General @{verbatim |
|
41 |
interface} script. |
|
42 |
||
43 |
\item[@{setting_def XSYMBOL_INSTALLFONTS}] may contain a small shell |
|
44 |
script to install the X11 fonts required for the X-Symbols mode of |
|
28253 | 45 |
Proof General. This is only relevant if the X11 display server runs |
28248 | 46 |
on a different machine than the Emacs application, with a different |
47 |
file-system view on the Proof General installation. Under most |
|
48 |
circumstances Proof General is able to refer to the font files that |
|
49 |
are part of its distribution. |
|
50 |
||
51 |
\end{description} |
|
52 |
*} |
|
53 |
||
54 |
||
28224 | 55 |
section {* Displaying documents *} |
56 |
||
57 |
text {* |
|
58 |
The @{tool_def display} utility displays documents in DVI or PDF |
|
59 |
format: |
|
60 |
\begin{ttbox} |
|
61 |
Usage: display [OPTIONS] FILE |
|
62 |
||
63 |
Options are: |
|
64 |
-c cleanup -- remove FILE after use |
|
65 |
||
66 |
Display document FILE (in DVI format). |
|
67 |
\end{ttbox} |
|
68 |
||
69 |
\medskip The @{verbatim "-c"} option causes the input file to be |
|
70 |
removed after use. The program for viewing @{verbatim dvi} files is |
|
71 |
determined by the @{setting DVI_VIEWER} setting. |
|
72 |
*} |
|
73 |
||
74 |
||
75 |
section {* Viewing documentation \label{sec:tool-doc} *} |
|
76 |
||
77 |
text {* |
|
78 |
The @{tool_def doc} utility displays online documentation: |
|
79 |
\begin{ttbox} |
|
80 |
Usage: doc [DOC] |
|
81 |
||
82 |
View Isabelle documentation DOC, or show list of available documents. |
|
83 |
\end{ttbox} |
|
84 |
If called without arguments, it lists all available documents. Each |
|
85 |
line starts with an identifier, followed by a short description. Any |
|
86 |
of these identifiers may be specified as the first argument in order |
|
87 |
to have the corresponding document displayed. |
|
88 |
||
89 |
\medskip The @{setting ISABELLE_DOCS} setting specifies the list of |
|
90 |
directories (separated by colons) to be scanned for documentations. |
|
91 |
The program for viewing @{verbatim dvi} files is determined by the |
|
92 |
@{setting DVI_VIEWER} setting. |
|
93 |
*} |
|
94 |
||
95 |
||
96 |
section {* Getting logic images *} |
|
97 |
||
98 |
text {* |
|
99 |
The @{tool_def findlogics} utility traverses all directories |
|
100 |
specified in @{setting ISABELLE_PATH}, looking for Isabelle logic |
|
101 |
images. Its usage is: |
|
102 |
\begin{ttbox} |
|
103 |
Usage: findlogics |
|
104 |
||
105 |
Collect heap file names from ISABELLE_PATH. |
|
106 |
\end{ttbox} |
|
107 |
||
108 |
The base names of all files found on the path are printed --- sorted |
|
109 |
and with duplicates removed. Also note that lookup in @{setting |
|
110 |
ISABELLE_PATH} includes the current values of @{setting ML_SYSTEM} |
|
111 |
and @{setting ML_PLATFORM}. Thus switching to another ML compiler |
|
112 |
may change the set of logic images available. |
|
113 |
*} |
|
114 |
||
115 |
||
116 |
section {* Inspecting the settings environment \label{sec:tool-getenv} *} |
|
117 |
||
118 |
text {* |
|
119 |
The Isabelle settings environment --- as provided by the |
|
120 |
site-default and user-specific settings files --- can be inspected |
|
121 |
with the @{tool_def getenv} utility: |
|
122 |
\begin{ttbox} |
|
123 |
Usage: getenv [OPTIONS] [VARNAMES ...] |
|
124 |
||
125 |
Options are: |
|
126 |
-a display complete environment |
|
127 |
-b print values only (doesn't work for -a) |
|
128 |
||
129 |
Get value of VARNAMES from the Isabelle settings. |
|
130 |
\end{ttbox} |
|
131 |
||
132 |
With the @{verbatim "-a"} option, one may inspect the full process |
|
133 |
environment that Isabelle related programs are run in. This usually |
|
134 |
contains much more variables than are actually Isabelle settings. |
|
135 |
Normally, output is a list of lines of the form @{text |
|
136 |
name}@{verbatim "="}@{text value}. The @{verbatim "-b"} option |
|
137 |
causes only the values to be printed. |
|
138 |
*} |
|
139 |
||
140 |
||
141 |
subsubsection {* Examples *} |
|
142 |
||
143 |
text {* |
|
144 |
Get the ML system name and the location where the compiler binaries |
|
145 |
are supposed to reside as follows: |
|
146 |
\begin{ttbox} |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28253
diff
changeset
|
147 |
isabelle getenv ML_SYSTEM ML_HOME |
28224 | 148 |
{\out ML_SYSTEM=polyml} |
149 |
{\out ML_HOME=/usr/share/polyml/x86-linux} |
|
150 |
\end{ttbox} |
|
151 |
||
152 |
The next one peeks at the output directory for Isabelle logic |
|
153 |
images: |
|
154 |
\begin{ttbox} |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28253
diff
changeset
|
155 |
isabelle getenv -b ISABELLE_OUTPUT |
28224 | 156 |
{\out /home/me/isabelle/heaps/polyml_x86-linux} |
157 |
\end{ttbox} |
|
158 |
Here we have used the @{verbatim "-b"} option to suppress the |
|
159 |
@{verbatim "ISABELLE_OUTPUT="} prefix. The value above is what |
|
160 |
became of the following assignment in the default settings file: |
|
161 |
\begin{ttbox} |
|
162 |
ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps" |
|
163 |
\end{ttbox} |
|
164 |
||
165 |
Note how the @{setting ML_IDENTIFIER} value got appended |
|
166 |
automatically to each path component. This is a special feature of |
|
167 |
@{setting ISABELLE_OUTPUT}. |
|
168 |
*} |
|
169 |
||
170 |
||
171 |
section {* Installing standalone Isabelle executables \label{sec:tool-install} *} |
|
172 |
||
173 |
text {* |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28253
diff
changeset
|
174 |
By default, the main Isabelle binaries (@{executable "isabelle"} |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28253
diff
changeset
|
175 |
etc.) are just run from their location within the distribution |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28253
diff
changeset
|
176 |
directory, probably indirectly by the shell through its @{setting |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28253
diff
changeset
|
177 |
PATH}. Other schemes of installation are supported by the |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28253
diff
changeset
|
178 |
@{tool_def install} utility: |
28224 | 179 |
\begin{ttbox} |
180 |
Usage: install [OPTIONS] |
|
181 |
||
182 |
Options are: |
|
183 |
-d DISTDIR use DISTDIR as Isabelle distribution |
|
184 |
(default ISABELLE_HOME) |
|
185 |
-p DIR install standalone binaries in DIR |
|
186 |
||
187 |
Install Isabelle executables with absolute references to the current |
|
188 |
distribution directory. |
|
189 |
\end{ttbox} |
|
190 |
||
191 |
The @{verbatim "-d"} option overrides the current Isabelle |
|
192 |
distribution directory as determined by @{setting ISABELLE_HOME}. |
|
193 |
||
194 |
The @{verbatim "-p"} option installs executable wrapper scripts for |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28253
diff
changeset
|
195 |
@{executable "isabelle-process"}, @{executable isabelle}, |
28238 | 196 |
@{executable Isabelle}, containing proper absolute references to the |
197 |
Isabelle distribution directory. A typical @{verbatim DIR} |
|
198 |
specification would be some directory expected to be in the shell's |
|
199 |
@{setting PATH}, such as @{verbatim "/usr/local/bin"}. It is |
|
200 |
important to note that a plain manual copy of the original Isabelle |
|
201 |
executables does not work, since it disrupts the integrity of the |
|
202 |
Isabelle distribution. |
|
28224 | 203 |
*} |
204 |
||
205 |
||
206 |
section {* Creating instances of the Isabelle logo *} |
|
207 |
||
208 |
text {* |
|
209 |
The @{tool_def logo} utility creates any instance of the generic |
|
210 |
Isabelle logo as an Encapsuled Postscript file (EPS): |
|
211 |
\begin{ttbox} |
|
212 |
Usage: logo [OPTIONS] NAME |
|
213 |
||
214 |
Create instance NAME of the Isabelle logo (as EPS). |
|
215 |
||
216 |
Options are: |
|
217 |
-o OUTFILE set output file (default determined from NAME) |
|
218 |
-q quiet mode |
|
219 |
\end{ttbox} |
|
220 |
You are encouraged to use this to create a derived logo for your |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28253
diff
changeset
|
221 |
Isabelle project. For example, @{verbatim isabelle} @{tool |
28238 | 222 |
logo}~@{verbatim Bali} creates @{verbatim isabelle_bali.eps}. |
28224 | 223 |
*} |
224 |
||
225 |
||
226 |
section {* Isabelle's version of make \label{sec:tool-make} *} |
|
227 |
||
228 |
text {* |
|
229 |
The Isabelle @{tool_def make} utility is a very simple wrapper for |
|
230 |
ordinary Unix @{executable make}: |
|
231 |
\begin{ttbox} |
|
232 |
Usage: make [ARGS ...] |
|
233 |
||
234 |
Compile the logic in current directory using IsaMakefile. |
|
235 |
ARGS are directly passed to the system make program. |
|
236 |
\end{ttbox} |
|
237 |
||
238 |
Note that the Isabelle settings environment is also active. Thus one |
|
239 |
may refer to its values within the @{verbatim IsaMakefile}, e.g.\ |
|
240 |
@{verbatim "$(ISABELLE_OUTPUT)"}. Furthermore, programs started from |
|
241 |
the make file also inherit this environment. Typically, @{verbatim |
|
242 |
IsaMakefile}s defer the real work to the @{tool_ref usedir} utility. |
|
243 |
||
244 |
\medskip The basic @{verbatim IsaMakefile} convention is that the |
|
245 |
default target builds the actual logic, including its parents if |
|
246 |
appropriate. The @{verbatim images} target is intended to build all |
|
247 |
local logic images, while the @{verbatim test} target shall build |
|
248 |
all related examples. The @{verbatim all} target shall do |
|
249 |
@{verbatim images} and @{verbatim test}. |
|
250 |
*} |
|
251 |
||
252 |
||
253 |
subsubsection {* Examples *} |
|
254 |
||
255 |
text {* |
|
256 |
Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's |
|
257 |
object-logics as a model for your own developments. For example, |
|
28238 | 258 |
see @{"file" "~~/src/FOL/IsaMakefile"}. |
28224 | 259 |
*} |
260 |
||
261 |
||
262 |
section {* Make all logics *} |
|
263 |
||
264 |
text {* |
|
265 |
The @{tool_def makeall} utility applies Isabelle make to all logic |
|
266 |
directories of the distribution: |
|
267 |
\begin{ttbox} |
|
268 |
Usage: makeall [ARGS ...] |
|
269 |
||
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28253
diff
changeset
|
270 |
Apply isabelle make to all logics (passing ARGS). |
28224 | 271 |
\end{ttbox} |
272 |
||
273 |
The arguments @{verbatim ARGS} are just passed verbatim to each |
|
274 |
@{tool make} invocation. |
|
275 |
*} |
|
276 |
||
277 |
||
278 |
section {* Printing documents *} |
|
279 |
||
280 |
text {* |
|
281 |
The @{tool_def print} utility prints documents: |
|
282 |
\begin{ttbox} |
|
283 |
Usage: print [OPTIONS] FILE |
|
284 |
||
285 |
Options are: |
|
286 |
-c cleanup -- remove FILE after use |
|
287 |
||
288 |
Print document FILE. |
|
289 |
\end{ttbox} |
|
290 |
||
291 |
The @{verbatim "-c"} option causes the input file to be removed |
|
292 |
after use. The printer spool command is determined by the @{setting |
|
293 |
PRINT_COMMAND} setting. |
|
294 |
*} |
|
295 |
||
296 |
||
297 |
section {* Run Isabelle with plain tty interaction \label{sec:tool-tty} *} |
|
298 |
||
299 |
text {* |
|
300 |
The @{tool_def tty} utility runs the Isabelle process interactively |
|
301 |
within a plain terminal session: |
|
302 |
\begin{ttbox} |
|
303 |
Usage: tty [OPTIONS] |
|
304 |
||
305 |
Options are: |
|
306 |
-l NAME logic image name (default ISABELLE_LOGIC) |
|
307 |
-m MODE add print mode for output |
|
308 |
-p NAME line editor program name (default ISABELLE_LINE_EDITOR) |
|
309 |
||
310 |
Run Isabelle process with plain tty interaction, and optional line editor. |
|
311 |
\end{ttbox} |
|
312 |
||
313 |
The @{verbatim "-l"} option specifies the logic image. The |
|
314 |
@{verbatim "-m"} option specifies additional print modes. The The |
|
315 |
@{verbatim "-p"} option specifies an alternative line editor (such |
|
28238 | 316 |
as the @{executable_def rlwrap} wrapper for GNU readline); the |
317 |
fall-back is to use raw standard input. |
|
28224 | 318 |
*} |
319 |
||
320 |
||
321 |
section {* Remove awkward symbol names from theory sources *} |
|
322 |
||
323 |
text {* |
|
324 |
The @{tool_def unsymbolize} utility tunes Isabelle theory sources to |
|
325 |
improve readability for plain ASCII output (e.g.\ in email |
|
326 |
communication). Most notably, @{tool unsymbolize} replaces awkward |
|
327 |
arrow symbols such as @{verbatim "\\"}@{verbatim "<Longrightarrow>"} |
|
328 |
by @{verbatim "==>"}. |
|
329 |
\begin{ttbox} |
|
330 |
Usage: unsymbolize [FILES|DIRS...] |
|
331 |
||
332 |
Recursively find .thy/.ML files, removing unreadable symbol names. |
|
333 |
Note: this is an ad-hoc script; there is no systematic way to replace |
|
334 |
symbols independently of the inner syntax of a theory! |
|
335 |
||
336 |
Renames old versions of FILES by appending "~~". |
|
337 |
\end{ttbox} |
|
338 |
*} |
|
339 |
||
340 |
||
341 |
section {* Output the version identifier of the Isabelle distribution *} |
|
342 |
||
343 |
text {* |
|
344 |
The @{tool_def version} utility outputs the full version string of |
|
345 |
the Isabelle distribution being used, e.g.\ ``@{verbatim |
|
346 |
"Isabelle2008: June 2008"}. There are no options nor arguments. |
|
347 |
*} |
|
348 |
||
349 |
||
350 |
section {* Convert XML to YXML *} |
|
351 |
||
352 |
text {* |
|
353 |
The @{tool_def yxml} tool converts a standard XML document (stdin) |
|
354 |
to the much simpler and more efficient YXML format of Isabelle |
|
355 |
(stdout). The YXML format is defined as follows. |
|
356 |
||
357 |
\begin{enumerate} |
|
358 |
||
359 |
\item The encoding is always UTF-8. |
|
360 |
||
361 |
\item Body text is represented verbatim (no escaping, no special |
|
362 |
treatment of white space, no named entities, no CDATA chunks, no |
|
363 |
comments). |
|
364 |
||
365 |
\item Markup elements are represented via ASCII control characters |
|
366 |
@{text "\<^bold>X = 5"} and @{text "\<^bold>Y = 6"} as follows: |
|
367 |
||
368 |
\begin{tabular}{ll} |
|
369 |
XML & YXML \\\hline |
|
370 |
@{verbatim "<"}@{text "name attribute"}@{verbatim "="}@{text "value \<dots>"}@{verbatim ">"} & |
|
371 |
@{text "\<^bold>X\<^bold>Yname\<^bold>Yattribute"}@{verbatim "="}@{text "value\<dots>\<^bold>X"} \\ |
|
372 |
@{verbatim "</"}@{text name}@{verbatim ">"} & @{text "\<^bold>X\<^bold>Y\<^bold>X"} \\ |
|
373 |
\end{tabular} |
|
374 |
||
375 |
There is no special case for empty body text, i.e.\ @{verbatim |
|
376 |
"<foo/>"} is treated like @{verbatim "<foo></foo>"}. Also note that |
|
377 |
@{text "\<^bold>X"} and @{text "\<^bold>Y"} may never occur in |
|
378 |
well-formed XML documents. |
|
379 |
||
380 |
\end{enumerate} |
|
381 |
||
382 |
Parsing YXML is pretty straight-forward: split the text into chunks |
|
383 |
separated by @{text "\<^bold>X"}, then split each chunk into |
|
384 |
sub-chunks separated by @{text "\<^bold>Y"}. Markup chunks start |
|
385 |
with an empty sub-chunk, and a second empty sub-chunk indicates |
|
386 |
close of an element. Any other non-empty chunk consists of plain |
|
28238 | 387 |
text. For example, see @{"file" "~~/src/Pure/General/yxml.ML"} or |
388 |
@{"file" "~~/src/Pure/General/yxml.scala"}. |
|
28224 | 389 |
|
390 |
YXML documents may be detected quickly by checking that the first |
|
391 |
two characters are @{text "\<^bold>X\<^bold>Y"}. |
|
392 |
*} |
|
393 |
||
394 |
end |