1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Misc}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 \isacommand{theory}\isamarkupfalse% |
|
11 \ Misc\isanewline |
|
12 \isakeyword{imports}\ Base\isanewline |
|
13 \isakeyword{begin}% |
|
14 \endisatagtheory |
|
15 {\isafoldtheory}% |
|
16 % |
|
17 \isadelimtheory |
|
18 % |
|
19 \endisadelimtheory |
|
20 % |
|
21 \isamarkupchapter{Miscellaneous tools \label{ch:tools}% |
|
22 } |
|
23 \isamarkuptrue% |
|
24 % |
|
25 \begin{isamarkuptext}% |
|
26 Subsequently we describe various Isabelle related utilities, given |
|
27 in alphabetical order.% |
|
28 \end{isamarkuptext}% |
|
29 \isamarkuptrue% |
|
30 % |
|
31 \isamarkupsection{Resolving Isabelle components \label{sec:tool-components}% |
|
32 } |
|
33 \isamarkuptrue% |
|
34 % |
|
35 \begin{isamarkuptext}% |
|
36 The \indexdef{}{tool}{components}\hypertarget{tool.components}{\hyperlink{tool.components}{\mbox{\isa{\isatool{components}}}}} tool resolves Isabelle components: |
|
37 \begin{ttbox} |
|
38 Usage: isabelle components [OPTIONS] [COMPONENTS ...] |
|
39 |
|
40 Options are: |
|
41 -R URL component repository |
|
42 (default $ISABELLE_COMPONENT_REPOSITORY) |
|
43 -a all missing components |
|
44 -l list status |
|
45 |
|
46 Resolve Isabelle components via download and installation. |
|
47 COMPONENTS are identified via base name. |
|
48 |
|
49 ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components" |
|
50 \end{ttbox} |
|
51 |
|
52 Components are initialized as described in \secref{sec:components} |
|
53 in a permissive manner, which can mark components as ``missing''. |
|
54 This state is amended by letting \hyperlink{tool.components}{\mbox{\isa{\isatool{components}}}} download and |
|
55 unpack components that are published on the default component |
|
56 repository \url{http://isabelle.in.tum.de/components/} in |
|
57 particular. |
|
58 |
|
59 Option \verb|-R| specifies an alternative component |
|
60 repository. Note that \verb|file:///| URLs can be used for |
|
61 local directories. |
|
62 |
|
63 Option \verb|-a| selects all missing components to be |
|
64 installed. Explicit components may be named as command |
|
65 line-arguments as well. Note that components are uniquely |
|
66 identified by their base name, while the installation takes place in |
|
67 the location that was specified in the attempt to initialize the |
|
68 component before. |
|
69 |
|
70 Option \verb|-l| lists the current state of available and |
|
71 missing components with their location (full name) within the |
|
72 file-system.% |
|
73 \end{isamarkuptext}% |
|
74 \isamarkuptrue% |
|
75 % |
|
76 \isamarkupsection{Displaying documents% |
|
77 } |
|
78 \isamarkuptrue% |
|
79 % |
|
80 \begin{isamarkuptext}% |
|
81 The \indexdef{}{tool}{display}\hypertarget{tool.display}{\hyperlink{tool.display}{\mbox{\isa{\isatool{display}}}}} tool displays documents in DVI or PDF |
|
82 format: |
|
83 \begin{ttbox} |
|
84 Usage: isabelle display [OPTIONS] FILE |
|
85 |
|
86 Options are: |
|
87 -c cleanup -- remove FILE after use |
|
88 |
|
89 Display document FILE (in DVI format). |
|
90 \end{ttbox} |
|
91 |
|
92 \medskip The \verb|-c| option causes the input file to be |
|
93 removed after use. The program for viewing \verb|dvi| files is |
|
94 determined by the \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isaliteral{5F}{\isacharunderscore}}VIEWER}}}} setting.% |
|
95 \end{isamarkuptext}% |
|
96 \isamarkuptrue% |
|
97 % |
|
98 \isamarkupsection{Viewing documentation \label{sec:tool-doc}% |
|
99 } |
|
100 \isamarkuptrue% |
|
101 % |
|
102 \begin{isamarkuptext}% |
|
103 The \indexdef{}{tool}{doc}\hypertarget{tool.doc}{\hyperlink{tool.doc}{\mbox{\isa{\isatool{doc}}}}} tool displays online documentation: |
|
104 \begin{ttbox} |
|
105 Usage: isabelle doc [DOC] |
|
106 |
|
107 View Isabelle documentation DOC, or show list of available documents. |
|
108 \end{ttbox} |
|
109 If called without arguments, it lists all available documents. Each |
|
110 line starts with an identifier, followed by a short description. Any |
|
111 of these identifiers may be specified as the first argument in order |
|
112 to have the corresponding document displayed. |
|
113 |
|
114 \medskip The \hyperlink{setting.ISABELLE-DOCS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DOCS}}}} setting specifies the list of |
|
115 directories (separated by colons) to be scanned for documentations. |
|
116 The program for viewing \verb|dvi| files is determined by the |
|
117 \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isaliteral{5F}{\isacharunderscore}}VIEWER}}}} setting.% |
|
118 \end{isamarkuptext}% |
|
119 \isamarkuptrue% |
|
120 % |
|
121 \isamarkupsection{Shell commands within the settings environment \label{sec:tool-env}% |
|
122 } |
|
123 \isamarkuptrue% |
|
124 % |
|
125 \begin{isamarkuptext}% |
|
126 The \indexdef{}{tool}{env}\hypertarget{tool.env}{\hyperlink{tool.env}{\mbox{\isa{\isatool{env}}}}} tool is a direct wrapper for the standard |
|
127 \verb|/usr/bin/env| command on POSIX systems, running within |
|
128 the Isabelle settings environment (\secref{sec:settings}). |
|
129 |
|
130 The command-line arguments are that of the underlying version of |
|
131 \verb|env|. For example, the following invokes an instance of |
|
132 the GNU Bash shell within the Isabelle environment: |
|
133 \begin{alltt} |
|
134 isabelle env bash |
|
135 \end{alltt}% |
|
136 \end{isamarkuptext}% |
|
137 \isamarkuptrue% |
|
138 % |
|
139 \isamarkupsection{Getting logic images% |
|
140 } |
|
141 \isamarkuptrue% |
|
142 % |
|
143 \begin{isamarkuptext}% |
|
144 The \indexdef{}{tool}{findlogics}\hypertarget{tool.findlogics}{\hyperlink{tool.findlogics}{\mbox{\isa{\isatool{findlogics}}}}} tool traverses all directories |
|
145 specified in \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PATH}}}}, looking for Isabelle logic |
|
146 images. Its usage is: |
|
147 \begin{ttbox} |
|
148 Usage: isabelle findlogics |
|
149 |
|
150 Collect heap file names from ISABELLE_PATH. |
|
151 \end{ttbox} |
|
152 |
|
153 The base names of all files found on the path are printed --- sorted |
|
154 and with duplicates removed. Also note that lookup in \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PATH}}}} includes the current values of \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}} |
|
155 and \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}}. Thus switching to another ML compiler |
|
156 may change the set of logic images available.% |
|
157 \end{isamarkuptext}% |
|
158 \isamarkuptrue% |
|
159 % |
|
160 \isamarkupsection{Inspecting the settings environment \label{sec:tool-getenv}% |
|
161 } |
|
162 \isamarkuptrue% |
|
163 % |
|
164 \begin{isamarkuptext}% |
|
165 The Isabelle settings environment --- as provided by the |
|
166 site-default and user-specific settings files --- can be inspected |
|
167 with the \indexdef{}{tool}{getenv}\hypertarget{tool.getenv}{\hyperlink{tool.getenv}{\mbox{\isa{\isatool{getenv}}}}} tool: |
|
168 \begin{ttbox} |
|
169 Usage: isabelle getenv [OPTIONS] [VARNAMES ...] |
|
170 |
|
171 Options are: |
|
172 -a display complete environment |
|
173 -b print values only (doesn't work for -a) |
|
174 -d FILE dump complete environment to FILE |
|
175 (null terminated entries) |
|
176 |
|
177 Get value of VARNAMES from the Isabelle settings. |
|
178 \end{ttbox} |
|
179 |
|
180 With the \verb|-a| option, one may inspect the full process |
|
181 environment that Isabelle related programs are run in. This usually |
|
182 contains much more variables than are actually Isabelle settings. |
|
183 Normally, output is a list of lines of the form \isa{name}\verb|=|\isa{value}. The \verb|-b| option |
|
184 causes only the values to be printed. |
|
185 |
|
186 Option \verb|-d| produces a dump of the complete environment |
|
187 to the specified file. Entries are terminated by the ASCII null |
|
188 character, i.e.\ the C string terminator.% |
|
189 \end{isamarkuptext}% |
|
190 \isamarkuptrue% |
|
191 % |
|
192 \isamarkupsubsubsection{Examples% |
|
193 } |
|
194 \isamarkuptrue% |
|
195 % |
|
196 \begin{isamarkuptext}% |
|
197 Get the location of \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} where |
|
198 user-specific information is stored: |
|
199 \begin{ttbox} |
|
200 isabelle getenv ISABELLE_HOME_USER |
|
201 \end{ttbox} |
|
202 |
|
203 \medskip Get the value only of the same settings variable, which is |
|
204 particularly useful in shell scripts: |
|
205 \begin{ttbox} |
|
206 isabelle getenv -b ISABELLE_OUTPUT |
|
207 \end{ttbox}% |
|
208 \end{isamarkuptext}% |
|
209 \isamarkuptrue% |
|
210 % |
|
211 \isamarkupsection{Installing standalone Isabelle executables \label{sec:tool-install}% |
|
212 } |
|
213 \isamarkuptrue% |
|
214 % |
|
215 \begin{isamarkuptext}% |
|
216 By default, the main Isabelle binaries (\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} etc.) are just run from their location within the |
|
217 distribution directory, probably indirectly by the shell through its |
|
218 \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}. Other schemes of installation are supported by the |
|
219 \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatool{install}}}}} tool: |
|
220 \begin{ttbox} |
|
221 Usage: isabelle install [OPTIONS] |
|
222 |
|
223 Options are: |
|
224 -d DISTDIR use DISTDIR as Isabelle distribution |
|
225 (default ISABELLE_HOME) |
|
226 -p DIR install standalone binaries in DIR |
|
227 |
|
228 Install Isabelle executables with absolute references to the current |
|
229 distribution directory. |
|
230 \end{ttbox} |
|
231 |
|
232 The \verb|-d| option overrides the current Isabelle |
|
233 distribution directory as determined by \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}. |
|
234 |
|
235 The \verb|-p| option installs executable wrapper scripts for |
|
236 \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}}, \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}, containing |
|
237 proper absolute references to the Isabelle distribution directory. |
|
238 A typical \verb|DIR| specification would be some directory |
|
239 expected to be in the shell's \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}, such as \verb|$HOME/bin|. |
|
240 |
|
241 It is possible to make symbolic links of the main Isabelle |
|
242 executables, but making separate copies outside the Isabelle |
|
243 distribution directory will not work.% |
|
244 \end{isamarkuptext}% |
|
245 \isamarkuptrue% |
|
246 % |
|
247 \isamarkupsection{Creating instances of the Isabelle logo% |
|
248 } |
|
249 \isamarkuptrue% |
|
250 % |
|
251 \begin{isamarkuptext}% |
|
252 The \indexdef{}{tool}{logo}\hypertarget{tool.logo}{\hyperlink{tool.logo}{\mbox{\isa{\isatool{logo}}}}} tool creates any instance of the generic |
|
253 Isabelle logo as EPS or PDF. |
|
254 \begin{ttbox} |
|
255 Usage: isabelle logo [OPTIONS] NAME |
|
256 |
|
257 Create instance NAME of the Isabelle logo (as EPS or PDF). |
|
258 |
|
259 Options are: |
|
260 -o OUTFILE specify output file and format |
|
261 (default "isabelle_name.pdf") |
|
262 -q quiet mode |
|
263 \end{ttbox} |
|
264 |
|
265 Option \verb|-o| specifies an explicit output file name and |
|
266 format, e.g.\ \verb|mylogo.eps| for an EPS logo. The default |
|
267 is \verb|isabelle_|\isa{name}\verb|.pdf|, with the |
|
268 lower-case version of the given name and PDF output. |
|
269 |
|
270 Option \verb|-q| omits printing of the result file name. |
|
271 |
|
272 \medskip Implementors of Isabelle tools and applications are |
|
273 encouraged to make derived Isabelle logos for their own projects |
|
274 using this template.% |
|
275 \end{isamarkuptext}% |
|
276 \isamarkuptrue% |
|
277 % |
|
278 \isamarkupsection{Isabelle wrapper for make \label{sec:tool-make}% |
|
279 } |
|
280 \isamarkuptrue% |
|
281 % |
|
282 \begin{isamarkuptext}% |
|
283 The old \indexdef{}{tool}{make}\hypertarget{tool.make}{\hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}}} tool is a very simple wrapper for |
|
284 ordinary Unix \hyperlink{executable.make}{\mbox{\isa{\isatt{make}}}}: |
|
285 \begin{ttbox} |
|
286 Usage: isabelle make [ARGS ...] |
|
287 |
|
288 Compile the logic in current directory using IsaMakefile. |
|
289 ARGS are directly passed to the system make program. |
|
290 \end{ttbox} |
|
291 |
|
292 Note that the Isabelle settings environment is also active. Thus one |
|
293 may refer to its values within the \verb|IsaMakefile|, e.g.\ |
|
294 \verb|$(ISABELLE_HOME)|. Furthermore, programs started from |
|
295 the make file also inherit this environment.% |
|
296 \end{isamarkuptext}% |
|
297 \isamarkuptrue% |
|
298 % |
|
299 \isamarkupsection{Creating Isabelle session directories |
|
300 \label{sec:tool-mkdir}% |
|
301 } |
|
302 \isamarkuptrue% |
|
303 % |
|
304 \begin{isamarkuptext}% |
|
305 The old \indexdef{}{tool}{mkdir}\hypertarget{tool.mkdir}{\hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}}} tool prepares Isabelle session |
|
306 source directories, including a sensible default setup of \verb|IsaMakefile|, \verb|ROOT.ML|, and a \verb|document| |
|
307 directory with a minimal \verb|root.tex| that is sufficient to |
|
308 print all theories of the session (in the order of appearance); see |
|
309 \secref{sec:tool-document} for further information on Isabelle |
|
310 document preparation. The usage of \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}} is: |
|
311 |
|
312 \begin{ttbox} |
|
313 Usage: isabelle mkdir [OPTIONS] [LOGIC] NAME |
|
314 |
|
315 Options are: |
|
316 -I FILE alternative IsaMakefile output |
|
317 -P include parent logic target |
|
318 -b setup build mode (session outputs heap image) |
|
319 -q quiet mode |
|
320 |
|
321 Prepare session directory, including IsaMakefile and document source, |
|
322 with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC) |
|
323 \end{ttbox} |
|
324 |
|
325 The \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}} tool is conservative in the sense that any |
|
326 existing \verb|IsaMakefile| etc.\ is left unchanged. Thus it |
|
327 is safe to invoke it multiple times, although later runs may not |
|
328 have the desired effect. |
|
329 |
|
330 Note that \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}} is unable to change \verb|IsaMakefile| |
|
331 incrementally --- manual changes are required for multiple |
|
332 sub-sessions. On order to get an initial working session, the only |
|
333 editing needed is to add appropriate \verb|use_thy| calls to the |
|
334 generated \verb|ROOT.ML| file.% |
|
335 \end{isamarkuptext}% |
|
336 \isamarkuptrue% |
|
337 % |
|
338 \isamarkupsubsubsection{Options% |
|
339 } |
|
340 \isamarkuptrue% |
|
341 % |
|
342 \begin{isamarkuptext}% |
|
343 The \verb|-I| option specifies an alternative to \verb|IsaMakefile| for dependencies. Note that ``\verb|-|'' refers |
|
344 to \emph{stdout}, i.e.\ ``\verb|-I-|'' provides an easy way |
|
345 to peek at \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}}'s idea of \hyperlink{tool.make}{\mbox{\isa{\isatool{make}}}} setup required for |
|
346 some particular of Isabelle session. |
|
347 |
|
348 \medskip The \verb|-P| option includes a target for the |
|
349 parent \verb|LOGIC| session in the generated \verb|IsaMakefile|. The corresponding sources are assumed to be located |
|
350 within the Isabelle distribution. |
|
351 |
|
352 \medskip The \verb|-b| option sets up the current directory |
|
353 as the base for a new session that provides an actual logic image, |
|
354 as opposed to one that only runs several theories based on an |
|
355 existing image. Note that in the latter case, everything except |
|
356 \verb|IsaMakefile| would be placed into a separate directory |
|
357 \verb|NAME|, rather than the current one. See |
|
358 \secref{sec:tool-usedir} for further information on \emph{build |
|
359 mode} vs.\ \emph{example mode} of \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}. |
|
360 |
|
361 \medskip The \verb|-q| option enables quiet mode, suppressing |
|
362 further notes on how to proceed.% |
|
363 \end{isamarkuptext}% |
|
364 \isamarkuptrue% |
|
365 % |
|
366 \isamarkupsection{Printing documents% |
|
367 } |
|
368 \isamarkuptrue% |
|
369 % |
|
370 \begin{isamarkuptext}% |
|
371 The \indexdef{}{tool}{print}\hypertarget{tool.print}{\hyperlink{tool.print}{\mbox{\isa{\isatool{print}}}}} tool prints documents: |
|
372 \begin{ttbox} |
|
373 Usage: isabelle print [OPTIONS] FILE |
|
374 |
|
375 Options are: |
|
376 -c cleanup -- remove FILE after use |
|
377 |
|
378 Print document FILE. |
|
379 \end{ttbox} |
|
380 |
|
381 The \verb|-c| option causes the input file to be removed |
|
382 after use. The printer spool command is determined by the \hyperlink{setting.PRINT-COMMAND}{\mbox{\isa{\isatt{PRINT{\isaliteral{5F}{\isacharunderscore}}COMMAND}}}} setting.% |
|
383 \end{isamarkuptext}% |
|
384 \isamarkuptrue% |
|
385 % |
|
386 \isamarkupsection{Remove awkward symbol names from theory sources% |
|
387 } |
|
388 \isamarkuptrue% |
|
389 % |
|
390 \begin{isamarkuptext}% |
|
391 The \indexdef{}{tool}{unsymbolize}\hypertarget{tool.unsymbolize}{\hyperlink{tool.unsymbolize}{\mbox{\isa{\isatool{unsymbolize}}}}} tool tunes Isabelle theory sources to |
|
392 improve readability for plain ASCII output (e.g.\ in email |
|
393 communication). Most notably, \hyperlink{tool.unsymbolize}{\mbox{\isa{\isatool{unsymbolize}}}} replaces awkward |
|
394 arrow symbols such as \verb|\|\verb|<Longrightarrow>| |
|
395 by \verb|==>|. |
|
396 \begin{ttbox} |
|
397 Usage: isabelle unsymbolize [FILES|DIRS...] |
|
398 |
|
399 Recursively find .thy/.ML files, removing unreadable symbol names. |
|
400 Note: this is an ad-hoc script; there is no systematic way to replace |
|
401 symbols independently of the inner syntax of a theory! |
|
402 |
|
403 Renames old versions of FILES by appending "~~". |
|
404 \end{ttbox}% |
|
405 \end{isamarkuptext}% |
|
406 \isamarkuptrue% |
|
407 % |
|
408 \isamarkupsection{Running Isabelle sessions \label{sec:tool-usedir}% |
|
409 } |
|
410 \isamarkuptrue% |
|
411 % |
|
412 \begin{isamarkuptext}% |
|
413 The old \indexdef{}{tool}{usedir}\hypertarget{tool.usedir}{\hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}} tool builds object-logic images, or |
|
414 runs example sessions based on existing logics. Its usage is: |
|
415 \begin{ttbox} |
|
416 Usage: isabelle usedir [OPTIONS] LOGIC NAME |
|
417 |
|
418 Options are: |
|
419 -C BOOL copy existing document directory to -D PATH (default true) |
|
420 -D PATH dump generated document sources into PATH |
|
421 -M MAX multithreading: maximum number of worker threads (default 1) |
|
422 -P PATH set path for remote theory browsing information |
|
423 -Q INT set threshold for sub-proof parallelization (default 50) |
|
424 -T LEVEL multithreading: trace level (default 0) |
|
425 -V VARIANT declare alternative document VARIANT |
|
426 -b build mode (output heap image, using current dir) |
|
427 -d FORMAT build document as FORMAT (default false) |
|
428 -f NAME use ML file NAME (default ROOT.ML) |
|
429 -g BOOL generate session graph image for document (default false) |
|
430 -i BOOL generate theory browser information (default false) |
|
431 -m MODE add print mode for output |
|
432 -p LEVEL set level of detail for proof objects (default 0) |
|
433 -q LEVEL set level of parallel proof checking (default 1) |
|
434 -r reset session path |
|
435 -s NAME override session NAME |
|
436 -t BOOL internal session timing (default false) |
|
437 -v BOOL be verbose (default false) |
|
438 |
|
439 Build object-logic or run examples. Also creates browsing |
|
440 information (HTML etc.) according to settings. |
|
441 |
|
442 ISABELLE_USEDIR_OPTIONS=... |
|
443 |
|
444 ML_PLATFORM=... |
|
445 ML_HOME=... |
|
446 ML_SYSTEM=... |
|
447 ML_OPTIONS=... |
|
448 \end{ttbox} |
|
449 |
|
450 Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}USEDIR{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}} |
|
451 setting is implicitly prefixed to \emph{any} \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} |
|
452 call. Since the \verb|IsaMakefile|s of all object-logics |
|
453 distributed with Isabelle just invoke \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} for the real |
|
454 work, one may control compilation options globally via above |
|
455 variable. In particular, generation of \rmindex{HTML} browsing |
|
456 information and document preparation is controlled here.% |
|
457 \end{isamarkuptext}% |
|
458 \isamarkuptrue% |
|
459 % |
|
460 \isamarkupsubsubsection{Options% |
|
461 } |
|
462 \isamarkuptrue% |
|
463 % |
|
464 \begin{isamarkuptext}% |
|
465 Basically, there are two different modes of operation: \emph{build |
|
466 mode} (enabled through the \verb|-b| option) and |
|
467 \emph{example mode} (default). |
|
468 |
|
469 Calling \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} with \verb|-b| runs \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} with input image \verb|LOGIC| and output to |
|
470 \verb|NAME|, as provided on the command line. This will be a |
|
471 batch session, running \verb|ROOT.ML| from the current |
|
472 directory and then quitting. It is assumed that \verb|ROOT.ML| |
|
473 contains all ML commands required to build the logic. |
|
474 |
|
475 In example mode, \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} runs a read-only session of |
|
476 \verb|LOGIC| and automatically runs \verb|ROOT.ML| from |
|
477 within directory \verb|NAME|. It assumes that this file |
|
478 contains appropriate ML commands to run the desired examples. |
|
479 |
|
480 \medskip The \verb|-i| option controls theory browser data |
|
481 generation. It may be explicitly turned on or off --- as usual, the |
|
482 last occurrence of \verb|-i| on the command line wins. |
|
483 |
|
484 The \verb|-P| option specifies a path (or actual URL) to be |
|
485 prefixed to any \emph{non-local} reference of existing theories. |
|
486 Thus user sessions may easily link to existing Isabelle libraries |
|
487 already present on the WWW. |
|
488 |
|
489 The \verb|-m| options specifies additional print modes to be |
|
490 activated temporarily while the session is processed. |
|
491 |
|
492 \medskip The \verb|-d| option controls document preparation. |
|
493 Valid arguments are \verb|false| (do not prepare any document; |
|
494 this is default), or any of \verb|dvi|, \verb|dvi.gz|, |
|
495 \verb|ps|, \verb|ps.gz|, \verb|pdf|. The logic |
|
496 session has to provide a properly setup \verb|document| |
|
497 directory. See \secref{sec:tool-document} and |
|
498 \secref{sec:tool-latex} for more details. |
|
499 |
|
500 \medskip The \verb|-V| option declares alternative document |
|
501 variants, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}). The standard |
|
502 document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end |
|
503 commands, proof body texts, and ML code will be presented |
|
504 faithfully. |
|
505 |
|
506 An alternative variant ``\verb|outline=/proof/ML|'' would |
|
507 fold proof and ML parts, replacing the original text by a short |
|
508 place-holder. The form ``\isa{name}\verb|=-|,'' means to |
|
509 remove document \isa{name} from the list of variants to be |
|
510 processed. Any number of \verb|-V| options may be given; |
|
511 later declarations have precedence over earlier ones. |
|
512 |
|
513 Some document variant \isa{name} may use an alternative {\LaTeX} |
|
514 entry point called \verb|document/root_|\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{22}{\isachardoublequote}}}\verb|.tex| if that file exists; otherwise the common |
|
515 \verb|document/root.tex| is used. |
|
516 |
|
517 \medskip The \verb|-g| option produces images of the theory |
|
518 dependency graph (cf.\ \secref{sec:browse}) for inclusion in the |
|
519 generated document, both as \verb|session_graph.eps| and |
|
520 \verb|session_graph.pdf| at the same time. To include this in |
|
521 the final {\LaTeX} document one could say \verb|\includegraphics{session_graph}| in \verb|document/root.tex| (omitting the file-name extension enables |
|
522 {\LaTeX} to select to correct version, either for the DVI or PDF |
|
523 output path). |
|
524 |
|
525 \medskip The \verb|-D| option causes the generated document |
|
526 sources to be dumped at location \verb|PATH|; this path is |
|
527 relative to the session's main directory. If the \verb|-C| |
|
528 option is true, this will include a copy of an existing \verb|document| directory as provided by the user. For example, \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}}~\verb|-D generated HOL Foo| produces a complete set |
|
529 of document sources at \verb|Foo/generated|. Subsequent |
|
530 invocation of \hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}~\verb|Foo/generated| (see also |
|
531 \secref{sec:tool-document}) will process the final result |
|
532 independently of an Isabelle job. This decoupled mode of operation |
|
533 facilitates debugging of serious {\LaTeX} errors, for example. |
|
534 |
|
535 \medskip The \verb|-p| option determines the level of detail |
|
536 for internal proof objects, see also the \emph{Isabelle Reference |
|
537 Manual}~\cite{isabelle-ref}. |
|
538 |
|
539 \medskip The \verb|-q| option specifies the level of parallel |
|
540 proof checking: \verb|0| no proofs, \verb|1| toplevel |
|
541 proofs (default), \verb|2| toplevel and nested Isar proofs. |
|
542 The option \verb|-Q| specifies a threshold for \verb|-q2|: nested proofs are only parallelized when the current number |
|
543 of forked proofs falls below the given value (default 50), |
|
544 multiplied by the number of worker threads (see option \verb|-M|). |
|
545 |
|
546 \medskip The \verb|-t| option produces a more detailed |
|
547 internal timing report of the session. |
|
548 |
|
549 \medskip The \verb|-v| option causes additional information |
|
550 to be printed while running the session, notably the location of |
|
551 prepared documents. |
|
552 |
|
553 \medskip The \verb|-M| option specifies the maximum number of |
|
554 parallel worker threads used for processing independent tasks when |
|
555 checking theory sources (multithreading only works on suitable ML |
|
556 platforms). The special value of \verb|0| or \verb|max| |
|
557 refers to the number of actual CPU cores of the underlying machine, |
|
558 which is a good starting point for optimal performance tuning. The |
|
559 \verb|-T| option determines the level of detail in tracing |
|
560 output concerning the internal locking and scheduling in |
|
561 multithreaded operation. This may be helpful in isolating |
|
562 performance bottle-necks, e.g.\ due to excessive wait states when |
|
563 locking critical code sections. |
|
564 |
|
565 \medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} session is named by some \emph{session |
|
566 identifier}. These accumulate, documenting the way sessions depend |
|
567 on others. For example, consider \verb|Pure/FOL/ex|, which |
|
568 refers to the examples of FOL, which in turn is built upon Pure. |
|
569 |
|
570 The current session's identifier is by default just the base name of |
|
571 the \verb|LOGIC| argument (in build mode), or of the \verb|NAME| argument (in example mode). This may be overridden explicitly |
|
572 via the \verb|-s| option.% |
|
573 \end{isamarkuptext}% |
|
574 \isamarkuptrue% |
|
575 % |
|
576 \isamarkupsection{Output the version identifier of the Isabelle distribution% |
|
577 } |
|
578 \isamarkuptrue% |
|
579 % |
|
580 \begin{isamarkuptext}% |
|
581 The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatool{version}}}}} tool displays Isabelle version information: |
|
582 \begin{ttbox} |
|
583 Usage: isabelle version [OPTIONS] |
|
584 |
|
585 Options are: |
|
586 -i short identification (derived from Mercurial id) |
|
587 |
|
588 Display Isabelle version information. |
|
589 \end{ttbox} |
|
590 |
|
591 \medskip The default is to output the full version string of the |
|
592 Isabelle distribution, e.g.\ ``\verb|Isabelle2012: May 2012|. |
|
593 |
|
594 The \verb|-i| option produces a short identification derived |
|
595 from the Mercurial id of the \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} directory.% |
|
596 \end{isamarkuptext}% |
|
597 \isamarkuptrue% |
|
598 % |
|
599 \isamarkupsection{Convert XML to YXML% |
|
600 } |
|
601 \isamarkuptrue% |
|
602 % |
|
603 \begin{isamarkuptext}% |
|
604 The \indexdef{}{tool}{yxml}\hypertarget{tool.yxml}{\hyperlink{tool.yxml}{\mbox{\isa{\isatool{yxml}}}}} tool converts a standard XML document (stdin) |
|
605 to the much simpler and more efficient YXML format of Isabelle |
|
606 (stdout). The YXML format is defined as follows. |
|
607 |
|
608 \begin{enumerate} |
|
609 |
|
610 \item The encoding is always UTF-8. |
|
611 |
|
612 \item Body text is represented verbatim (no escaping, no special |
|
613 treatment of white space, no named entities, no CDATA chunks, no |
|
614 comments). |
|
615 |
|
616 \item Markup elements are represented via ASCII control characters |
|
617 \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{5}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{6}}{\isaliteral{22}{\isachardoublequote}}} as follows: |
|
618 |
|
619 \begin{tabular}{ll} |
|
620 XML & YXML \\\hline |
|
621 \verb|<|\isa{{\isaliteral{22}{\isachardoublequote}}name\ attribute{\isaliteral{22}{\isachardoublequote}}}\verb|=|\isa{{\isaliteral{22}{\isachardoublequote}}value\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}\verb|>| & |
|
622 \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Yname\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Yattribute{\isaliteral{22}{\isachardoublequote}}}\verb|=|\isa{{\isaliteral{22}{\isachardoublequote}}value{\isaliteral{5C3C646F74733E}{\isasymdots}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} \\ |
|
623 \verb|</|\isa{name}\verb|>| & \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} \\ |
|
624 \end{tabular} |
|
625 |
|
626 There is no special case for empty body text, i.e.\ \verb|<foo/>| is treated like \verb|<foo></foo>|. Also note that |
|
627 \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}} may never occur in |
|
628 well-formed XML documents. |
|
629 |
|
630 \end{enumerate} |
|
631 |
|
632 Parsing YXML is pretty straight-forward: split the text into chunks |
|
633 separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}}, then split each chunk into |
|
634 sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}. Markup chunks start |
|
635 with an empty sub-chunk, and a second empty sub-chunk indicates |
|
636 close of an element. Any other non-empty chunk consists of plain |
|
637 text. For example, see \verb|~~/src/Pure/PIDE/yxml.ML| or |
|
638 \verb|~~/src/Pure/PIDE/yxml.scala|. |
|
639 |
|
640 YXML documents may be detected quickly by checking that the first |
|
641 two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.% |
|
642 \end{isamarkuptext}% |
|
643 \isamarkuptrue% |
|
644 % |
|
645 \isadelimtheory |
|
646 % |
|
647 \endisadelimtheory |
|
648 % |
|
649 \isatagtheory |
|
650 \isacommand{end}\isamarkupfalse% |
|
651 % |
|
652 \endisatagtheory |
|
653 {\isafoldtheory}% |
|
654 % |
|
655 \isadelimtheory |
|
656 % |
|
657 \endisadelimtheory |
|
658 \end{isabellebody}% |
|
659 %%% Local Variables: |
|
660 %%% mode: latex |
|
661 %%% TeX-master: "root" |
|
662 %%% End: |
|