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