|
1 |
|
2 % $Id$ |
|
3 |
|
4 \chapter{Miscellaneous tools} |
|
5 |
|
6 |
|
7 \section{Inspecting the settings environment -- \texttt{isatool getenv}} |
|
8 \label{sec:tool-getenv} |
|
9 |
|
10 The Isabelle settings environment --- as provided by the site-default |
|
11 and user-specific settings files --- can be inspected with the |
|
12 \tooldx{getenv} utility: |
|
13 \begin{ttbox} |
|
14 Usage: isatool getenv [OPTIONS] [VARNAMES ...] |
|
15 |
|
16 Options are: |
|
17 -a display complete environment |
|
18 -b print values only (doesn't work for -a) |
|
19 |
|
20 Get value of VARNAMES from the Isabelle settings. |
|
21 \end{ttbox} |
|
22 |
|
23 With the \texttt{-a} option, one may inspect the full process |
|
24 environment that Isabelle related programs are run in. This usually |
|
25 contains much more variables than are actually Isabelle settings. |
|
26 |
|
27 Unless the \texttt{-b} option is given, the output is a list of lines |
|
28 of the form $varname\mathtt{=}value$. |
|
29 |
|
30 |
|
31 \subsection*{Examples} |
|
32 |
|
33 Get the {\ML} system identifier and the location where the compiler |
|
34 binaries are supposed to be installed as follows: |
|
35 \begin{ttbox} |
|
36 isatool getenv ML_SYSTEM ML_HOME |
|
37 {\out ML_HOME=/usr/local/sml109.27/bin} |
|
38 {\out ML_SYSTEM=smlnj-1.09} |
|
39 \end{ttbox} |
|
40 |
|
41 This one peeks at the search path that \texttt{isabelle} uses to |
|
42 locate logic images: |
|
43 \begin{ttbox} |
|
44 isatool getenv -b ISABELLE_PATH |
|
45 {\out /home/mmw/isabelle/heaps/smlnj-1.09:/proj/isabelle/heaps/smlnj-1.09} |
|
46 \end{ttbox} |
|
47 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 |
|
49 the default settings file: |
|
50 \begin{ttbox} |
|
51 ISABELLE_PATH=\$ISABELLE_HOME_USER/heaps:\$ISABELLE_HOME/heaps |
|
52 \end{ttbox} |
|
53 Note how \texttt{\$ML_SYSTEM} got appended automatically to each path |
|
54 component. This is a special feature of \texttt{ISABELLE_PATH} (and |
|
55 also of \texttt{ISABELLE_OUTPUT}). |
|
56 |
|
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 |
|
65 \section{Isabelle's version of make --- \texttt{isatool make}} |
|
66 |
|
67 \begin{ttbox} |
|
68 Usage: isatool make [ARGS ...] |
|
69 |
|
70 Compiles logic in current directory using IsaMakefile. |
|
71 ARGS are directly passed to the system make program. |
|
72 \end{ttbox} |
|
73 |
|
74 |
|
75 \section{ --- \texttt{isatool usedir}} |
|
76 |
|
77 \begin{ttbox} |
|
78 Usage: isatool usedir LOGIC NAME |
|
79 |
|
80 Options are: |
|
81 -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) |
|
84 -s NAME override session NAME |
|
85 |
|
86 Build object-logic or run examples. Also creates browsing |
|
87 information (HTML etc.) according to settings. |
|
88 \end{ttbox} |
|
89 |
|
90 |
|
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} |