29 \section{Tuning proof scripts --- \texttt{isatool expandshort}} |
29 \section{Tuning proof scripts --- \texttt{isatool expandshort}} |
30 |
30 |
31 The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance |
31 The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance |
32 readability a bit: |
32 readability a bit: |
33 \begin{ttbox} |
33 \begin{ttbox} |
34 Usage: expandshort [FILES ...] |
34 Usage: isatool expandshort [FILES ...] |
35 |
35 |
36 Expand shorthand goal commands in FILES. Also contracts uses of |
36 Expand shorthand goal commands in FILES. Also contracts uses of |
37 resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on |
37 resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on |
38 1-element lists; furthermore expands tabs, since they are now |
38 1-element lists; furthermore expands tabs, since they are now |
39 forbidden in ML string constants. |
39 forbidden in ML string constants. |
56 |
56 |
57 Collect heap file names from ISABELLE_PATH. |
57 Collect heap file names from ISABELLE_PATH. |
58 \end{ttbox} |
58 \end{ttbox} |
59 The base names of all files found on the path are printed --- sorted |
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} |
60 and with duplicates removed. Also note that \texttt{ISABELLE_PATH} |
61 implicitely depends upon \texttt{ML_SYSTEM}. Thus switching to another |
61 implicitly depends upon \texttt{ML_SYSTEM}. Thus switching to another |
62 {\ML} compiler may change the set of logic images available. |
62 {\ML} compiler may change the set of logic images available. |
63 |
63 |
64 |
64 |
65 \section{Inspecting the settings environment -- \texttt{isatool getenv}} |
65 \section{Inspecting the settings environment -- \texttt{isatool getenv}} |
66 \label{sec:tool-getenv} |
66 \label{sec:tool-getenv} |
122 |
122 |
123 Compiles logic in current directory using IsaMakefile. |
123 Compiles logic in current directory using IsaMakefile. |
124 ARGS are directly passed to the system make program. |
124 ARGS are directly passed to the system make program. |
125 \end{ttbox} |
125 \end{ttbox} |
126 Note that the Isabelle settings environment is also active. Thus one |
126 Note that the Isabelle settings environment is also active. Thus one |
127 may refer to its values within the \texttt{IsaMakefile}, e.g.\ |
127 may refer to its values within the \ttindex{IsaMakefile}, e.g.\ |
128 \texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the |
128 \texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the |
129 make file also inherit this environment. |
129 make file also inherit this environment. |
130 |
130 |
131 \medskip You may want to have a look at the \texttt{IsaMakefile}s of |
131 Typically, \texttt{IsaMakefile}s defer the real work to the |
132 the distributed object-logics as examples for your own developements. |
132 \texttt{usedir} utility, see \S\ref{sec:tool-usedir}. |
|
133 |
133 |
134 |
134 |
135 |
135 \section{Running complete logics --- \texttt{isatool usedir}} \label{sec:tool-usedir} |
136 \section{Running complete logics --- \texttt{isatool usedir}} \label{sec:tool-usedir} |
136 |
137 |
137 FIXME |
138 The \tooldx{usedir} utility builds object-logic images, or runs |
138 |
139 example sessions based on existing logics. Its usage is: |
139 %FIXME |
140 %FIXME |
140 % -g BOOL generate theory graph data (default false) |
141 % -g BOOL generate theory graph data (default false) |
141 \begin{ttbox} |
142 \begin{ttbox} |
142 Usage: isatool usedir LOGIC NAME |
143 Usage: isatool usedir LOGIC NAME |
143 |
144 |
148 |
149 |
149 Build object-logic or run examples. Also creates browsing |
150 Build object-logic or run examples. Also creates browsing |
150 information (HTML etc.) according to settings. |
151 information (HTML etc.) according to settings. |
151 \end{ttbox} |
152 \end{ttbox} |
152 |
153 |
153 FIXME |
154 The value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is |
|
155 implicitely prefixed to \emph{any} \texttt{usedir} call. Since the |
|
156 \ttindex{IsaMakefile}s of all object-logics distributed with Isabelle |
|
157 just invoke \texttt{usedir} for the real work, one may control |
|
158 compilation options globally via above variable. In particular, |
|
159 generation of \rmindex{HTML} browsing information is enabled or |
|
160 disabled this way. |
|
161 |
|
162 |
|
163 \subsection*{Options} |
|
164 |
|
165 There are two slightly different modes of operation: \emph{build} mode |
|
166 (enabled through the \texttt{-b} option) and \emph{example} mode. |
|
167 |
|
168 Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with |
|
169 input image \texttt{LOGIC} and output to \texttt{NAME}, as provided as |
|
170 arguments. This will be a batch session, executing just |
|
171 \texttt{use_dir".";}\index{*use_dir}, and then quitting. It is assumed |
|
172 that there is a file \texttt{ROOT.ML} in the current directory |
|
173 containing all {\ML} commands required to build the logic. |
|
174 |
|
175 In example mode, on the other hand, \texttt{usedir} runs a read-only |
|
176 session of \texttt{LOGIC} (typically just built before) and does an |
|
177 automatic \texttt{use_dir"NAME";}. I.e.\ it assumes that some file |
|
178 \texttt{ROOT.ML} in directory \texttt{NAME} contains appropriate {\ML} |
|
179 commands to run the desired examples. |
|
180 |
|
181 \medskip The \texttt{-h} option controls HTML browsing data |
|
182 generation. It may be explicitely turned on or off --- the last |
|
183 occurrence of some \texttt{-h} on the command line wins. |
|
184 |
|
185 \medskip Any \texttt{usedir} session is named by some \emph{session |
|
186 identifier}. These may accumulate, documenting the way sessions |
|
187 depend on others. For example, consider \texttt{Pure/FOL/ZF/ex}, which |
|
188 refers the examples of {\ZF} set theory, built upon {\FOL}, built upon |
|
189 {\Pure}. |
|
190 |
|
191 The current session's identifier is by default just the base name of |
|
192 the \texttt{LOGIC} argument (in build mode), or the \texttt{NAME} |
|
193 argument (in example mode). This may be overridden explicitely via the |
|
194 \texttt{-s} option. |
|
195 |
|
196 |
|
197 \subsection*{Examples} |
|
198 |
|
199 Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's |
|
200 object-logics as a model for your own developements. |