1 theory Presentation |
|
2 imports Base |
|
3 begin |
|
4 |
|
5 chapter {* Presenting theories \label{ch:present} *} |
|
6 |
|
7 text {* Isabelle provides several ways to present the outcome of |
|
8 formal developments, including WWW-based browsable libraries or |
|
9 actual printable documents. Presentation is centered around the |
|
10 concept of \emph{sessions} (\chref{ch:session}). The global session |
|
11 structure is that of a tree, with Isabelle Pure at its root, further |
|
12 object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and |
|
13 application sessions further on in the hierarchy. |
|
14 |
|
15 The tools @{tool_ref mkroot} and @{tool_ref build} provide the |
|
16 primary means for managing Isabelle sessions, including proper setup |
|
17 for presentation; @{tool build} takes care to have @{executable_ref |
|
18 "isabelle-process"} run any additional stages required for document |
|
19 preparation, notably the @{tool_ref document} and @{tool_ref latex}. |
|
20 The complete tool chain for managing batch-mode Isabelle sessions is |
|
21 illustrated in \figref{fig:session-tools}. |
|
22 |
|
23 \begin{figure}[htbp] |
|
24 \begin{center} |
|
25 \begin{tabular}{lp{0.6\textwidth}} |
|
26 |
|
27 @{tool_ref mkroot} & invoked once by the user to initialize the |
|
28 session @{verbatim ROOT} with optional @{verbatim document} |
|
29 directory; \\ |
|
30 |
|
31 @{tool_ref build} & invoked repeatedly by the user to keep |
|
32 session output up-to-date (HTML, documents etc.); \\ |
|
33 |
|
34 @{executable "isabelle-process"} & run through @{tool_ref |
|
35 build}; \\ |
|
36 |
|
37 @{tool_ref document} & run by the Isabelle process if document |
|
38 preparation is enabled; \\ |
|
39 |
|
40 @{tool_ref latex} & universal {\LaTeX} tool wrapper invoked |
|
41 multiple times by @{tool_ref document}; also useful for manual |
|
42 experiments; \\ |
|
43 |
|
44 \end{tabular} |
|
45 \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools} |
|
46 \end{center} |
|
47 \end{figure} |
|
48 *} |
|
49 |
|
50 |
|
51 section {* Generating theory browser information \label{sec:info} *} |
|
52 |
|
53 text {* |
|
54 \index{theory browsing information|bold} |
|
55 |
|
56 As a side-effect of building sessions, Isabelle is able to generate |
|
57 theory browsing information, including HTML documents that show the |
|
58 theory sources and the relationship with its ancestors and |
|
59 descendants. Besides the HTML file that is generated for every |
|
60 theory, Isabelle stores links to all theories in an index |
|
61 file. These indexes are linked with other indexes to represent the |
|
62 overall tree structure of the sessions. |
|
63 |
|
64 Isabelle also generates graph files that represent the theory |
|
65 dependencies within a session. There is a graph browser Java applet |
|
66 embedded in the generated HTML pages, and also a stand-alone |
|
67 application that allows browsing theory graphs without having to |
|
68 start a WWW client first. The latter version also includes features |
|
69 such as generating Postscript files, which are not available in the |
|
70 applet version. See \secref{sec:browse} for further information. |
|
71 |
|
72 \medskip |
|
73 |
|
74 The easiest way to let Isabelle generate theory browsing information |
|
75 for existing sessions is to invoke @{tool build} with suitable |
|
76 options: |
|
77 |
|
78 \begin{ttbox} |
|
79 isabelle build -o browser_info -v -c FOL |
|
80 \end{ttbox} |
|
81 |
|
82 The presentation output will appear in @{verbatim |
|
83 "$ISABELLE_BROWSER_INFO/FOL"} as reported by the above verbose |
|
84 invocation of the build process. |
|
85 |
|
86 Many Isabelle sessions (such as @{verbatim "HOL-Library"} in @{file |
|
87 "~~/src/HOL/Library"}) also provide actual printable documents. |
|
88 These are prepared automatically as well if enabled like this: |
|
89 \begin{ttbox} |
|
90 isabelle build -o browser_info -o document=pdf -v -c HOL-Library |
|
91 \end{ttbox} |
|
92 |
|
93 Enabling both browser info and document preparation simultaneously |
|
94 causes an appropriate ``document'' link to be included in the HTML |
|
95 index. Documents may be generated independently of browser |
|
96 information as well, see \secref{sec:tool-document} for further |
|
97 details. |
|
98 |
|
99 \bigskip The theory browsing information is stored in a |
|
100 sub-directory directory determined by the @{setting_ref |
|
101 ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the |
|
102 session identifier (according to the tree structure of sub-sessions |
|
103 by default). In order to present Isabelle applications on the web, |
|
104 the corresponding subdirectory from @{setting ISABELLE_BROWSER_INFO} |
|
105 can be put on a WWW server. |
|
106 *} |
|
107 |
|
108 section {* Preparing session root directories \label{sec:tool-mkroot} *} |
|
109 |
|
110 text {* The @{tool_def mkroot} tool configures a given directory as |
|
111 session root, with some @{verbatim ROOT} file and optional document |
|
112 source directory. Its usage is: |
|
113 \begin{ttbox} |
|
114 Usage: isabelle mkroot [OPTIONS] [DIR] |
|
115 |
|
116 Options are: |
|
117 -d enable document preparation |
|
118 -n NAME alternative session name (default: DIR base name) |
|
119 |
|
120 Prepare session root DIR (default: current directory). |
|
121 \end{ttbox} |
|
122 |
|
123 The results are placed in the given directory @{text dir}, which |
|
124 refers to the current directory by default. The @{tool mkroot} tool |
|
125 is conservative in the sense that it does not overwrite existing |
|
126 files or directories. Earlier attempts to generate a session root |
|
127 need to be deleted manually. |
|
128 |
|
129 \medskip Option @{verbatim "-d"} indicates that the session shall be |
|
130 accompanied by a formal document, with @{text dir}@{verbatim |
|
131 "/document/root.tex"} as its {\LaTeX} entry point (see also |
|
132 \chref{ch:present}). |
|
133 |
|
134 Option @{verbatim "-n"} allows to specify an alternative session |
|
135 name; otherwise the base name of the given directory is used. |
|
136 |
|
137 \medskip The implicit Isabelle settings variable @{setting |
|
138 ISABELLE_LOGIC} specifies the parent session, and @{setting |
|
139 ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled |
|
140 into the generated @{verbatim ROOT} file. *} |
|
141 |
|
142 |
|
143 subsubsection {* Examples *} |
|
144 |
|
145 text {* Produce session @{verbatim Test} (with document preparation) |
|
146 within a separate directory of the same name: |
|
147 \begin{ttbox} |
|
148 isabelle mkroot -d Test && isabelle build -D Test |
|
149 \end{ttbox} |
|
150 |
|
151 \medskip Upgrade the current directory into a session ROOT with |
|
152 document preparation, and build it: |
|
153 \begin{ttbox} |
|
154 isabelle mkroot -d && isabelle build -D . |
|
155 \end{ttbox} |
|
156 *} |
|
157 |
|
158 |
|
159 section {* Preparing Isabelle session documents |
|
160 \label{sec:tool-document} *} |
|
161 |
|
162 text {* The @{tool_def document} tool prepares logic session |
|
163 documents, processing the sources both as provided by the user and |
|
164 generated by Isabelle. Its usage is: |
|
165 \begin{ttbox} |
|
166 Usage: isabelle document [OPTIONS] [DIR] |
|
167 |
|
168 Options are: |
|
169 -c cleanup -- be aggressive in removing old stuff |
|
170 -n NAME specify document name (default 'document') |
|
171 -o FORMAT specify output format: dvi (default), dvi.gz, ps, |
|
172 ps.gz, pdf |
|
173 -t TAGS specify tagged region markup |
|
174 |
|
175 Prepare the theory session document in DIR (default 'document') |
|
176 producing the specified output format. |
|
177 \end{ttbox} |
|
178 This tool is usually run automatically as part of the Isabelle build |
|
179 process, provided document preparation has been enabled via suitable |
|
180 options. It may be manually invoked on the generated browser |
|
181 information document output as well, e.g.\ in case of errors |
|
182 encountered in the batch run. |
|
183 |
|
184 \medskip The @{verbatim "-c"} option tells @{tool document} to |
|
185 dispose the document sources after successful operation! This is |
|
186 the right thing to do for sources generated by an Isabelle process, |
|
187 but take care of your files in manual document preparation! |
|
188 |
|
189 \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify |
|
190 the final output file name and format, the default is ``@{verbatim |
|
191 document.dvi}''. Note that the result will appear in the parent of |
|
192 the target @{verbatim DIR}. |
|
193 |
|
194 \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret |
|
195 tagged Isabelle command regions. Tags are specified as a comma |
|
196 separated list of modifier/name pairs: ``@{verbatim "+"}@{text |
|
197 foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim |
|
198 "-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to |
|
199 fold text tagged as @{text foo}. The builtin default is equivalent |
|
200 to the tag specification ``@{verbatim |
|
201 "+theory,+proof,+ML,+visible,-invisible"}''; see also the {\LaTeX} |
|
202 macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and |
|
203 @{verbatim "\\isafoldtag"}, in @{file |
|
204 "~~/lib/texinputs/isabelle.sty"}. |
|
205 |
|
206 \medskip Document preparation requires a @{verbatim document} |
|
207 directory within the session sources. This directory is supposed to |
|
208 contain all the files needed to produce the final document --- apart |
|
209 from the actual theories which are generated by Isabelle. |
|
210 |
|
211 \medskip For most practical purposes, @{tool document} is smart |
|
212 enough to create any of the specified output formats, taking |
|
213 @{verbatim root.tex} supplied by the user as a starting point. This |
|
214 even includes multiple runs of {\LaTeX} to accommodate references |
|
215 and bibliographies (the latter assumes @{verbatim root.bib} within |
|
216 the same directory). |
|
217 |
|
218 In more complex situations, a separate @{verbatim build} script for |
|
219 the document sources may be given. It is invoked with command-line |
|
220 arguments for the document format and the document variant name. |
|
221 The script needs to produce corresponding output files, e.g.\ |
|
222 @{verbatim root.pdf} for target format @{verbatim pdf} (and default |
|
223 default variants). The main work can be again delegated to @{tool |
|
224 latex}, but it is also possible to harvest generated {\LaTeX} |
|
225 sources and copy them elsewhere, for example. |
|
226 |
|
227 \medskip When running the session, Isabelle copies the content of |
|
228 the original @{verbatim document} directory into its proper place |
|
229 within @{setting ISABELLE_BROWSER_INFO}, according to the session |
|
230 path and document variant. Then, for any processed theory @{text A} |
|
231 some {\LaTeX} source is generated and put there as @{text |
|
232 A}@{verbatim ".tex"}. Furthermore, a list of all generated theory |
|
233 files is put into @{verbatim session.tex}. Typically, the root |
|
234 {\LaTeX} file provided by the user would include @{verbatim |
|
235 session.tex} to get a document containing all the theories. |
|
236 |
|
237 The {\LaTeX} versions of the theories require some macros defined in |
|
238 @{file "~~/lib/texinputs/isabelle.sty"}. Doing @{verbatim |
|
239 "\\usepackage{isabelle}"} in @{verbatim root.tex} should be fine; |
|
240 the underlying @{tool latex} already includes an appropriate path |
|
241 specification for {\TeX} inputs. |
|
242 |
|
243 If the text contains any references to Isabelle symbols (such as |
|
244 @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim |
|
245 "isabellesym.sty"} should be included as well. This package |
|
246 contains a standard set of {\LaTeX} macro definitions @{verbatim |
|
247 "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim |
|
248 "<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a |
|
249 complete list of predefined Isabelle symbols. Users may invent |
|
250 further symbols as well, just by providing {\LaTeX} macros in a |
|
251 similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of |
|
252 the distribution. |
|
253 |
|
254 For proper setup of DVI and PDF documents (with hyperlinks and |
|
255 bookmarks), we recommend to include @{file |
|
256 "~~/lib/texinputs/pdfsetup.sty"} as well. |
|
257 |
|
258 \medskip As a final step of Isabelle document preparation, @{tool |
|
259 document}~@{verbatim "-c"} is run on the resulting copy of the |
|
260 @{verbatim document} directory. Thus the actual output document is |
|
261 built and installed in its proper place. The generated sources are |
|
262 deleted after successful run of {\LaTeX} and friends. |
|
263 |
|
264 Some care is needed if the document output location is configured |
|
265 differently, say within a directory whose content is still required |
|
266 afterwards! |
|
267 *} |
|
268 |
|
269 |
|
270 section {* Running {\LaTeX} within the Isabelle environment |
|
271 \label{sec:tool-latex} *} |
|
272 |
|
273 text {* The @{tool_def latex} tool provides the basic interface for |
|
274 Isabelle document preparation. Its usage is: |
|
275 \begin{ttbox} |
|
276 Usage: isabelle latex [OPTIONS] [FILE] |
|
277 |
|
278 Options are: |
|
279 -o FORMAT specify output format: dvi (default), dvi.gz, ps, |
|
280 ps.gz, pdf, bbl, idx, sty, syms |
|
281 |
|
282 Run LaTeX (and related tools) on FILE (default root.tex), |
|
283 producing the specified output format. |
|
284 \end{ttbox} |
|
285 |
|
286 Appropriate {\LaTeX}-related programs are run on the input file, |
|
287 according to the given output format: @{executable latex}, |
|
288 @{executable pdflatex}, @{executable dvips}, @{executable bibtex} |
|
289 (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim |
|
290 idx}). The actual commands are determined from the settings |
|
291 environment (@{setting ISABELLE_LATEX} etc.). |
|
292 |
|
293 The @{verbatim sty} output format causes the Isabelle style files to |
|
294 be updated from the distribution. This is useful in special |
|
295 situations where the document sources are to be processed another |
|
296 time by separate tools. |
|
297 |
|
298 The @{verbatim syms} output is for internal use; it generates lists |
|
299 of symbols that are available without loading additional {\LaTeX} |
|
300 packages. |
|
301 *} |
|
302 |
|
303 |
|
304 subsubsection {* Examples *} |
|
305 |
|
306 text {* Invoking @{tool latex} by hand may be occasionally useful when |
|
307 debugging failed attempts of the automatic document preparation |
|
308 stage of batch-mode Isabelle. The abortive process leaves the |
|
309 sources at a certain place within @{setting ISABELLE_BROWSER_INFO}, |
|
310 see the runtime error message for details. This enables users to |
|
311 inspect {\LaTeX} runs in further detail, e.g.\ like this: |
|
312 |
|
313 \begin{ttbox} |
|
314 cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document |
|
315 isabelle latex -o pdf |
|
316 \end{ttbox} |
|
317 *} |
|
318 |
|
319 end |
|