|
1 (* $Id$ *) |
|
2 |
|
3 theory Presentation |
|
4 imports Pure |
|
5 begin |
|
6 |
|
7 chapter {* Presenting theories \label{ch:present} *} |
|
8 |
|
9 text {* |
|
10 Isabelle provides several ways to present the outcome of formal |
|
11 developments, including WWW-based browsable libraries or actual |
|
12 printable documents. Presentation is centered around the concept of |
|
13 \emph{logic sessions}. The global session structure is that of a |
|
14 tree, with Isabelle Pure at its root, further object-logics derived |
|
15 (e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions |
|
16 in leaf positions (usually without a separate image). |
|
17 |
|
18 The Isabelle tools @{tool_ref mkdir} and @{tool_ref make} provide |
|
19 the primary means for managing Isabelle sessions, including proper |
|
20 setup for presentation. Here the @{tool_ref usedir} tool takes care |
|
21 to let @{executable_ref "isabelle-process"} process run any |
|
22 additional stages required for document preparation, notably the |
|
23 tools @{tool_ref document} and @{tool_ref latex}. The complete tool |
|
24 chain for managing batch-mode Isabelle sessions is illustrated in |
|
25 \figref{fig:session-tools}. |
|
26 |
|
27 \begin{figure}[htbp] |
|
28 \begin{center} |
|
29 \begin{tabular}{lp{0.6\textwidth}} |
|
30 |
|
31 @{verbatim "isatool mkdir"} & invoked once by the user to create |
|
32 the initial source setup (common @{verbatim IsaMakefile} plus a |
|
33 single session directory); \\ |
|
34 |
|
35 @{verbatim "isatool make"} & invoked repeatedly by the user to |
|
36 keep session output up-to-date (HTML, documents etc.); \\ |
|
37 |
|
38 @{verbatim "isatool usedir"} & part of the standard @{verbatim |
|
39 IsaMakefile} entry of a session; \\ |
|
40 |
|
41 @{verbatim "isabelle-process"} & run through @{verbatim "isatool |
|
42 usedir"}; \\ |
|
43 |
|
44 @{verbatim "isatool document"} & run by the Isabelle process if |
|
45 document preparation is enabled; \\ |
|
46 |
|
47 @{verbatim "isatool latex"} & universal {\LaTeX} tool wrapper |
|
48 invoked multiple times by @{verbatim "isatool document"}; also |
|
49 useful for manual experiments; \\ |
|
50 |
|
51 \end{tabular} |
|
52 \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools} |
|
53 \end{center} |
|
54 \end{figure} |
|
55 *} |
|
56 |
|
57 |
|
58 section {* Generating theory browser information \label{sec:info} *} |
|
59 |
|
60 text {* |
|
61 \index{theory browsing information|bold} |
|
62 |
|
63 As a side-effect of running a logic sessions, Isabelle is able to |
|
64 generate theory browsing information, including HTML documents that |
|
65 show a theory's definition, the theorems proved in its ML file and |
|
66 the relationship with its ancestors and descendants. Besides the |
|
67 HTML file that is generated for every theory, Isabelle stores links |
|
68 to all theories in an index file. These indexes are linked with |
|
69 other indexes to represent the overall tree structure of logic |
|
70 sessions. |
|
71 |
|
72 Isabelle also generates graph files that represent the theory |
|
73 hierarchy of a logic. There is a graph browser Java applet embedded |
|
74 in the generated HTML pages, and also a stand-alone application that |
|
75 allows browsing theory graphs without having to start a WWW client |
|
76 first. The latter version also includes features such as generating |
|
77 Postscript files, which are not available in the applet version. |
|
78 See \secref{sec:browse} for further information. |
|
79 |
|
80 \medskip |
|
81 |
|
82 The easiest way to let Isabelle generate theory browsing information |
|
83 for existing sessions is to append ``@{verbatim "-i true"}'' to the |
|
84 @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim |
|
85 "isatool make"} (or @{verbatim "./build"} in the distribution). For |
|
86 example, add something like this to your Isabelle settings file |
|
87 |
|
88 \begin{ttbox} |
|
89 ISABELLE_USEDIR_OPTIONS="-i true" |
|
90 \end{ttbox} |
|
91 |
|
92 and then change into the @{verbatim "src/FOL"} directory of the |
|
93 Isabelle distribution and run @{verbatim "isatool make"}, or even |
|
94 @{verbatim "isatool make all"}. The presentation output will appear |
|
95 in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to |
|
96 @{verbatim "~/isabelle/browser_info/FOL"}. Note that option |
|
97 @{verbatim "-v true"} will make the internal runs of @{tool usedir} |
|
98 more explicit about such details. |
|
99 |
|
100 Many standard Isabelle sessions (such as @{verbatim "HOL/ex"}) also |
|
101 provide actual printable documents. These are prepared |
|
102 automatically as well if enabled like this, using the @{verbatim |
|
103 "-d"} option |
|
104 \begin{ttbox} |
|
105 ISABELLE_USEDIR_OPTIONS="-i true -d dvi" |
|
106 \end{ttbox} |
|
107 Enabling options @{verbatim "-i"} and @{verbatim "-d"} |
|
108 simultaneausly as shown above causes an appropriate ``document'' |
|
109 link to be included in the HTML index. Documents (or raw document |
|
110 sources) may be generated independently of browser information as |
|
111 well, see \secref{sec:tool-document} for further details. |
|
112 |
|
113 \bigskip The theory browsing information is stored in a |
|
114 sub-directory directory determined by the @{setting_ref |
|
115 ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the |
|
116 session identifier (according to the tree structure of sub-sessions |
|
117 by default). A complete WWW view of all standard object-logics and |
|
118 examples of the Isabelle distribution is available at the Cambridge |
|
119 or Munich Isabelle sites: |
|
120 \begin{center}\small |
|
121 \begin{tabular}{l} |
|
122 \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ |
|
123 \url{http://isabelle.in.tum.de/library/} \\ |
|
124 \end{tabular} |
|
125 \end{center} |
|
126 |
|
127 \medskip In order to present your own theories on the web, simply |
|
128 copy the corresponding subdirectory from @{setting |
|
129 ISABELLE_BROWSER_INFO} to your WWW server, having generated browser |
|
130 info like this: |
|
131 \begin{ttbox} |
|
132 isatool usedir -i true HOL Foo |
|
133 \end{ttbox} |
|
134 |
|
135 This assumes that directory @{verbatim Foo} contains some @{verbatim |
|
136 ROOT.ML} file to load all your theories, and HOL is your parent |
|
137 logic image (@{verbatim isatool}~@{tool_ref mkdir} assists in |
|
138 setting up Isabelle session directories. Theory browser information |
|
139 for HOL should have been generated already beforehand. |
|
140 Alternatively, one may specify an external link to an existing body |
|
141 of HTML data by giving @{tool usedir} a @{verbatim "-P"} option like |
|
142 this: |
|
143 \begin{ttbox} |
|
144 isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo |
|
145 \end{ttbox} |
|
146 |
|
147 \medskip For production use, the @{tool usedir} tool is usually |
|
148 invoked in an appropriate @{verbatim IsaMakefile}, via the Isabelle |
|
149 @{tool make} tool. There is a separate @{tool mkdir} tool to |
|
150 provide easy setup of all this, with only minimal manual editing |
|
151 required. |
|
152 \begin{ttbox} |
|
153 isatool mkdir HOL Foo && isatool make |
|
154 \end{ttbox} |
|
155 See \secref{sec:tool-mkdir} for more information on preparing |
|
156 Isabelle session directories, including the setup for documents. |
|
157 *} |
|
158 |
|
159 |
|
160 section {* Browsing theory graphs \label{sec:browse} *} |
|
161 |
|
162 text {* |
|
163 \index{theory graph browser|bold} |
|
164 |
|
165 The Isabelle graph browser is a general tool for visualizing |
|
166 dependency graphs. Certain nodes of the graph (i.e.~theories) can |
|
167 be grouped together in ``directories'', whose contents may be |
|
168 hidden, thus enabling the user to collapse irrelevant portions of |
|
169 information. The browser is written in Java, it can be used both as |
|
170 a stand-alone application and as an applet. Note that the option |
|
171 @{verbatim "-g"} of @{verbatim isatool}~@{tool_ref usedir} creates |
|
172 graph presentations in batch mode for inclusion in session |
|
173 documents. |
|
174 *} |
|
175 |
|
176 |
|
177 subsection {* Invoking the graph browser *} |
|
178 |
|
179 text {* |
|
180 The stand-alone version of the graph browser is wrapped up as an |
|
181 Isabelle tool called @{tool_def browser}: |
|
182 |
|
183 \begin{ttbox} |
|
184 Usage: browser [OPTIONS] [GRAPHFILE] |
|
185 |
|
186 Options are: |
|
187 -c cleanup -- remove GRAPHFILE after use |
|
188 -o FILE output to FILE (ps, eps, pdf) |
|
189 \end{ttbox} |
|
190 When no filename is specified, the browser automatically changes to |
|
191 the directory @{setting ISABELLE_BROWSER_INFO}. |
|
192 |
|
193 \medskip The @{verbatim "-c"} option causes the input file to be |
|
194 removed after use. |
|
195 |
|
196 The @{verbatim "-o"} option indicates batch-mode operation, with the |
|
197 output written to the indicated file; note that @{verbatim pdf} |
|
198 produces an @{verbatim eps} copy as well. |
|
199 |
|
200 \medskip The applet version of the browser is part of the standard |
|
201 WWW theory presentation, see the link ``theory dependencies'' within |
|
202 each session index. |
|
203 *} |
|
204 |
|
205 |
|
206 subsection {* Using the graph browser *} |
|
207 |
|
208 text {* |
|
209 The browser's main window, which is shown in |
|
210 \figref{fig:browserwindow}, consists of two sub-windows. In the |
|
211 left sub-window, the directory tree is displayed. The graph itself |
|
212 is displayed in the right sub-window. |
|
213 |
|
214 \begin{figure}[ht] |
|
215 \includegraphics[width=\textwidth]{browser_screenshot} |
|
216 \caption{\label{fig:browserwindow} Browser main window} |
|
217 \end{figure} |
|
218 *} |
|
219 |
|
220 |
|
221 subsubsection {* The directory tree window *} |
|
222 |
|
223 text {* |
|
224 We describe the usage of the directory browser and the meaning of |
|
225 the different items in the browser window. |
|
226 |
|
227 \begin{itemize} |
|
228 |
|
229 \item A red arrow before a directory name indicates that the |
|
230 directory is currently ``folded'', i.e.~the nodes in this directory |
|
231 are collapsed to one single node. In the right sub-window, the names |
|
232 of nodes corresponding to folded directories are enclosed in square |
|
233 brackets and displayed in red color. |
|
234 |
|
235 \item A green downward arrow before a directory name indicates that |
|
236 the directory is currently ``unfolded''. It can be folded by |
|
237 clicking on the directory name. Clicking on the name for a second |
|
238 time unfolds the directory again. Alternatively, a directory can |
|
239 also be unfolded by clicking on the corresponding node in the right |
|
240 sub-window. |
|
241 |
|
242 \item Blue arrows stand before ordinary node names. When clicking on |
|
243 such a name (i.e.\ that of a theory), the graph display window |
|
244 focuses to the corresponding node. Double clicking invokes a text |
|
245 viewer window in which the contents of the theory file are |
|
246 displayed. |
|
247 |
|
248 \end{itemize} |
|
249 *} |
|
250 |
|
251 |
|
252 subsubsection {* The graph display window *} |
|
253 |
|
254 text {* |
|
255 When pointing on an ordinary node, an upward and a downward arrow is |
|
256 shown. Initially, both of these arrows are green. Clicking on the |
|
257 upward or downward arrow collapses all predecessor or successor |
|
258 nodes, respectively. The arrow's color then changes to red, |
|
259 indicating that the predecessor or successor nodes are currently |
|
260 collapsed. The node corresponding to the collapsed nodes has the |
|
261 name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply |
|
262 click on the red arrow or on the node with the name ``@{verbatim |
|
263 "[....]"}''. Similar to the directory browser, the contents of |
|
264 theory files can be displayed by double clicking on the |
|
265 corresponding node. |
|
266 *} |
|
267 |
|
268 |
|
269 subsubsection {* The ``File'' menu *} |
|
270 |
|
271 text {* |
|
272 Due to Java Applet security restrictions this menu is only available |
|
273 in the full application version. The meaning of the menu items is as |
|
274 follows: |
|
275 |
|
276 \begin{description} |
|
277 |
|
278 \item[Open \dots] Open a new graph file. |
|
279 |
|
280 \item[Export to PostScript] Outputs the current graph in Postscript |
|
281 format, appropriately scaled to fit on one single sheet of A4 paper. |
|
282 The resulting file can be printed directly. |
|
283 |
|
284 \item[Export to EPS] Outputs the current graph in Encapsulated |
|
285 Postscript format. The resulting file can be included in other |
|
286 documents. |
|
287 |
|
288 \item[Quit] Quit the graph browser. |
|
289 |
|
290 \end{description} |
|
291 *} |
|
292 |
|
293 |
|
294 subsection {* Syntax of graph definition files *} |
|
295 |
|
296 text {* |
|
297 A graph definition file has the following syntax: |
|
298 |
|
299 \begin{tabular}{rcl} |
|
300 @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\ |
|
301 @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"} |
|
302 \end{tabular} |
|
303 |
|
304 The meaning of the items in a vertex description is as follows: |
|
305 |
|
306 \begin{description} |
|
307 |
|
308 \item[@{text vertex_name}] The name of the vertex. |
|
309 |
|
310 \item[@{text vertex_ID}] The vertex identifier. Note that there may |
|
311 be several vertices with equal names, whereas identifiers must be |
|
312 unique. |
|
313 |
|
314 \item[@{text dir_name}] The name of the ``directory'' the vertex |
|
315 should be placed in. A ``@{verbatim "+"}'' sign after @{text |
|
316 dir_name} indicates that the nodes in the directory are initially |
|
317 visible. Directories are initially invisible by default. |
|
318 |
|
319 \item[@{text path}] The path of the corresponding theory file. This |
|
320 is specified relatively to the path of the graph definition file. |
|
321 |
|
322 \item[List of successor/predecessor nodes] A ``@{verbatim "<"}'' |
|
323 sign before the list means that successor nodes are listed, a |
|
324 ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If |
|
325 neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the |
|
326 browser assumes that successor nodes are listed. |
|
327 |
|
328 \end{description} |
|
329 *} |
|
330 |
|
331 |
|
332 section {* Creating Isabelle session directories |
|
333 \label{sec:tool-mkdir} *} |
|
334 |
|
335 text {* |
|
336 The @{tool_def mkdir} utility prepares Isabelle session source |
|
337 directories, including a sensible default setup of @{verbatim |
|
338 IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document} |
|
339 directory with a minimal @{verbatim root.tex} that is sufficient to |
|
340 print all theories of the session (in the order of appearance); see |
|
341 \secref{sec:tool-document} for further information on Isabelle |
|
342 document preparation. The usage of @{verbatim "isatool mkdir"} is: |
|
343 |
|
344 \begin{ttbox} |
|
345 Usage: mkdir [OPTIONS] [LOGIC] NAME |
|
346 |
|
347 Options are: |
|
348 -I FILE alternative IsaMakefile output |
|
349 -P include parent logic target |
|
350 -b setup build mode (session outputs heap image) |
|
351 -q quiet mode |
|
352 |
|
353 Prepare session directory, including IsaMakefile and document source, |
|
354 with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC) |
|
355 \end{ttbox} |
|
356 |
|
357 The @{tool mkdir} tool is conservative in the sense that any |
|
358 existing @{verbatim IsaMakefile} etc.\ is left unchanged. Thus it |
|
359 is safe to invoke it multiple times, although later runs may not |
|
360 have the desired effect. |
|
361 |
|
362 Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile} |
|
363 incrementally --- manual changes are required for multiple |
|
364 sub-sessions. On order to get an initial working session, the only |
|
365 editing needed is to add appropriate @{ML use_thy} calls to the |
|
366 generated @{verbatim ROOT.ML} file. |
|
367 *} |
|
368 |
|
369 |
|
370 subsubsection {* Options *} |
|
371 |
|
372 text {* |
|
373 The @{verbatim "-I"} option specifies an alternative to @{verbatim |
|
374 IsaMakefile} for dependencies. Note that ``@{verbatim "-"}'' refers |
|
375 to \emph{stdout}, i.e.\ ``@{verbatim "-I-"}'' provides an easy way |
|
376 to peek at @{tool mkdir}'s idea of @{tool make} setup required for |
|
377 some particular of Isabelle session. |
|
378 |
|
379 \medskip The @{verbatim "-P"} option includes a target for the |
|
380 parent @{verbatim LOGIC} session in the generated @{verbatim |
|
381 IsaMakefile}. The corresponding sources are assumed to be located |
|
382 within the Isabelle distribution. |
|
383 |
|
384 \medskip The @{verbatim "-b"} option sets up the current directory |
|
385 as the base for a new session that provides an actual logic image, |
|
386 as opposed to one that only runs several theories based on an |
|
387 existing image. Note that in the latter case, everything except |
|
388 @{verbatim IsaMakefile} would be placed into a separate directory |
|
389 @{verbatim NAME}, rather than the current one. See |
|
390 \secref{sec:tool-usedir} for further information on \emph{build |
|
391 mode} vs.\ \emph{example mode} of the @{tool usedir} utility. |
|
392 |
|
393 \medskip The @{verbatim "-q"} option enables quiet mode, suppressing |
|
394 further notes on how to proceed. |
|
395 *} |
|
396 |
|
397 |
|
398 subsubsection {* Examples *} |
|
399 |
|
400 text {* |
|
401 The standard setup of a single ``example session'' based on the |
|
402 default logic, with proper document generation is generated like |
|
403 this: |
|
404 \begin{ttbox} |
|
405 isatool mkdir Foo && isatool make |
|
406 \end{ttbox} |
|
407 |
|
408 \noindent The theory sources should be put into the @{verbatim Foo} |
|
409 directory, and its @{verbatim ROOT.ML} should be edited to load all |
|
410 required theories. Invoking @{verbatim "isatool make"} again would |
|
411 run the whole session, generating browser information and the |
|
412 document automatically. The @{verbatim IsaMakefile} is typically |
|
413 tuned manually later, e.g.\ adding source dependencies, or changing |
|
414 the options passed to @{tool usedir}. |
|
415 |
|
416 \medskip Large projects may demand further sessions, potentially |
|
417 with separate logic images being created. This usually requires |
|
418 manual editing of the generated @{verbatim IsaMakefile}, which is |
|
419 meant to cover all of the sub-session directories at the same time |
|
420 (this is the deeper reasong why @{verbatim IsaMakefile} is not made |
|
421 part of the initial session directory created by @{verbatim "isatool |
|
422 mkdir"}). See @{verbatim "src/HOL/IsaMakefile"} of the Isabelle |
|
423 distribution for a full-blown example. |
|
424 *} |
|
425 |
|
426 |
|
427 section {* Running Isabelle sessions \label{sec:tool-usedir} *} |
|
428 |
|
429 text {* |
|
430 The @{tool_def usedir} utility builds object-logic images, or runs |
|
431 example sessions based on existing logics. Its usage is: |
|
432 \begin{ttbox} |
|
433 |
|
434 Usage: usedir [OPTIONS] LOGIC NAME |
|
435 |
|
436 Options are: |
|
437 -C BOOL copy existing document directory to -D PATH (default true) |
|
438 -D PATH dump generated document sources into PATH |
|
439 -M MAX multithreading: maximum number of worker threads (default 1) |
|
440 -P PATH set path for remote theory browsing information |
|
441 -T LEVEL multithreading: trace level (default 0) |
|
442 -V VERSION declare alternative document VERSION |
|
443 -b build mode (output heap image, using current dir) |
|
444 -c BOOL tell ML system to compress output image (default true) |
|
445 -d FORMAT build document as FORMAT (default false) |
|
446 -f NAME use ML file NAME (default ROOT.ML) |
|
447 -g BOOL generate session graph image for document (default false) |
|
448 -i BOOL generate theory browser information (default false) |
|
449 -m MODE add print mode for output |
|
450 -p LEVEL set level of detail for proof objects |
|
451 -r reset session path |
|
452 -s NAME override session NAME |
|
453 -v BOOL be verbose (default false) |
|
454 |
|
455 Build object-logic or run examples. Also creates browsing |
|
456 information (HTML etc.) according to settings. |
|
457 |
|
458 ISABELLE_USEDIR_OPTIONS= |
|
459 HOL_USEDIR_OPTIONS= |
|
460 \end{ttbox} |
|
461 |
|
462 Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS} |
|
463 setting is implicitly prefixed to \emph{any} @{tool usedir} |
|
464 call. Since the @{verbatim IsaMakefile}s of all object-logics |
|
465 distributed with Isabelle just invoke \texttt{usedir} for the real |
|
466 work, one may control compilation options globally via above |
|
467 variable. In particular, generation of \rmindex{HTML} browsing |
|
468 information and document preparation is controlled here. |
|
469 |
|
470 The @{setting_ref HOL_USEDIR_OPTIONS} setting is specific to the |
|
471 plain and main Isabelle/HOL images; its value is appended to |
|
472 @{setting ISABELLE_USEDIR_OPTIONS} for these particular sessions |
|
473 only. |
|
474 *} |
|
475 |
|
476 |
|
477 subsubsection {* Options *} |
|
478 |
|
479 text {* |
|
480 Basically, there are two different modes of operation: \emph{build |
|
481 mode} (enabled through the @{verbatim "-b"} option) and |
|
482 \emph{example mode} (default). |
|
483 |
|
484 Calling @{tool usedir} with @{verbatim "-b"} runs @{executable |
|
485 "isabelle-process"} with input image @{verbatim LOGIC} and output to |
|
486 @{verbatim NAME}, as provided on the command line. This will be a |
|
487 batch session, running @{verbatim ROOT.ML} from the current |
|
488 directory and then quitting. It is assumed that @{verbatim ROOT.ML} |
|
489 contains all ML commands required to build the logic. |
|
490 |
|
491 In example mode, @{verbatim usedir} runs a read-only session of |
|
492 @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from |
|
493 within directory @{verbatim NAME}. It assumes that this file |
|
494 contains appropriate ML commands to run the desired examples. |
|
495 |
|
496 \medskip The @{verbatim "-i"} option controls theory browser data |
|
497 generation. It may be explicitly turned on or off --- as usual, the |
|
498 last occurrence of @{verbatim "-i"} on the command line wins. |
|
499 |
|
500 The @{verbatim "-P"} option specifies a path (or actual URL) to be |
|
501 prefixed to any \emph{non-local} reference of existing theories. |
|
502 Thus user sessions may easily link to existing Isabelle libraries |
|
503 already present on the WWW. |
|
504 |
|
505 The @{verbatim "-m"} options specifies additional print modes to be |
|
506 activated temporarily while the session is processed. |
|
507 |
|
508 \medskip The @{verbatim "-d"} option controls document preparation. |
|
509 Valid arguments are @{verbatim false} (do not prepare any document; |
|
510 this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz}, |
|
511 @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}. The logic |
|
512 session has to provide a properly setup @{verbatim document} |
|
513 directory. See \secref{sec:tool-document} and |
|
514 \secref{sec:tool-latex} for more details. |
|
515 |
|
516 \medskip The @{verbatim "-V"} option declares alternative document |
|
517 versions, consisting of name/tags pairs (cf.\ options @{verbatim |
|
518 "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool). The |
|
519 standard document is equivalent to ``@{verbatim |
|
520 "document=theory,proof,ML"}'', which means that all theory begin/end |
|
521 commands, proof body texts, and ML code will be presented |
|
522 faithfully. An alternative version ``@{verbatim |
|
523 "outline=/proof/ML"}'' would fold proof and ML parts, replacing the |
|
524 original text by a short place-holder. The form ``@{text |
|
525 name}@{verbatim "=-"},'' means to remove document @{text name} from |
|
526 the list of versions to be processed. Any number of @{verbatim |
|
527 "-V"} options may be given; later declarations have precedence over |
|
528 earlier ones. |
|
529 |
|
530 \medskip The @{verbatim "-g"} option produces images of the theory |
|
531 dependency graph (cf.\ \secref{sec:browse}) for inclusion in the |
|
532 generated document, both as @{verbatim session_graph.eps} and |
|
533 @{verbatim session_graph.pdf} at the same time. To include this in |
|
534 the final {\LaTeX} document one could say @{verbatim |
|
535 "\\includegraphics{session_graph}"} in @{verbatim |
|
536 "document/root.tex"} (omitting the file-name extension enables |
|
537 {\LaTeX} to select to correct version, either for the DVI or PDF |
|
538 output path). |
|
539 |
|
540 \medskip The @{verbatim "-D"} option causes the generated document |
|
541 sources to be dumped at location @{verbatim PATH}; this path is |
|
542 relative to the session's main directory. If the @{verbatim "-C"} |
|
543 option is true, this will include a copy of an existing @{verbatim |
|
544 document} directory as provided by the user. For example, |
|
545 @{verbatim "isatool usedir -D generated HOL Foo"} produces a |
|
546 complete set of document sources at @{verbatim "Foo/generated"}. |
|
547 Subsequent invocation of @{verbatim "isatool document |
|
548 Foo/generated"} (see also \secref{sec:tool-document}) will process |
|
549 the final result independently of an Isabelle job. This decoupled |
|
550 mode of operation facilitates debugging of serious {\LaTeX} errors, |
|
551 for example. |
|
552 |
|
553 \medskip The @{verbatim "-p"} option determines the level of detail |
|
554 for internal proof objects, see also the \emph{Isabelle Reference |
|
555 Manual}~\cite{isabelle-ref}. |
|
556 |
|
557 \medskip The @{verbatim "-v"} option causes additional information |
|
558 to be printed while running the session, notably the location of |
|
559 prepared documents. |
|
560 |
|
561 \medskip The @{verbatim "-M"} option specifies the maximum number of |
|
562 parallel threads used for processing independent tasks when checking |
|
563 theory sources (multithreading only works on suitable ML platforms). |
|
564 The special value of ``@{verbatim 0}'' or ``@{verbatim max}'' refers |
|
565 to the number of actual CPU cores of the underlying machine, which |
|
566 is a good starting point for optimal performance tuning. The |
|
567 @{verbatim "-T"} option determines the level of detail in tracing |
|
568 output concerning the internal locking and scheduling in |
|
569 multithreaded operation. This may be helpful in isolating |
|
570 performance bottle-necks, e.g.\ due to excessive wait states when |
|
571 locking critical code sections. |
|
572 |
|
573 \medskip Any @{tool usedir} session is named by some \emph{session |
|
574 identifier}. These accumulate, documenting the way sessions depend |
|
575 on others. For example, consider @{verbatim "Pure/FOL/ex"}, which |
|
576 refers to the examples of FOL, which in turn is built upon Pure. |
|
577 |
|
578 The current session's identifier is by default just the base name of |
|
579 the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim |
|
580 NAME} argument (in example mode). This may be overridden explicitly |
|
581 via the @{verbatim "-s"} option. |
|
582 *} |
|
583 |
|
584 |
|
585 subsubsection {* Examples *} |
|
586 |
|
587 text {* |
|
588 Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's |
|
589 object-logics as a model for your own developments. For example, |
|
590 see @{verbatim "src/FOL/IsaMakefile"}. The Isabelle @{tool_ref |
|
591 mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation |
|
592 of @{tool usedir} as well. |
|
593 *} |
|
594 |
|
595 |
|
596 section {* Preparing Isabelle session documents |
|
597 \label{sec:tool-document} *} |
|
598 |
|
599 text {* |
|
600 The @{tool_def document} utility prepares logic session documents, |
|
601 processing the sources both as provided by the user and generated by |
|
602 Isabelle. Its usage is: |
|
603 \begin{ttbox} |
|
604 Usage: document [OPTIONS] [DIR] |
|
605 |
|
606 Options are: |
|
607 -c cleanup -- be aggressive in removing old stuff |
|
608 -n NAME specify document name (default 'document') |
|
609 -o FORMAT specify output format: dvi (default), dvi.gz, ps, |
|
610 ps.gz, pdf |
|
611 -t TAGS specify tagged region markup |
|
612 |
|
613 Prepare the theory session document in DIR (default 'document') |
|
614 producing the specified output format. |
|
615 \end{ttbox} |
|
616 This tool is usually run automatically as part of the corresponding |
|
617 Isabelle batch process, provided document preparation has been |
|
618 enabled (cf.\ the @{verbatim "-d"} option of the @{tool_ref usedir} |
|
619 tool). It may be manually invoked on the generated browser |
|
620 information document output as well, e.g.\ in case of errors |
|
621 encountered in the batch run. |
|
622 |
|
623 \medskip The @{verbatim "-c"} option tells the @{tool document} tool |
|
624 to dispose the document sources after successful operation. This is |
|
625 the right thing to do for sources generated by an Isabelle process, |
|
626 but take care of your files in manual document preparation! |
|
627 |
|
628 \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify |
|
629 the final output file name and format, the default is ``@{verbatim |
|
630 document.dvi}''. Note that the result will appear in the parent of |
|
631 the target @{verbatim DIR}. |
|
632 |
|
633 \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret |
|
634 tagged Isabelle command regions. Tags are specified as a comma |
|
635 separated list of modifier/name pairs: ``@{verbatim "+"}@{text |
|
636 foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim |
|
637 "-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to |
|
638 fold text tagged as @{text foo}. The builtin default is equivalent |
|
639 to the tag specification ``@{verbatim |
|
640 "/theory,/proof,/ML,+visible,-invisible"}''; see also the {\LaTeX} |
|
641 macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and |
|
642 @{verbatim "\\isafoldtag"}, in @{verbatim isabelle.sty}. |
|
643 |
|
644 \medskip Document preparation requires a properly setup ``@{verbatim |
|
645 document}'' directory within the logic session sources. This |
|
646 directory is supposed to contain all the files needed to produce the |
|
647 final document --- apart from the actual theories which are |
|
648 generated by Isabelle. |
|
649 |
|
650 \medskip For most practical purposes, the @{tool document} tool is |
|
651 smart enough to create any of the specified output formats, taking |
|
652 @{verbatim root.tex} supplied by the user as a starting point. This |
|
653 even includes multiple runs of {\LaTeX} to accommodate references |
|
654 and bibliographies (the latter assumes @{verbatim root.bib} within |
|
655 the same directory). |
|
656 |
|
657 In more complex situations, a separate @{verbatim IsaMakefile} for |
|
658 the document sources may be given instead. This should provide |
|
659 targets for any admissible document format; these have to produce |
|
660 corresponding output files named after @{verbatim root} as well, |
|
661 e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}. |
|
662 |
|
663 \medskip When running the session, Isabelle copies the original |
|
664 @{verbatim document} directory into its proper place within |
|
665 @{verbatim ISABELLE_BROWSER_INFO} according to the session path. |
|
666 Then, for any processed theory @{text A} some {\LaTeX} source is |
|
667 generated and put there as @{text A}@{verbatim ".tex"}. |
|
668 Furthermore, a list of all generated theory files is put into |
|
669 @{verbatim session.tex}. Typically, the root {\LaTeX} file provided |
|
670 by the user would include @{verbatim session.tex} to get a document |
|
671 containing all the theories. |
|
672 |
|
673 The {\LaTeX} versions of the theories require some macros defined in |
|
674 @{verbatim isabelle.sty} as distributed with Isabelle. Doing |
|
675 @{verbatim "\\usepackage{isabelle}"} in @{verbatim root.tex} should |
|
676 be fine; the underlying Isabelle @{tool latex} tool already includes |
|
677 an appropriate path specification for {\TeX} inputs. |
|
678 |
|
679 If the text contains any references to Isabelle symbols (such as |
|
680 @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim |
|
681 isabellesym.sty} should be included as well. This package contains |
|
682 a standard set of {\LaTeX} macro definitions @{verbatim |
|
683 "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim |
|
684 "<"}@{text foo}@{verbatim ">"}, (see \appref{app:symbols} for a |
|
685 complete list of predefined Isabelle symbols). Users may invent |
|
686 further symbols as well, just by providing {\LaTeX} macros in a |
|
687 similar fashion as in @{verbatim isabellesym.sty} of the |
|
688 distribution. |
|
689 |
|
690 For proper setup of DVI and PDF documents (with hyperlinks and |
|
691 bookmarks), we recommend to include @{verbatim pdfsetup.sty} as |
|
692 well. |
|
693 |
|
694 \medskip As a final step of document preparation within Isabelle, |
|
695 @{verbatim "isatool document -c"} is run on the resulting @{verbatim |
|
696 document} directory. Thus the actual output document is built and |
|
697 installed in its proper place (as linked by the session's @{verbatim |
|
698 index.html} if option @{verbatim "-i"} of @{tool_ref usedir} has |
|
699 been enabled, cf.\ \secref{sec:info}). The generated sources are |
|
700 deleted after successful run of {\LaTeX} and friends. Note that a |
|
701 separate copy of the sources may be retained by passing an option |
|
702 @{verbatim "-D"} to the @{tool usedir} utility when running the |
|
703 session. |
|
704 *} |
|
705 |
|
706 |
|
707 section {* Running {\LaTeX} within the Isabelle environment |
|
708 \label{sec:tool-latex} *} |
|
709 |
|
710 text {* |
|
711 The @{tool_def latex} utility provides the basic interface for |
|
712 Isabelle document preparation. Its usage is: |
|
713 \begin{ttbox} |
|
714 Usage: latex [OPTIONS] [FILE] |
|
715 |
|
716 Options are: |
|
717 -o FORMAT specify output format: dvi (default), dvi.gz, ps, |
|
718 ps.gz, pdf, bbl, idx, sty, syms |
|
719 |
|
720 Run LaTeX (and related tools) on FILE (default root.tex), |
|
721 producing the specified output format. |
|
722 \end{ttbox} |
|
723 |
|
724 Appropriate {\LaTeX}-related programs are run on the input file, |
|
725 according to the given output format: @{executable latex}, |
|
726 @{executable pdflatex}, @{executable dvips}, @{executable bibtex} |
|
727 (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim |
|
728 idx}). The actual commands are determined from the settings |
|
729 environment (@{setting ISABELLE_LATEX} etc.). |
|
730 |
|
731 The @{verbatim sty} output format causes the Isabelle style files to |
|
732 be updated from the distribution. This is useful in special |
|
733 situations where the document sources are to be processed another |
|
734 time by separate tools (cf.\ option @{verbatim "-D"} of the @{tool |
|
735 usedir} utility). |
|
736 |
|
737 The @{verbatim syms} output is for internal use; it generates lists |
|
738 of symbols that are available without loading additional {\LaTeX} |
|
739 packages. |
|
740 *} |
|
741 |
|
742 |
|
743 subsubsection {* Examples *} |
|
744 |
|
745 text {* |
|
746 Invoking @{verbatim "isatool latex"} by hand may be occasionally |
|
747 useful when debugging failed attempts of the automatic document |
|
748 preparation stage of batch-mode Isabelle. The abortive process |
|
749 leaves the sources at a certain place within @{setting |
|
750 ISABELLE_BROWSER_INFO}, see the runtime error message for details. |
|
751 This enables users to inspect {\LaTeX} runs in further detail, e.g.\ |
|
752 like this: |
|
753 \begin{ttbox} |
|
754 cd ~/isabelle/browser_info/HOL/Test/document |
|
755 isatool latex -o pdf |
|
756 \end{ttbox} |
|
757 *} |
|
758 |
|
759 end |