56 section {* Generating theory browser information \label{sec:info} *} |
51 section {* Generating theory browser information \label{sec:info} *} |
57 |
52 |
58 text {* |
53 text {* |
59 \index{theory browsing information|bold} |
54 \index{theory browsing information|bold} |
60 |
55 |
61 As a side-effect of running a logic sessions, Isabelle is able to |
56 As a side-effect of building sessions, Isabelle is able to generate |
62 generate theory browsing information, including HTML documents that |
57 theory browsing information, including HTML documents that show the |
63 show a theory's definition, the theorems proved in its ML file and |
58 theory sources and the relationship with its ancestors and |
64 the relationship with its ancestors and descendants. Besides the |
59 descendants. Besides the HTML file that is generated for every |
65 HTML file that is generated for every theory, Isabelle stores links |
60 theory, Isabelle stores links to all theories in an index |
66 to all theories in an index file. These indexes are linked with |
61 file. These indexes are linked with other indexes to represent the |
67 other indexes to represent the overall tree structure of logic |
62 overall tree structure of the sessions. |
68 sessions. |
|
69 |
63 |
70 Isabelle also generates graph files that represent the theory |
64 Isabelle also generates graph files that represent the theory |
71 hierarchy of a logic. There is a graph browser Java applet embedded |
65 dependencies within a session. There is a graph browser Java applet |
72 in the generated HTML pages, and also a stand-alone application that |
66 embedded in the generated HTML pages, and also a stand-alone |
73 allows browsing theory graphs without having to start a WWW client |
67 application that allows browsing theory graphs without having to |
74 first. The latter version also includes features such as generating |
68 start a WWW client first. The latter version also includes features |
75 Postscript files, which are not available in the applet version. |
69 such as generating Postscript files, which are not available in the |
76 See \secref{sec:browse} for further information. |
70 applet version. See \secref{sec:browse} for further information. |
77 |
71 |
78 \medskip |
72 \medskip |
79 |
73 |
80 The easiest way to let Isabelle generate theory browsing information |
74 The easiest way to let Isabelle generate theory browsing information |
81 for existing sessions is to append ``@{verbatim "-i true"}'' to the |
75 for existing sessions is to invoke @{tool build} with suitable |
82 @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{tool make}. |
76 options: |
83 For example, add something like this to your Isabelle settings file |
77 |
84 |
78 \begin{ttbox} |
85 \begin{ttbox} |
79 isabelle build -o browser_info -v -c FOL |
86 ISABELLE_USEDIR_OPTIONS="-i true" |
80 \end{ttbox} |
87 \end{ttbox} |
81 |
88 |
82 The presentation output will appear in @{verbatim |
89 and then change into the @{file "~~/src/FOL"} directory and run |
83 "$ISABELLE_BROWSER_INFO/FOL"} as reported by the above verbose |
90 @{tool make}, or even @{tool make}~@{verbatim all}. The |
84 invocation of the build process. |
91 presentation output will appear in @{verbatim |
85 |
92 "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to something like |
86 Many Isabelle sessions (such as @{verbatim "HOL-Library"} in @{file |
93 @{verbatim "~/.isabelle/IsabelleXXXX/browser_info/FOL"}. Note that |
87 "~~/src/HOL/Library"}) also provide actual printable documents. |
94 option @{verbatim "-v true"} will make the internal runs of @{tool |
88 These are prepared automatically as well if enabled like this: |
95 usedir} more explicit about such details. |
89 \begin{ttbox} |
96 |
90 isabelle build -o browser_info -o document=pdf -v -c HOL-Library |
97 Many standard Isabelle sessions (such as @{file "~~/src/HOL/ex"}) |
91 \end{ttbox} |
98 also provide actual printable documents. These are prepared |
92 |
99 automatically as well if enabled like this, using the @{verbatim |
93 Enabling both browser info and document preparation simultaneously |
100 "-d"} option |
94 causes an appropriate ``document'' link to be included in the HTML |
101 \begin{ttbox} |
95 index. Documents may be generated independently of browser |
102 ISABELLE_USEDIR_OPTIONS="-i true -d dvi" |
96 information as well, see \secref{sec:tool-document} for further |
103 \end{ttbox} |
97 details. |
104 Enabling options @{verbatim "-i"} and @{verbatim "-d"} |
|
105 simultaneously as shown above causes an appropriate ``document'' |
|
106 link to be included in the HTML index. Documents (or raw document |
|
107 sources) may be generated independently of browser information as |
|
108 well, see \secref{sec:tool-document} for further details. |
|
109 |
98 |
110 \bigskip The theory browsing information is stored in a |
99 \bigskip The theory browsing information is stored in a |
111 sub-directory directory determined by the @{setting_ref |
100 sub-directory directory determined by the @{setting_ref |
112 ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the |
101 ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the |
113 session identifier (according to the tree structure of sub-sessions |
102 session identifier (according to the tree structure of sub-sessions |
114 by default). A complete WWW view of all standard object-logics and |
103 by default). In order to present Isabelle applications on the web, |
115 examples of the Isabelle distribution is available at the usual |
104 the corresponding subdirectory from @{setting ISABELLE_BROWSER_INFO} |
116 Isabelle sites: |
105 can be put on a WWW server. |
117 \begin{center}\small |
106 *} |
118 \begin{tabular}{l} |
107 |
119 \url{http://isabelle.in.tum.de/dist/library/} \\ |
108 section {* Preparing session root directories \label{sec:tool-mkroot} *} |
120 \url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/} \\ |
109 |
121 \url{http://mirror.cse.unsw.edu.au/pub/isabelle/dist/library/} \\ |
110 text {* The @{tool_def mkroot} tool configures a given directory as |
122 \end{tabular} |
111 session root, with some @{verbatim ROOT} file and optional document |
123 \end{center} |
112 source directory. Its usage is: |
124 |
113 \begin{ttbox} |
125 \medskip In order to present your own theories on the web, simply |
114 Usage: isabelle mkroot [OPTIONS] [DIR] |
126 copy the corresponding subdirectory from @{setting |
|
127 ISABELLE_BROWSER_INFO} to your WWW server, having generated browser |
|
128 info like this: |
|
129 \begin{ttbox} |
|
130 isabelle usedir -i true HOL Foo |
|
131 \end{ttbox} |
|
132 |
|
133 This assumes that directory @{verbatim Foo} contains some @{verbatim |
|
134 ROOT.ML} file to load all your theories, and HOL is your parent |
|
135 logic image (@{tool_ref mkdir} assists in setting up Isabelle |
|
136 session directories. Theory browser information for HOL should have |
|
137 been generated already beforehand. Alternatively, one may specify |
|
138 an external link to an existing body of HTML data by giving @{tool |
|
139 usedir} a @{verbatim "-P"} option like this: |
|
140 \begin{ttbox} |
|
141 isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo |
|
142 \end{ttbox} |
|
143 |
|
144 \medskip For production use, @{tool usedir} is usually invoked in an |
|
145 appropriate @{verbatim IsaMakefile}, via @{tool make}. There is a |
|
146 separate @{tool mkdir} tool to provide easy setup of all this, with |
|
147 only minimal manual editing required. |
|
148 \begin{ttbox} |
|
149 isabelle mkdir HOL Foo && isabelle make |
|
150 \end{ttbox} |
|
151 See \secref{sec:tool-mkdir} for more information on preparing |
|
152 Isabelle session directories, including the setup for documents. |
|
153 *} |
|
154 |
|
155 |
|
156 section {* Creating Isabelle session directories |
|
157 \label{sec:tool-mkdir} *} |
|
158 |
|
159 text {* The @{tool_def mkdir} tool prepares Isabelle session source |
|
160 directories, including a sensible default setup of @{verbatim |
|
161 IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document} |
|
162 directory with a minimal @{verbatim root.tex} that is sufficient to |
|
163 print all theories of the session (in the order of appearance); see |
|
164 \secref{sec:tool-document} for further information on Isabelle |
|
165 document preparation. The usage of @{tool mkdir} is: |
|
166 |
|
167 \begin{ttbox} |
|
168 Usage: isabelle mkdir [OPTIONS] [LOGIC] NAME |
|
169 |
115 |
170 Options are: |
116 Options are: |
171 -I FILE alternative IsaMakefile output |
117 -d enable document preparation |
172 -P include parent logic target |
118 -n NAME alternative session name (default: DIR base name) |
173 -b setup build mode (session outputs heap image) |
119 |
174 -q quiet mode |
120 Prepare session root DIR (default: current directory). |
175 |
121 \end{ttbox} |
176 Prepare session directory, including IsaMakefile and document source, |
122 |
177 with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC) |
123 The results are placed in the given directory @{text dir}, which |
178 \end{ttbox} |
124 refers to the current directory by default. The @{tool mkroot} tool |
179 |
125 is conservative in the sense that it does not overwrite existing |
180 The @{tool mkdir} tool is conservative in the sense that any |
126 files or directories. Earlier attempts to generate a session root |
181 existing @{verbatim IsaMakefile} etc.\ is left unchanged. Thus it |
127 need to be deleted manually. |
182 is safe to invoke it multiple times, although later runs may not |
128 |
183 have the desired effect. |
129 \medskip Option @{verbatim "-d"} indicates that the session shall be |
184 |
130 accompanied by a formal document, with @{text dir}@{verbatim |
185 Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile} |
131 "/document/root.tex"} as its {\LaTeX} entry point (see also |
186 incrementally --- manual changes are required for multiple |
132 \chref{ch:present}). |
187 sub-sessions. On order to get an initial working session, the only |
133 |
188 editing needed is to add appropriate @{ML use_thy} calls to the |
134 Option @{verbatim "-n"} allows to specify an alternative session |
189 generated @{verbatim ROOT.ML} file. |
135 name; otherwise the base name of the given directory is used. |
190 *} |
136 |
191 |
137 \medskip The implicit Isabelle settings variable @{setting |
192 |
138 ISABELLE_LOGIC} specifies the parent session, and @{setting |
193 subsubsection {* Options *} |
139 ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled |
194 |
140 into the generated @{verbatim ROOT} file. *} |
195 text {* |
|
196 The @{verbatim "-I"} option specifies an alternative to @{verbatim |
|
197 IsaMakefile} for dependencies. Note that ``@{verbatim "-"}'' refers |
|
198 to \emph{stdout}, i.e.\ ``@{verbatim "-I-"}'' provides an easy way |
|
199 to peek at @{tool mkdir}'s idea of @{tool make} setup required for |
|
200 some particular of Isabelle session. |
|
201 |
|
202 \medskip The @{verbatim "-P"} option includes a target for the |
|
203 parent @{verbatim LOGIC} session in the generated @{verbatim |
|
204 IsaMakefile}. The corresponding sources are assumed to be located |
|
205 within the Isabelle distribution. |
|
206 |
|
207 \medskip The @{verbatim "-b"} option sets up the current directory |
|
208 as the base for a new session that provides an actual logic image, |
|
209 as opposed to one that only runs several theories based on an |
|
210 existing image. Note that in the latter case, everything except |
|
211 @{verbatim IsaMakefile} would be placed into a separate directory |
|
212 @{verbatim NAME}, rather than the current one. See |
|
213 \secref{sec:tool-usedir} for further information on \emph{build |
|
214 mode} vs.\ \emph{example mode} of @{tool usedir}. |
|
215 |
|
216 \medskip The @{verbatim "-q"} option enables quiet mode, suppressing |
|
217 further notes on how to proceed. |
|
218 *} |
|
219 |
141 |
220 |
142 |
221 subsubsection {* Examples *} |
143 subsubsection {* Examples *} |
222 |
144 |
223 text {* |
145 text {* Produce session @{verbatim Test} (with document preparation) |
224 The standard setup of a single ``example session'' based on the |
146 within a separate directory of the same name: |
225 default logic, with proper document generation is generated like |
147 \begin{ttbox} |
226 this: |
148 isabelle mkroot -d Test && isabelle build -D Test |
227 \begin{ttbox} |
149 \end{ttbox} |
228 isabelle mkdir Foo && isabelle make |
150 |
229 \end{ttbox} |
151 \medskip Upgrade the current directory into a session ROOT with |
230 |
152 document preparation, and build it: |
231 \noindent The theory sources should be put into the @{verbatim Foo} |
153 \begin{ttbox} |
232 directory, and its @{verbatim ROOT.ML} should be edited to load all |
154 isabelle mkroot -d && isabelle build -D . |
233 required theories. Invoking @{tool make} again would run the whole |
155 \end{ttbox} |
234 session, generating browser information and the document |
|
235 automatically. The @{verbatim IsaMakefile} is typically tuned |
|
236 manually later, e.g.\ adding source dependencies, or changing the |
|
237 options passed to @{tool usedir}. |
|
238 |
|
239 \medskip Large projects may demand further sessions, potentially |
|
240 with separate logic images being created. This usually requires |
|
241 manual editing of the generated @{verbatim IsaMakefile}, which is |
|
242 meant to cover all of the sub-session directories at the same time |
|
243 (this is the deeper reasong why @{verbatim IsaMakefile} is not made |
|
244 part of the initial session directory created by @{tool mkdir}). |
|
245 *} |
|
246 |
|
247 |
|
248 section {* Running Isabelle sessions \label{sec:tool-usedir} *} |
|
249 |
|
250 text {* The @{tool_def usedir} tool builds object-logic images, or |
|
251 runs example sessions based on existing logics. Its usage is: |
|
252 \begin{ttbox} |
|
253 Usage: isabelle usedir [OPTIONS] LOGIC NAME |
|
254 |
|
255 Options are: |
|
256 -C BOOL copy existing document directory to -D PATH (default true) |
|
257 -D PATH dump generated document sources into PATH |
|
258 -M MAX multithreading: maximum number of worker threads (default 1) |
|
259 -P PATH set path for remote theory browsing information |
|
260 -Q INT set threshold for sub-proof parallelization (default 50) |
|
261 -T LEVEL multithreading: trace level (default 0) |
|
262 -V VARIANT declare alternative document VARIANT |
|
263 -b build mode (output heap image, using current dir) |
|
264 -d FORMAT build document as FORMAT (default false) |
|
265 -f NAME use ML file NAME (default ROOT.ML) |
|
266 -g BOOL generate session graph image for document (default false) |
|
267 -i BOOL generate theory browser information (default false) |
|
268 -m MODE add print mode for output |
|
269 -p LEVEL set level of detail for proof objects (default 0) |
|
270 -q LEVEL set level of parallel proof checking (default 1) |
|
271 -r reset session path |
|
272 -s NAME override session NAME |
|
273 -t BOOL internal session timing (default false) |
|
274 -v BOOL be verbose (default false) |
|
275 |
|
276 Build object-logic or run examples. Also creates browsing |
|
277 information (HTML etc.) according to settings. |
|
278 |
|
279 ISABELLE_USEDIR_OPTIONS=... |
|
280 |
|
281 ML_PLATFORM=... |
|
282 ML_HOME=... |
|
283 ML_SYSTEM=... |
|
284 ML_OPTIONS=... |
|
285 \end{ttbox} |
|
286 |
|
287 Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS} |
|
288 setting is implicitly prefixed to \emph{any} @{tool usedir} |
|
289 call. Since the @{verbatim IsaMakefile}s of all object-logics |
|
290 distributed with Isabelle just invoke @{tool usedir} for the real |
|
291 work, one may control compilation options globally via above |
|
292 variable. In particular, generation of \rmindex{HTML} browsing |
|
293 information and document preparation is controlled here. |
|
294 *} |
|
295 |
|
296 |
|
297 subsubsection {* Options *} |
|
298 |
|
299 text {* |
|
300 Basically, there are two different modes of operation: \emph{build |
|
301 mode} (enabled through the @{verbatim "-b"} option) and |
|
302 \emph{example mode} (default). |
|
303 |
|
304 Calling @{tool usedir} with @{verbatim "-b"} runs @{executable |
|
305 "isabelle-process"} with input image @{verbatim LOGIC} and output to |
|
306 @{verbatim NAME}, as provided on the command line. This will be a |
|
307 batch session, running @{verbatim ROOT.ML} from the current |
|
308 directory and then quitting. It is assumed that @{verbatim ROOT.ML} |
|
309 contains all ML commands required to build the logic. |
|
310 |
|
311 In example mode, @{tool usedir} runs a read-only session of |
|
312 @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from |
|
313 within directory @{verbatim NAME}. It assumes that this file |
|
314 contains appropriate ML commands to run the desired examples. |
|
315 |
|
316 \medskip The @{verbatim "-i"} option controls theory browser data |
|
317 generation. It may be explicitly turned on or off --- as usual, the |
|
318 last occurrence of @{verbatim "-i"} on the command line wins. |
|
319 |
|
320 The @{verbatim "-P"} option specifies a path (or actual URL) to be |
|
321 prefixed to any \emph{non-local} reference of existing theories. |
|
322 Thus user sessions may easily link to existing Isabelle libraries |
|
323 already present on the WWW. |
|
324 |
|
325 The @{verbatim "-m"} options specifies additional print modes to be |
|
326 activated temporarily while the session is processed. |
|
327 |
|
328 \medskip The @{verbatim "-d"} option controls document preparation. |
|
329 Valid arguments are @{verbatim false} (do not prepare any document; |
|
330 this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz}, |
|
331 @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}. The logic |
|
332 session has to provide a properly setup @{verbatim document} |
|
333 directory. See \secref{sec:tool-document} and |
|
334 \secref{sec:tool-latex} for more details. |
|
335 |
|
336 \medskip The @{verbatim "-V"} option declares alternative document |
|
337 variants, consisting of name/tags pairs (cf.\ options @{verbatim |
|
338 "-n"} and @{verbatim "-t"} of @{tool_ref document}). The standard |
|
339 document is equivalent to ``@{verbatim |
|
340 "document=theory,proof,ML"}'', which means that all theory begin/end |
|
341 commands, proof body texts, and ML code will be presented |
|
342 faithfully. |
|
343 |
|
344 An alternative variant ``@{verbatim "outline=/proof/ML"}'' would |
|
345 fold proof and ML parts, replacing the original text by a short |
|
346 place-holder. The form ``@{text name}@{verbatim "=-"},'' means to |
|
347 remove document @{text name} from the list of variants to be |
|
348 processed. Any number of @{verbatim "-V"} options may be given; |
|
349 later declarations have precedence over earlier ones. |
|
350 |
|
351 Some document variant @{text name} may use an alternative {\LaTeX} |
|
352 entry point called @{verbatim "document/root_"}@{text |
|
353 "name"}@{verbatim ".tex"} if that file exists; otherwise the common |
|
354 @{verbatim "document/root.tex"} is used. |
|
355 |
|
356 \medskip The @{verbatim "-g"} option produces images of the theory |
|
357 dependency graph (cf.\ \secref{sec:browse}) for inclusion in the |
|
358 generated document, both as @{verbatim session_graph.eps} and |
|
359 @{verbatim session_graph.pdf} at the same time. To include this in |
|
360 the final {\LaTeX} document one could say @{verbatim |
|
361 "\\includegraphics{session_graph}"} in @{verbatim |
|
362 "document/root.tex"} (omitting the file-name extension enables |
|
363 {\LaTeX} to select to correct version, either for the DVI or PDF |
|
364 output path). |
|
365 |
|
366 \medskip The @{verbatim "-D"} option causes the generated document |
|
367 sources to be dumped at location @{verbatim PATH}; this path is |
|
368 relative to the session's main directory. If the @{verbatim "-C"} |
|
369 option is true, this will include a copy of an existing @{verbatim |
|
370 document} directory as provided by the user. For example, @{tool |
|
371 usedir}~@{verbatim "-D generated HOL Foo"} produces a complete set |
|
372 of document sources at @{verbatim "Foo/generated"}. Subsequent |
|
373 invocation of @{tool document}~@{verbatim "Foo/generated"} (see also |
|
374 \secref{sec:tool-document}) will process the final result |
|
375 independently of an Isabelle job. This decoupled mode of operation |
|
376 facilitates debugging of serious {\LaTeX} errors, for example. |
|
377 |
|
378 \medskip The @{verbatim "-p"} option determines the level of detail |
|
379 for internal proof objects, see also the \emph{Isabelle Reference |
|
380 Manual}~\cite{isabelle-ref}. |
|
381 |
|
382 \medskip The @{verbatim "-q"} option specifies the level of parallel |
|
383 proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel |
|
384 proofs (default), @{verbatim 2} toplevel and nested Isar proofs. |
|
385 The option @{verbatim "-Q"} specifies a threshold for @{verbatim |
|
386 "-q2"}: nested proofs are only parallelized when the current number |
|
387 of forked proofs falls below the given value (default 50), |
|
388 multiplied by the number of worker threads (see option @{verbatim |
|
389 "-M"}). |
|
390 |
|
391 \medskip The @{verbatim "-t"} option produces a more detailed |
|
392 internal timing report of the session. |
|
393 |
|
394 \medskip The @{verbatim "-v"} option causes additional information |
|
395 to be printed while running the session, notably the location of |
|
396 prepared documents. |
|
397 |
|
398 \medskip The @{verbatim "-M"} option specifies the maximum number of |
|
399 parallel worker threads used for processing independent tasks when |
|
400 checking theory sources (multithreading only works on suitable ML |
|
401 platforms). The special value of @{verbatim 0} or @{verbatim max} |
|
402 refers to the number of actual CPU cores of the underlying machine, |
|
403 which is a good starting point for optimal performance tuning. The |
|
404 @{verbatim "-T"} option determines the level of detail in tracing |
|
405 output concerning the internal locking and scheduling in |
|
406 multithreaded operation. This may be helpful in isolating |
|
407 performance bottle-necks, e.g.\ due to excessive wait states when |
|
408 locking critical code sections. |
|
409 |
|
410 \medskip Any @{tool usedir} session is named by some \emph{session |
|
411 identifier}. These accumulate, documenting the way sessions depend |
|
412 on others. For example, consider @{verbatim "Pure/FOL/ex"}, which |
|
413 refers to the examples of FOL, which in turn is built upon Pure. |
|
414 |
|
415 The current session's identifier is by default just the base name of |
|
416 the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim |
|
417 NAME} argument (in example mode). This may be overridden explicitly |
|
418 via the @{verbatim "-s"} option. |
|
419 *} |
156 *} |
420 |
157 |
421 |
158 |
422 section {* Preparing Isabelle session documents |
159 section {* Preparing Isabelle session documents |
423 \label{sec:tool-document} *} |
160 \label{sec:tool-document} *} |