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