1 |
1 |
2 % $Id$ |
2 % $Id$ |
3 |
3 |
4 \chapter{Miscellaneous tools} |
4 \chapter{Miscellaneous tools} |
|
5 |
|
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. |
5 |
63 |
6 |
64 |
7 \section{Inspecting the settings environment -- \texttt{isatool getenv}} |
65 \section{Inspecting the settings environment -- \texttt{isatool getenv}} |
8 \label{sec:tool-getenv} |
66 \label{sec:tool-getenv} |
9 |
67 |
21 \end{ttbox} |
79 \end{ttbox} |
22 |
80 |
23 With the \texttt{-a} option, one may inspect the full process |
81 With the \texttt{-a} option, one may inspect the full process |
24 environment that Isabelle related programs are run in. This usually |
82 environment that Isabelle related programs are run in. This usually |
25 contains much more variables than are actually Isabelle settings. |
83 contains much more variables than are actually Isabelle settings. |
26 |
84 Normally output is a list of lines of the form |
27 Unless the \texttt{-b} option is given, the output is a list of lines |
85 \mbox{$varname$\texttt{=}$value$}. The \texttt{-b} option causes only |
28 of the form $varname\mathtt{=}value$. |
86 the values to be printed. |
29 |
87 |
30 |
88 |
31 \subsection*{Examples} |
89 \subsection*{Examples} |
32 |
90 |
33 Get the {\ML} system identifier and the location where the compiler |
91 Get the {\ML} system identifier and the location where the compiler |
34 binaries are supposed to be installed as follows: |
92 binaries are supposed to reside as follows: |
35 \begin{ttbox} |
93 \begin{ttbox} |
36 isatool getenv ML_SYSTEM ML_HOME |
94 isatool getenv ML_SYSTEM ML_HOME |
|
95 {\out ML_SYSTEM=smlnj-1.09} |
37 {\out ML_HOME=/usr/local/sml109.27/bin} |
96 {\out ML_HOME=/usr/local/sml109.27/bin} |
38 {\out ML_SYSTEM=smlnj-1.09} |
|
39 \end{ttbox} |
97 \end{ttbox} |
40 |
98 |
41 This one peeks at the search path that \texttt{isabelle} uses to |
99 The next one peeks at the search path that \texttt{isabelle} uses to |
42 locate logic images: |
100 locate logic images: |
43 \begin{ttbox} |
101 \begin{ttbox} |
44 isatool getenv -b ISABELLE_PATH |
102 isatool getenv -b ISABELLE_PATH |
45 {\out /home/mmw/isabelle/heaps/smlnj-1.09:/proj/isabelle/heaps/smlnj-1.09} |
103 {\out /home/me/isabelle/heaps/smlnj-1.09:/proj/isabelle/heaps/smlnj-1.09} |
46 \end{ttbox} |
104 \end{ttbox} |
47 We used the \texttt{-b} option to suppress the \texttt{ISABELLE_PATH=} |
105 We used the \texttt{-b} option to suppress the \texttt{ISABELLE_PATH=} |
48 prefix. The value above is what became of the following assignment in |
106 prefix. The value above is what became of the following assignment in |
49 the default settings file: |
107 the default settings file: |
50 \begin{ttbox} |
108 \begin{ttbox} |
51 ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps |
109 ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps |
52 \end{ttbox} |
110 \end{ttbox} |
53 Note how \texttt{\$ML_SYSTEM} got appended automatically to each path |
111 Note how the \texttt{ML_SYSTEM} value got appended automatically to |
54 component. This is a special feature of \texttt{ISABELLE_PATH} (and |
112 each path component. This is a special feature of |
55 also of \texttt{ISABELLE_OUTPUT}). |
113 \texttt{ISABELLE_PATH} (and also of \texttt{ISABELLE_OUTPUT}). |
56 |
114 |
57 \section{Get logic images --- \texttt{isatool findlogics}} |
|
58 |
|
59 \begin{ttbox} |
|
60 Usage: isatool findlogics |
|
61 |
|
62 Collect heap file names from ISABELLE_PATH. |
|
63 \end{ttbox} |
|
64 |
115 |
65 \section{Isabelle's version of make --- \texttt{isatool make}} |
116 \section{Isabelle's version of make --- \texttt{isatool make}} |
66 |
117 |
|
118 The Isabelle \tooldx{make} utility is a very simple wrapper for |
|
119 ordinary Unix \texttt{make}: |
67 \begin{ttbox} |
120 \begin{ttbox} |
68 Usage: isatool make [ARGS ...] |
121 Usage: isatool make [ARGS ...] |
69 |
122 |
70 Compiles logic in current directory using IsaMakefile. |
123 Compiles logic in current directory using IsaMakefile. |
71 ARGS are directly passed to the system make program. |
124 ARGS are directly passed to the system make program. |
72 \end{ttbox} |
125 \end{ttbox} |
|
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. |
73 |
133 |
74 |
134 |
75 \section{ --- \texttt{isatool usedir}} |
135 \section{Running complete logics --- \texttt{isatool usedir}} \label{sec:tool-usedir} |
76 |
136 |
|
137 FIXME |
|
138 |
|
139 %FIXME |
|
140 % -g BOOL generate theory graph data (default false) |
77 \begin{ttbox} |
141 \begin{ttbox} |
78 Usage: isatool usedir LOGIC NAME |
142 Usage: isatool usedir LOGIC NAME |
79 |
143 |
80 Options are: |
144 Options are: |
81 -b build mode (output heap image, use dir ".") |
145 -b build mode (output heap image, use dir ".") |
82 -g BOOL generate theory graph data (default false) |
|
83 -h BOOL generate theory HTML data (default false) |
146 -h BOOL generate theory HTML data (default false) |
84 -s NAME override session NAME |
147 -s NAME override session NAME |
85 |
148 |
86 Build object-logic or run examples. Also creates browsing |
149 Build object-logic or run examples. Also creates browsing |
87 information (HTML etc.) according to settings. |
150 information (HTML etc.) according to settings. |
88 \end{ttbox} |
151 \end{ttbox} |
89 |
152 |
90 |
153 FIXME |
91 \section{ --- \texttt{isatool doc}} |
|
92 |
|
93 \begin{ttbox} |
|
94 Usage: isatool doc [DOC] |
|
95 |
|
96 View Isabelle documentation DOC, or show list of available documents. |
|
97 \end{ttbox} |
|
98 |
|
99 |
|
100 \section{ --- \texttt{isatool expandshort}} |
|
101 |
|
102 \begin{ttbox} |
|
103 Usage: expandshort [FILES ...] |
|
104 |
|
105 Expand shorthand goal commands in FILES. Also contracts uses of |
|
106 resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on |
|
107 1-element lists; furthermore expands tabs, since they are now |
|
108 forbidden in ML string constants. |
|
109 |
|
110 Renames old versions of FILES by appending "~~". |
|
111 \end{ttbox} |
|