author | wenzelm |
Mon, 30 Jul 2012 14:11:29 +0200 | |
changeset 48602 | 342ca8f3197b |
parent 48590 | 80ba76b46247 |
child 48616 | be8002ee43d8 |
permissions | -rw-r--r-- |
28221 | 1 |
theory Presentation |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42009
diff
changeset
|
2 |
imports Base |
28221 | 3 |
begin |
4 |
||
5 |
chapter {* Presenting theories \label{ch:present} *} |
|
6 |
||
7 |
text {* |
|
8 |
Isabelle provides several ways to present the outcome of formal |
|
9 |
developments, including WWW-based browsable libraries or actual |
|
10 |
printable documents. Presentation is centered around the concept of |
|
11 |
\emph{logic sessions}. The global session structure is that of a |
|
12 |
tree, with Isabelle Pure at its root, further object-logics derived |
|
13 |
(e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions |
|
14 |
in leaf positions (usually without a separate image). |
|
15 |
||
48602 | 16 |
The tools @{tool_ref mkdir} and @{tool_ref make} provide the primary |
17 |
means for managing Isabelle sessions, including proper setup for |
|
18 |
presentation. Here @{tool_ref usedir} takes care to let |
|
19 |
@{executable_ref "isabelle-process"} process run any additional |
|
20 |
stages required for document preparation, notably the tools |
|
21 |
@{tool_ref document} and @{tool_ref latex}. The complete tool chain |
|
22 |
for managing batch-mode Isabelle sessions is illustrated in |
|
28221 | 23 |
\figref{fig:session-tools}. |
24 |
||
25 |
\begin{figure}[htbp] |
|
26 |
\begin{center} |
|
27 |
\begin{tabular}{lp{0.6\textwidth}} |
|
28 |
||
48602 | 29 |
@{tool_ref mkdir} & invoked once by the user to create the |
30 |
initial source setup (common @{verbatim IsaMakefile} plus a |
|
31 |
single session directory); \\ |
|
28221 | 32 |
|
48602 | 33 |
@{tool make} & invoked repeatedly by the user to keep session |
34 |
output up-to-date (HTML, documents etc.); \\ |
|
28238 | 35 |
|
48602 | 36 |
@{tool usedir} & part of the standard @{verbatim IsaMakefile} |
37 |
entry of a session; \\ |
|
28221 | 38 |
|
48602 | 39 |
@{executable "isabelle-process"} & run through @{tool_ref |
40 |
usedir}; \\ |
|
28221 | 41 |
|
48602 | 42 |
@{tool_ref document} & run by the Isabelle process if document |
43 |
preparation is enabled; \\ |
|
28221 | 44 |
|
48602 | 45 |
@{tool_ref latex} & universal {\LaTeX} tool wrapper invoked |
46 |
multiple times by @{tool_ref document}; also useful for manual |
|
47 |
experiments; \\ |
|
28221 | 48 |
|
49 |
\end{tabular} |
|
50 |
\caption{The tool chain of Isabelle session presentation} \label{fig:session-tools} |
|
51 |
\end{center} |
|
52 |
\end{figure} |
|
53 |
*} |
|
54 |
||
55 |
||
56 |
section {* Generating theory browser information \label{sec:info} *} |
|
57 |
||
58 |
text {* |
|
59 |
\index{theory browsing information|bold} |
|
60 |
||
61 |
As a side-effect of running a logic sessions, Isabelle is able to |
|
62 |
generate theory browsing information, including HTML documents that |
|
63 |
show a theory's definition, the theorems proved in its ML file and |
|
64 |
the relationship with its ancestors and descendants. Besides the |
|
65 |
HTML file that is generated for every theory, Isabelle stores links |
|
66 |
to all theories in an index file. These indexes are linked with |
|
67 |
other indexes to represent the overall tree structure of logic |
|
68 |
sessions. |
|
69 |
||
70 |
Isabelle also generates graph files that represent the theory |
|
71 |
hierarchy of a logic. There is a graph browser Java applet embedded |
|
72 |
in the generated HTML pages, and also a stand-alone application that |
|
73 |
allows browsing theory graphs without having to start a WWW client |
|
74 |
first. The latter version also includes features such as generating |
|
75 |
Postscript files, which are not available in the applet version. |
|
76 |
See \secref{sec:browse} for further information. |
|
77 |
||
78 |
\medskip |
|
79 |
||
80 |
The easiest way to let Isabelle generate theory browsing information |
|
81 |
for existing sessions is to append ``@{verbatim "-i true"}'' to the |
|
48602 | 82 |
@{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{tool make}. |
83 |
For example, add something like this to your Isabelle settings file |
|
28221 | 84 |
|
85 |
\begin{ttbox} |
|
86 |
ISABELLE_USEDIR_OPTIONS="-i true" |
|
87 |
\end{ttbox} |
|
88 |
||
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40387
diff
changeset
|
89 |
and then change into the @{file "~~/src/FOL"} directory and run |
48602 | 90 |
@{tool make}, or even @{tool make}~@{verbatim all}. The |
91 |
presentation output will appear in @{verbatim |
|
92 |
"ISABELLE_BROWSER_INFO/FOL"}, which usually refers to something like |
|
93 |
@{verbatim "~/.isabelle/IsabelleXXXX/browser_info/FOL"}. Note that |
|
94 |
option @{verbatim "-v true"} will make the internal runs of @{tool |
|
95 |
usedir} more explicit about such details. |
|
28221 | 96 |
|
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40387
diff
changeset
|
97 |
Many standard Isabelle sessions (such as @{file "~~/src/HOL/ex"}) |
28238 | 98 |
also provide actual printable documents. These are prepared |
28221 | 99 |
automatically as well if enabled like this, using the @{verbatim |
100 |
"-d"} option |
|
101 |
\begin{ttbox} |
|
102 |
ISABELLE_USEDIR_OPTIONS="-i true -d dvi" |
|
103 |
\end{ttbox} |
|
104 |
Enabling options @{verbatim "-i"} and @{verbatim "-d"} |
|
28225 | 105 |
simultaneously as shown above causes an appropriate ``document'' |
28221 | 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 |
||
110 |
\bigskip The theory browsing information is stored in a |
|
111 |
sub-directory directory determined by the @{setting_ref |
|
112 |
ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the |
|
113 |
session identifier (according to the tree structure of sub-sessions |
|
114 |
by default). A complete WWW view of all standard object-logics and |
|
28225 | 115 |
examples of the Isabelle distribution is available at the usual |
116 |
Isabelle sites: |
|
28221 | 117 |
\begin{center}\small |
118 |
\begin{tabular}{l} |
|
28225 | 119 |
\url{http://isabelle.in.tum.de/dist/library/} \\ |
120 |
\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/} \\ |
|
121 |
\url{http://mirror.cse.unsw.edu.au/pub/isabelle/dist/library/} \\ |
|
28221 | 122 |
\end{tabular} |
123 |
\end{center} |
|
124 |
||
125 |
\medskip In order to present your own theories on the web, simply |
|
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} |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28238
diff
changeset
|
130 |
isabelle usedir -i true HOL Foo |
28221 | 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 |
|
48602 | 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: |
|
28221 | 140 |
\begin{ttbox} |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28238
diff
changeset
|
141 |
isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo |
28221 | 142 |
\end{ttbox} |
143 |
||
48602 | 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. |
|
28221 | 148 |
\begin{ttbox} |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28238
diff
changeset
|
149 |
isabelle mkdir HOL Foo && isabelle make |
28221 | 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 |
||
48602 | 159 |
text {* The @{tool_def mkdir} tool prepares Isabelle session source |
28221 | 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 |
|
48602 | 165 |
document preparation. The usage of @{tool mkdir} is: |
28221 | 166 |
|
167 |
\begin{ttbox} |
|
48602 | 168 |
Usage: isabelle mkdir [OPTIONS] [LOGIC] NAME |
28221 | 169 |
|
170 |
Options are: |
|
171 |
-I FILE alternative IsaMakefile output |
|
172 |
-P include parent logic target |
|
173 |
-b setup build mode (session outputs heap image) |
|
174 |
-q quiet mode |
|
175 |
||
176 |
Prepare session directory, including IsaMakefile and document source, |
|
177 |
with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC) |
|
178 |
\end{ttbox} |
|
179 |
||
180 |
The @{tool mkdir} tool is conservative in the sense that any |
|
181 |
existing @{verbatim IsaMakefile} etc.\ is left unchanged. Thus it |
|
182 |
is safe to invoke it multiple times, although later runs may not |
|
183 |
have the desired effect. |
|
184 |
||
185 |
Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile} |
|
186 |
incrementally --- manual changes are required for multiple |
|
187 |
sub-sessions. On order to get an initial working session, the only |
|
188 |
editing needed is to add appropriate @{ML use_thy} calls to the |
|
189 |
generated @{verbatim ROOT.ML} file. |
|
190 |
*} |
|
191 |
||
192 |
||
193 |
subsubsection {* Options *} |
|
194 |
||
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 |
|
48602 | 214 |
mode} vs.\ \emph{example mode} of @{tool usedir}. |
28221 | 215 |
|
216 |
\medskip The @{verbatim "-q"} option enables quiet mode, suppressing |
|
217 |
further notes on how to proceed. |
|
218 |
*} |
|
219 |
||
220 |
||
221 |
subsubsection {* Examples *} |
|
222 |
||
223 |
text {* |
|
224 |
The standard setup of a single ``example session'' based on the |
|
225 |
default logic, with proper document generation is generated like |
|
226 |
this: |
|
227 |
\begin{ttbox} |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28238
diff
changeset
|
228 |
isabelle mkdir Foo && isabelle make |
28221 | 229 |
\end{ttbox} |
230 |
||
231 |
\noindent The theory sources should be put into the @{verbatim Foo} |
|
232 |
directory, and its @{verbatim ROOT.ML} should be edited to load all |
|
48602 | 233 |
required theories. Invoking @{tool make} again would run the whole |
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}. |
|
28221 | 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 |
|
48602 | 244 |
part of the initial session directory created by @{tool mkdir}). |
245 |
See @{file "~~/src/HOL/IsaMakefile"} for a full-blown example. *} |
|
28221 | 246 |
|
247 |
||
248 |
section {* Running Isabelle sessions \label{sec:tool-usedir} *} |
|
249 |
||
48602 | 250 |
text {* The @{tool_def usedir} tool builds object-logic images, or |
251 |
runs example sessions based on existing logics. Its usage is: |
|
28221 | 252 |
\begin{ttbox} |
48602 | 253 |
Usage: isabelle usedir [OPTIONS] LOGIC NAME |
28221 | 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 |
|
41819
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
260 |
-Q INT set threshold for sub-proof parallelization (default 50) |
28221 | 261 |
-T LEVEL multithreading: trace level (default 0) |
42004 | 262 |
-V VARIANT declare alternative document VARIANT |
28221 | 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 |
|
32061
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset
|
269 |
-p LEVEL set level of detail for proof objects (default 0) |
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset
|
270 |
-q LEVEL set level of parallel proof checking (default 1) |
28221 | 271 |
-r reset session path |
272 |
-s NAME override session NAME |
|
31688 | 273 |
-t BOOL internal session timing (default false) |
28221 | 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 |
||
47978 | 279 |
ISABELLE_USEDIR_OPTIONS=... |
29435
a5f84ac14609
added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
wenzelm
parents:
28914
diff
changeset
|
280 |
|
47978 | 281 |
ML_PLATFORM=... |
282 |
ML_HOME=... |
|
283 |
ML_SYSTEM=... |
|
284 |
ML_OPTIONS=... |
|
28221 | 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 |
|
28238 | 290 |
distributed with Isabelle just invoke @{tool usedir} for the real |
28221 | 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 |
||
28238 | 311 |
In example mode, @{tool usedir} runs a read-only session of |
28221 | 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 |
|
42004 | 337 |
variants, consisting of name/tags pairs (cf.\ options @{verbatim |
48602 | 338 |
"-n"} and @{verbatim "-t"} of @{tool_ref document}). The standard |
339 |
document is equivalent to ``@{verbatim |
|
28221 | 340 |
"document=theory,proof,ML"}'', which means that all theory begin/end |
341 |
commands, proof body texts, and ML code will be presented |
|
42004 | 342 |
faithfully. An alternative variant ``@{verbatim |
28221 | 343 |
"outline=/proof/ML"}'' would fold proof and ML parts, replacing the |
344 |
original text by a short place-holder. The form ``@{text |
|
345 |
name}@{verbatim "=-"},'' means to remove document @{text name} from |
|
42004 | 346 |
the list of variants to be processed. Any number of @{verbatim |
28221 | 347 |
"-V"} options may be given; later declarations have precedence over |
348 |
earlier ones. |
|
349 |
||
350 |
\medskip The @{verbatim "-g"} option produces images of the theory |
|
351 |
dependency graph (cf.\ \secref{sec:browse}) for inclusion in the |
|
352 |
generated document, both as @{verbatim session_graph.eps} and |
|
353 |
@{verbatim session_graph.pdf} at the same time. To include this in |
|
354 |
the final {\LaTeX} document one could say @{verbatim |
|
355 |
"\\includegraphics{session_graph}"} in @{verbatim |
|
356 |
"document/root.tex"} (omitting the file-name extension enables |
|
357 |
{\LaTeX} to select to correct version, either for the DVI or PDF |
|
358 |
output path). |
|
359 |
||
360 |
\medskip The @{verbatim "-D"} option causes the generated document |
|
361 |
sources to be dumped at location @{verbatim PATH}; this path is |
|
362 |
relative to the session's main directory. If the @{verbatim "-C"} |
|
363 |
option is true, this will include a copy of an existing @{verbatim |
|
48602 | 364 |
document} directory as provided by the user. For example, @{tool |
365 |
usedir}~@{verbatim "-D generated HOL Foo"} produces a complete set |
|
366 |
of document sources at @{verbatim "Foo/generated"}. Subsequent |
|
367 |
invocation of @{tool document}~@{verbatim "Foo/generated"} (see also |
|
28238 | 368 |
\secref{sec:tool-document}) will process the final result |
369 |
independently of an Isabelle job. This decoupled mode of operation |
|
370 |
facilitates debugging of serious {\LaTeX} errors, for example. |
|
28221 | 371 |
|
372 |
\medskip The @{verbatim "-p"} option determines the level of detail |
|
373 |
for internal proof objects, see also the \emph{Isabelle Reference |
|
374 |
Manual}~\cite{isabelle-ref}. |
|
375 |
||
32061
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset
|
376 |
\medskip The @{verbatim "-q"} option specifies the level of parallel |
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset
|
377 |
proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel |
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset
|
378 |
proofs (default), @{verbatim 2} toplevel and nested Isar proofs. |
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
40800
diff
changeset
|
379 |
The option @{verbatim "-Q"} specifies a threshold for @{verbatim |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
40800
diff
changeset
|
380 |
"-q2"}: nested proofs are only parallelized when the current number |
41819
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
381 |
of forked proofs falls below the given value (default 50), |
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
382 |
multiplied by the number of worker threads (see option @{verbatim |
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
383 |
"-M"}). |
32061
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31688
diff
changeset
|
384 |
|
31688 | 385 |
\medskip The @{verbatim "-t"} option produces a more detailed |
386 |
internal timing report of the session. |
|
387 |
||
28221 | 388 |
\medskip The @{verbatim "-v"} option causes additional information |
389 |
to be printed while running the session, notably the location of |
|
390 |
prepared documents. |
|
391 |
||
392 |
\medskip The @{verbatim "-M"} option specifies the maximum number of |
|
41819
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
393 |
parallel worker threads used for processing independent tasks when |
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
394 |
checking theory sources (multithreading only works on suitable ML |
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
395 |
platforms). The special value of @{verbatim 0} or @{verbatim max} |
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
396 |
refers to the number of actual CPU cores of the underlying machine, |
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
397 |
which is a good starting point for optimal performance tuning. The |
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
398 |
@{verbatim "-T"} option determines the level of detail in tracing |
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
399 |
output concerning the internal locking and scheduling in |
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
400 |
multithreaded operation. This may be helpful in isolating |
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
401 |
performance bottle-necks, e.g.\ due to excessive wait states when |
2d84831dc1a0
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
wenzelm
parents:
41703
diff
changeset
|
402 |
locking critical code sections. |
28221 | 403 |
|
404 |
\medskip Any @{tool usedir} session is named by some \emph{session |
|
405 |
identifier}. These accumulate, documenting the way sessions depend |
|
406 |
on others. For example, consider @{verbatim "Pure/FOL/ex"}, which |
|
407 |
refers to the examples of FOL, which in turn is built upon Pure. |
|
408 |
||
409 |
The current session's identifier is by default just the base name of |
|
410 |
the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim |
|
411 |
NAME} argument (in example mode). This may be overridden explicitly |
|
412 |
via the @{verbatim "-s"} option. |
|
413 |
*} |
|
414 |
||
415 |
||
416 |
subsubsection {* Examples *} |
|
417 |
||
48602 | 418 |
text {* Refer to the @{verbatim IsaMakefile}s of the Isabelle |
419 |
distribution's object-logics as a model for your own developments. |
|
420 |
For example, see @{file "~~/src/FOL/IsaMakefile"}. The @{tool_ref |
|
28221 | 421 |
mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation |
48602 | 422 |
of @{tool usedir} as well. *} |
28221 | 423 |
|
424 |
||
425 |
section {* Preparing Isabelle session documents |
|
426 |
\label{sec:tool-document} *} |
|
427 |
||
48602 | 428 |
text {* The @{tool_def document} tool prepares logic session |
429 |
documents, processing the sources both as provided by the user and |
|
430 |
generated by Isabelle. Its usage is: |
|
28221 | 431 |
\begin{ttbox} |
48602 | 432 |
Usage: isabelle document [OPTIONS] [DIR] |
28221 | 433 |
|
434 |
Options are: |
|
435 |
-c cleanup -- be aggressive in removing old stuff |
|
436 |
-n NAME specify document name (default 'document') |
|
437 |
-o FORMAT specify output format: dvi (default), dvi.gz, ps, |
|
438 |
ps.gz, pdf |
|
439 |
-t TAGS specify tagged region markup |
|
440 |
||
441 |
Prepare the theory session document in DIR (default 'document') |
|
442 |
producing the specified output format. |
|
443 |
\end{ttbox} |
|
444 |
This tool is usually run automatically as part of the corresponding |
|
445 |
Isabelle batch process, provided document preparation has been |
|
48602 | 446 |
enabled (cf.\ the @{verbatim "-d"} option of @{tool_ref usedir}). |
447 |
It may be manually invoked on the generated browser information |
|
448 |
document output as well, e.g.\ in case of errors encountered in the |
|
449 |
batch run. |
|
28221 | 450 |
|
48602 | 451 |
\medskip The @{verbatim "-c"} option tells @{tool document} to |
452 |
dispose the document sources after successful operation. This is |
|
28221 | 453 |
the right thing to do for sources generated by an Isabelle process, |
454 |
but take care of your files in manual document preparation! |
|
455 |
||
456 |
\medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify |
|
457 |
the final output file name and format, the default is ``@{verbatim |
|
458 |
document.dvi}''. Note that the result will appear in the parent of |
|
459 |
the target @{verbatim DIR}. |
|
460 |
||
461 |
\medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret |
|
462 |
tagged Isabelle command regions. Tags are specified as a comma |
|
463 |
separated list of modifier/name pairs: ``@{verbatim "+"}@{text |
|
464 |
foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim |
|
465 |
"-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to |
|
466 |
fold text tagged as @{text foo}. The builtin default is equivalent |
|
467 |
to the tag specification ``@{verbatim |
|
30113
5ea17e90b08a
isabelle document: adapted (postulated) defaults for tags to actual isabelle.sty;
wenzelm
parents:
29435
diff
changeset
|
468 |
"+theory,+proof,+ML,+visible,-invisible"}''; see also the {\LaTeX} |
28221 | 469 |
macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and |
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40387
diff
changeset
|
470 |
@{verbatim "\\isafoldtag"}, in @{file |
28238 | 471 |
"~~/lib/texinputs/isabelle.sty"}. |
28221 | 472 |
|
473 |
\medskip Document preparation requires a properly setup ``@{verbatim |
|
474 |
document}'' directory within the logic session sources. This |
|
475 |
directory is supposed to contain all the files needed to produce the |
|
476 |
final document --- apart from the actual theories which are |
|
477 |
generated by Isabelle. |
|
478 |
||
48602 | 479 |
\medskip For most practical purposes, @{tool document} is smart |
480 |
enough to create any of the specified output formats, taking |
|
28221 | 481 |
@{verbatim root.tex} supplied by the user as a starting point. This |
482 |
even includes multiple runs of {\LaTeX} to accommodate references |
|
483 |
and bibliographies (the latter assumes @{verbatim root.bib} within |
|
484 |
the same directory). |
|
485 |
||
486 |
In more complex situations, a separate @{verbatim IsaMakefile} for |
|
487 |
the document sources may be given instead. This should provide |
|
488 |
targets for any admissible document format; these have to produce |
|
489 |
corresponding output files named after @{verbatim root} as well, |
|
490 |
e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}. |
|
491 |
||
42009
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
492 |
\medskip When running the session, Isabelle copies the content of |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
493 |
the original @{verbatim document} directory into its proper place |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
494 |
within @{setting ISABELLE_BROWSER_INFO}, according to the session |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
495 |
path and document variant. Then, for any processed theory @{text A} |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
496 |
some {\LaTeX} source is generated and put there as @{text |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
497 |
A}@{verbatim ".tex"}. Furthermore, a list of all generated theory |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
498 |
files is put into @{verbatim session.tex}. Typically, the root |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
499 |
{\LaTeX} file provided by the user would include @{verbatim |
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42004
diff
changeset
|
500 |
session.tex} to get a document containing all the theories. |
28221 | 501 |
|
502 |
The {\LaTeX} versions of the theories require some macros defined in |
|
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40387
diff
changeset
|
503 |
@{file "~~/lib/texinputs/isabelle.sty"}. Doing @{verbatim |
28238 | 504 |
"\\usepackage{isabelle}"} in @{verbatim root.tex} should be fine; |
48602 | 505 |
the underlying @{tool latex} already includes an appropriate path |
506 |
specification for {\TeX} inputs. |
|
28221 | 507 |
|
508 |
If the text contains any references to Isabelle symbols (such as |
|
509 |
@{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim |
|
28238 | 510 |
"isabellesym.sty"} should be included as well. This package |
511 |
contains a standard set of {\LaTeX} macro definitions @{verbatim |
|
28221 | 512 |
"\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28504
diff
changeset
|
513 |
"<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28504
diff
changeset
|
514 |
complete list of predefined Isabelle symbols. Users may invent |
28221 | 515 |
further symbols as well, just by providing {\LaTeX} macros in a |
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40387
diff
changeset
|
516 |
similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of |
28238 | 517 |
the distribution. |
28221 | 518 |
|
519 |
For proper setup of DVI and PDF documents (with hyperlinks and |
|
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40387
diff
changeset
|
520 |
bookmarks), we recommend to include @{file |
28238 | 521 |
"~~/lib/texinputs/pdfsetup.sty"} as well. |
28221 | 522 |
|
523 |
\medskip As a final step of document preparation within Isabelle, |
|
48602 | 524 |
@{tool document}~@{verbatim "-c"} is run on the resulting @{verbatim |
525 |
document} directory. Thus the actual output document is built and |
|
526 |
installed in its proper place (as linked by the session's @{verbatim |
|
527 |
index.html} if option @{verbatim "-i"} of @{tool_ref usedir} has |
|
528 |
been enabled, cf.\ \secref{sec:info}). The generated sources are |
|
529 |
deleted after successful run of {\LaTeX} and friends. Note that a |
|
530 |
separate copy of the sources may be retained by passing an option |
|
531 |
@{verbatim "-D"} to @{tool usedir} when running the session. *} |
|
28221 | 532 |
|
533 |
||
534 |
section {* Running {\LaTeX} within the Isabelle environment |
|
535 |
\label{sec:tool-latex} *} |
|
536 |
||
48602 | 537 |
text {* The @{tool_def latex} tool provides the basic interface for |
28221 | 538 |
Isabelle document preparation. Its usage is: |
539 |
\begin{ttbox} |
|
48602 | 540 |
Usage: isabelle latex [OPTIONS] [FILE] |
28221 | 541 |
|
542 |
Options are: |
|
543 |
-o FORMAT specify output format: dvi (default), dvi.gz, ps, |
|
544 |
ps.gz, pdf, bbl, idx, sty, syms |
|
545 |
||
546 |
Run LaTeX (and related tools) on FILE (default root.tex), |
|
547 |
producing the specified output format. |
|
548 |
\end{ttbox} |
|
549 |
||
550 |
Appropriate {\LaTeX}-related programs are run on the input file, |
|
551 |
according to the given output format: @{executable latex}, |
|
552 |
@{executable pdflatex}, @{executable dvips}, @{executable bibtex} |
|
553 |
(for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim |
|
554 |
idx}). The actual commands are determined from the settings |
|
555 |
environment (@{setting ISABELLE_LATEX} etc.). |
|
556 |
||
557 |
The @{verbatim sty} output format causes the Isabelle style files to |
|
558 |
be updated from the distribution. This is useful in special |
|
559 |
situations where the document sources are to be processed another |
|
48602 | 560 |
time by separate tools (cf.\ option @{verbatim "-D"} of @{tool |
561 |
usedir}). |
|
28221 | 562 |
|
563 |
The @{verbatim syms} output is for internal use; it generates lists |
|
564 |
of symbols that are available without loading additional {\LaTeX} |
|
565 |
packages. |
|
566 |
*} |
|
567 |
||
568 |
||
569 |
subsubsection {* Examples *} |
|
570 |
||
48602 | 571 |
text {* Invoking @{tool latex} by hand may be occasionally useful when |
572 |
debugging failed attempts of the automatic document preparation |
|
573 |
stage of batch-mode Isabelle. The abortive process leaves the |
|
574 |
sources at a certain place within @{setting ISABELLE_BROWSER_INFO}, |
|
575 |
see the runtime error message for details. This enables users to |
|
576 |
inspect {\LaTeX} runs in further detail, e.g.\ like this: |
|
577 |
||
28221 | 578 |
\begin{ttbox} |
40387
e4c9e0dad473
moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
wenzelm
parents:
35587
diff
changeset
|
579 |
cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28238
diff
changeset
|
580 |
isabelle latex -o pdf |
28221 | 581 |
\end{ttbox} |
582 |
*} |
|
583 |
||
584 |
end |