1.1 --- a/doc-src/System/IsaMakefile Mon Sep 15 17:32:12 2008 +0200
1.2 +++ b/doc-src/System/IsaMakefile Mon Sep 15 19:42:22 2008 +0200
1.3 @@ -22,7 +22,7 @@
1.4 Pure-System: $(LOG)/Pure-System.gz
1.5
1.6 $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \
1.7 - Thy/Basics.thy
1.8 + Thy/Basics.thy Thy/Presentation.thy
1.9 @$(USEDIR) -s System Pure Thy
1.10
1.11
2.1 --- a/doc-src/System/Makefile Mon Sep 15 17:32:12 2008 +0200
2.2 +++ b/doc-src/System/Makefile Mon Sep 15 19:42:22 2008 +0200
2.3 @@ -12,8 +12,9 @@
2.4 include ../Makefile.in
2.5
2.6 NAME = system
2.7 -FILES = system.tex Thy/document/Basics.tex misc.tex present.tex symbols.tex \
2.8 - ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
2.9 +FILES = system.tex Thy/document/Basics.tex misc.tex \
2.10 + Thy/document/Presentation.tex symbols.tex ../iman.sty \
2.11 + ../extra.sty ../ttbox.sty ../manual.bib
2.12
2.13 OUTPUT = syms.tex
2.14
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/System/Thy/Presentation.thy Mon Sep 15 19:42:22 2008 +0200
3.3 @@ -0,0 +1,759 @@
3.4 +(* $Id$ *)
3.5 +
3.6 +theory Presentation
3.7 +imports Pure
3.8 +begin
3.9 +
3.10 +chapter {* Presenting theories \label{ch:present} *}
3.11 +
3.12 +text {*
3.13 + Isabelle provides several ways to present the outcome of formal
3.14 + developments, including WWW-based browsable libraries or actual
3.15 + printable documents. Presentation is centered around the concept of
3.16 + \emph{logic sessions}. The global session structure is that of a
3.17 + tree, with Isabelle Pure at its root, further object-logics derived
3.18 + (e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions
3.19 + in leaf positions (usually without a separate image).
3.20 +
3.21 + The Isabelle tools @{tool_ref mkdir} and @{tool_ref make} provide
3.22 + the primary means for managing Isabelle sessions, including proper
3.23 + setup for presentation. Here the @{tool_ref usedir} tool takes care
3.24 + to let @{executable_ref "isabelle-process"} process run any
3.25 + additional stages required for document preparation, notably the
3.26 + tools @{tool_ref document} and @{tool_ref latex}. The complete tool
3.27 + chain for managing batch-mode Isabelle sessions is illustrated in
3.28 + \figref{fig:session-tools}.
3.29 +
3.30 + \begin{figure}[htbp]
3.31 + \begin{center}
3.32 + \begin{tabular}{lp{0.6\textwidth}}
3.33 +
3.34 + @{verbatim "isatool mkdir"} & invoked once by the user to create
3.35 + the initial source setup (common @{verbatim IsaMakefile} plus a
3.36 + single session directory); \\
3.37 +
3.38 + @{verbatim "isatool make"} & invoked repeatedly by the user to
3.39 + keep session output up-to-date (HTML, documents etc.); \\
3.40 +
3.41 + @{verbatim "isatool usedir"} & part of the standard @{verbatim
3.42 + IsaMakefile} entry of a session; \\
3.43 +
3.44 + @{verbatim "isabelle-process"} & run through @{verbatim "isatool
3.45 + usedir"}; \\
3.46 +
3.47 + @{verbatim "isatool document"} & run by the Isabelle process if
3.48 + document preparation is enabled; \\
3.49 +
3.50 + @{verbatim "isatool latex"} & universal {\LaTeX} tool wrapper
3.51 + invoked multiple times by @{verbatim "isatool document"}; also
3.52 + useful for manual experiments; \\
3.53 +
3.54 + \end{tabular}
3.55 + \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
3.56 + \end{center}
3.57 + \end{figure}
3.58 +*}
3.59 +
3.60 +
3.61 +section {* Generating theory browser information \label{sec:info} *}
3.62 +
3.63 +text {*
3.64 + \index{theory browsing information|bold}
3.65 +
3.66 + As a side-effect of running a logic sessions, Isabelle is able to
3.67 + generate theory browsing information, including HTML documents that
3.68 + show a theory's definition, the theorems proved in its ML file and
3.69 + the relationship with its ancestors and descendants. Besides the
3.70 + HTML file that is generated for every theory, Isabelle stores links
3.71 + to all theories in an index file. These indexes are linked with
3.72 + other indexes to represent the overall tree structure of logic
3.73 + sessions.
3.74 +
3.75 + Isabelle also generates graph files that represent the theory
3.76 + hierarchy of a logic. There is a graph browser Java applet embedded
3.77 + in the generated HTML pages, and also a stand-alone application that
3.78 + allows browsing theory graphs without having to start a WWW client
3.79 + first. The latter version also includes features such as generating
3.80 + Postscript files, which are not available in the applet version.
3.81 + See \secref{sec:browse} for further information.
3.82 +
3.83 + \medskip
3.84 +
3.85 + The easiest way to let Isabelle generate theory browsing information
3.86 + for existing sessions is to append ``@{verbatim "-i true"}'' to the
3.87 + @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim
3.88 + "isatool make"} (or @{verbatim "./build"} in the distribution). For
3.89 + example, add something like this to your Isabelle settings file
3.90 +
3.91 +\begin{ttbox}
3.92 +ISABELLE_USEDIR_OPTIONS="-i true"
3.93 +\end{ttbox}
3.94 +
3.95 + and then change into the @{verbatim "src/FOL"} directory of the
3.96 + Isabelle distribution and run @{verbatim "isatool make"}, or even
3.97 + @{verbatim "isatool make all"}. The presentation output will appear
3.98 + in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
3.99 + @{verbatim "~/isabelle/browser_info/FOL"}. Note that option
3.100 + @{verbatim "-v true"} will make the internal runs of @{tool usedir}
3.101 + more explicit about such details.
3.102 +
3.103 + Many standard Isabelle sessions (such as @{verbatim "HOL/ex"}) also
3.104 + provide actual printable documents. These are prepared
3.105 + automatically as well if enabled like this, using the @{verbatim
3.106 + "-d"} option
3.107 +\begin{ttbox}
3.108 +ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
3.109 +\end{ttbox}
3.110 + Enabling options @{verbatim "-i"} and @{verbatim "-d"}
3.111 + simultaneausly as shown above causes an appropriate ``document''
3.112 + link to be included in the HTML index. Documents (or raw document
3.113 + sources) may be generated independently of browser information as
3.114 + well, see \secref{sec:tool-document} for further details.
3.115 +
3.116 + \bigskip The theory browsing information is stored in a
3.117 + sub-directory directory determined by the @{setting_ref
3.118 + ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the
3.119 + session identifier (according to the tree structure of sub-sessions
3.120 + by default). A complete WWW view of all standard object-logics and
3.121 + examples of the Isabelle distribution is available at the Cambridge
3.122 + or Munich Isabelle sites:
3.123 + \begin{center}\small
3.124 + \begin{tabular}{l}
3.125 + \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
3.126 + \url{http://isabelle.in.tum.de/library/} \\
3.127 + \end{tabular}
3.128 + \end{center}
3.129 +
3.130 + \medskip In order to present your own theories on the web, simply
3.131 + copy the corresponding subdirectory from @{setting
3.132 + ISABELLE_BROWSER_INFO} to your WWW server, having generated browser
3.133 + info like this:
3.134 +\begin{ttbox}
3.135 +isatool usedir -i true HOL Foo
3.136 +\end{ttbox}
3.137 +
3.138 + This assumes that directory @{verbatim Foo} contains some @{verbatim
3.139 + ROOT.ML} file to load all your theories, and HOL is your parent
3.140 + logic image (@{verbatim isatool}~@{tool_ref mkdir} assists in
3.141 + setting up Isabelle session directories. Theory browser information
3.142 + for HOL should have been generated already beforehand.
3.143 + Alternatively, one may specify an external link to an existing body
3.144 + of HTML data by giving @{tool usedir} a @{verbatim "-P"} option like
3.145 + this:
3.146 +\begin{ttbox}
3.147 +isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
3.148 +\end{ttbox}
3.149 +
3.150 + \medskip For production use, the @{tool usedir} tool is usually
3.151 + invoked in an appropriate @{verbatim IsaMakefile}, via the Isabelle
3.152 + @{tool make} tool. There is a separate @{tool mkdir} tool to
3.153 + provide easy setup of all this, with only minimal manual editing
3.154 + required.
3.155 +\begin{ttbox}
3.156 +isatool mkdir HOL Foo && isatool make
3.157 +\end{ttbox}
3.158 + See \secref{sec:tool-mkdir} for more information on preparing
3.159 + Isabelle session directories, including the setup for documents.
3.160 +*}
3.161 +
3.162 +
3.163 +section {* Browsing theory graphs \label{sec:browse} *}
3.164 +
3.165 +text {*
3.166 + \index{theory graph browser|bold}
3.167 +
3.168 + The Isabelle graph browser is a general tool for visualizing
3.169 + dependency graphs. Certain nodes of the graph (i.e.~theories) can
3.170 + be grouped together in ``directories'', whose contents may be
3.171 + hidden, thus enabling the user to collapse irrelevant portions of
3.172 + information. The browser is written in Java, it can be used both as
3.173 + a stand-alone application and as an applet. Note that the option
3.174 + @{verbatim "-g"} of @{verbatim isatool}~@{tool_ref usedir} creates
3.175 + graph presentations in batch mode for inclusion in session
3.176 + documents.
3.177 +*}
3.178 +
3.179 +
3.180 +subsection {* Invoking the graph browser *}
3.181 +
3.182 +text {*
3.183 + The stand-alone version of the graph browser is wrapped up as an
3.184 + Isabelle tool called @{tool_def browser}:
3.185 +
3.186 +\begin{ttbox}
3.187 +Usage: browser [OPTIONS] [GRAPHFILE]
3.188 +
3.189 + Options are:
3.190 + -c cleanup -- remove GRAPHFILE after use
3.191 + -o FILE output to FILE (ps, eps, pdf)
3.192 +\end{ttbox}
3.193 + When no filename is specified, the browser automatically changes to
3.194 + the directory @{setting ISABELLE_BROWSER_INFO}.
3.195 +
3.196 + \medskip The @{verbatim "-c"} option causes the input file to be
3.197 + removed after use.
3.198 +
3.199 + The @{verbatim "-o"} option indicates batch-mode operation, with the
3.200 + output written to the indicated file; note that @{verbatim pdf}
3.201 + produces an @{verbatim eps} copy as well.
3.202 +
3.203 + \medskip The applet version of the browser is part of the standard
3.204 + WWW theory presentation, see the link ``theory dependencies'' within
3.205 + each session index.
3.206 +*}
3.207 +
3.208 +
3.209 +subsection {* Using the graph browser *}
3.210 +
3.211 +text {*
3.212 + The browser's main window, which is shown in
3.213 + \figref{fig:browserwindow}, consists of two sub-windows. In the
3.214 + left sub-window, the directory tree is displayed. The graph itself
3.215 + is displayed in the right sub-window.
3.216 +
3.217 + \begin{figure}[ht]
3.218 + \includegraphics[width=\textwidth]{browser_screenshot}
3.219 + \caption{\label{fig:browserwindow} Browser main window}
3.220 + \end{figure}
3.221 +*}
3.222 +
3.223 +
3.224 +subsubsection {* The directory tree window *}
3.225 +
3.226 +text {*
3.227 + We describe the usage of the directory browser and the meaning of
3.228 + the different items in the browser window.
3.229 +
3.230 + \begin{itemize}
3.231 +
3.232 + \item A red arrow before a directory name indicates that the
3.233 + directory is currently ``folded'', i.e.~the nodes in this directory
3.234 + are collapsed to one single node. In the right sub-window, the names
3.235 + of nodes corresponding to folded directories are enclosed in square
3.236 + brackets and displayed in red color.
3.237 +
3.238 + \item A green downward arrow before a directory name indicates that
3.239 + the directory is currently ``unfolded''. It can be folded by
3.240 + clicking on the directory name. Clicking on the name for a second
3.241 + time unfolds the directory again. Alternatively, a directory can
3.242 + also be unfolded by clicking on the corresponding node in the right
3.243 + sub-window.
3.244 +
3.245 + \item Blue arrows stand before ordinary node names. When clicking on
3.246 + such a name (i.e.\ that of a theory), the graph display window
3.247 + focuses to the corresponding node. Double clicking invokes a text
3.248 + viewer window in which the contents of the theory file are
3.249 + displayed.
3.250 +
3.251 + \end{itemize}
3.252 +*}
3.253 +
3.254 +
3.255 +subsubsection {* The graph display window *}
3.256 +
3.257 +text {*
3.258 + When pointing on an ordinary node, an upward and a downward arrow is
3.259 + shown. Initially, both of these arrows are green. Clicking on the
3.260 + upward or downward arrow collapses all predecessor or successor
3.261 + nodes, respectively. The arrow's color then changes to red,
3.262 + indicating that the predecessor or successor nodes are currently
3.263 + collapsed. The node corresponding to the collapsed nodes has the
3.264 + name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply
3.265 + click on the red arrow or on the node with the name ``@{verbatim
3.266 + "[....]"}''. Similar to the directory browser, the contents of
3.267 + theory files can be displayed by double clicking on the
3.268 + corresponding node.
3.269 +*}
3.270 +
3.271 +
3.272 +subsubsection {* The ``File'' menu *}
3.273 +
3.274 +text {*
3.275 + Due to Java Applet security restrictions this menu is only available
3.276 + in the full application version. The meaning of the menu items is as
3.277 + follows:
3.278 +
3.279 + \begin{description}
3.280 +
3.281 + \item[Open \dots] Open a new graph file.
3.282 +
3.283 + \item[Export to PostScript] Outputs the current graph in Postscript
3.284 + format, appropriately scaled to fit on one single sheet of A4 paper.
3.285 + The resulting file can be printed directly.
3.286 +
3.287 + \item[Export to EPS] Outputs the current graph in Encapsulated
3.288 + Postscript format. The resulting file can be included in other
3.289 + documents.
3.290 +
3.291 + \item[Quit] Quit the graph browser.
3.292 +
3.293 + \end{description}
3.294 +*}
3.295 +
3.296 +
3.297 +subsection {* Syntax of graph definition files *}
3.298 +
3.299 +text {*
3.300 + A graph definition file has the following syntax:
3.301 +
3.302 + \begin{tabular}{rcl}
3.303 + @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\
3.304 + @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"}
3.305 + \end{tabular}
3.306 +
3.307 + The meaning of the items in a vertex description is as follows:
3.308 +
3.309 + \begin{description}
3.310 +
3.311 + \item[@{text vertex_name}] The name of the vertex.
3.312 +
3.313 + \item[@{text vertex_ID}] The vertex identifier. Note that there may
3.314 + be several vertices with equal names, whereas identifiers must be
3.315 + unique.
3.316 +
3.317 + \item[@{text dir_name}] The name of the ``directory'' the vertex
3.318 + should be placed in. A ``@{verbatim "+"}'' sign after @{text
3.319 + dir_name} indicates that the nodes in the directory are initially
3.320 + visible. Directories are initially invisible by default.
3.321 +
3.322 + \item[@{text path}] The path of the corresponding theory file. This
3.323 + is specified relatively to the path of the graph definition file.
3.324 +
3.325 + \item[List of successor/predecessor nodes] A ``@{verbatim "<"}''
3.326 + sign before the list means that successor nodes are listed, a
3.327 + ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
3.328 + neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
3.329 + browser assumes that successor nodes are listed.
3.330 +
3.331 + \end{description}
3.332 +*}
3.333 +
3.334 +
3.335 +section {* Creating Isabelle session directories
3.336 + \label{sec:tool-mkdir} *}
3.337 +
3.338 +text {*
3.339 + The @{tool_def mkdir} utility prepares Isabelle session source
3.340 + directories, including a sensible default setup of @{verbatim
3.341 + IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document}
3.342 + directory with a minimal @{verbatim root.tex} that is sufficient to
3.343 + print all theories of the session (in the order of appearance); see
3.344 + \secref{sec:tool-document} for further information on Isabelle
3.345 + document preparation. The usage of @{verbatim "isatool mkdir"} is:
3.346 +
3.347 +\begin{ttbox}
3.348 +Usage: mkdir [OPTIONS] [LOGIC] NAME
3.349 +
3.350 + Options are:
3.351 + -I FILE alternative IsaMakefile output
3.352 + -P include parent logic target
3.353 + -b setup build mode (session outputs heap image)
3.354 + -q quiet mode
3.355 +
3.356 + Prepare session directory, including IsaMakefile and document source,
3.357 + with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
3.358 +\end{ttbox}
3.359 +
3.360 + The @{tool mkdir} tool is conservative in the sense that any
3.361 + existing @{verbatim IsaMakefile} etc.\ is left unchanged. Thus it
3.362 + is safe to invoke it multiple times, although later runs may not
3.363 + have the desired effect.
3.364 +
3.365 + Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile}
3.366 + incrementally --- manual changes are required for multiple
3.367 + sub-sessions. On order to get an initial working session, the only
3.368 + editing needed is to add appropriate @{ML use_thy} calls to the
3.369 + generated @{verbatim ROOT.ML} file.
3.370 +*}
3.371 +
3.372 +
3.373 +subsubsection {* Options *}
3.374 +
3.375 +text {*
3.376 + The @{verbatim "-I"} option specifies an alternative to @{verbatim
3.377 + IsaMakefile} for dependencies. Note that ``@{verbatim "-"}'' refers
3.378 + to \emph{stdout}, i.e.\ ``@{verbatim "-I-"}'' provides an easy way
3.379 + to peek at @{tool mkdir}'s idea of @{tool make} setup required for
3.380 + some particular of Isabelle session.
3.381 +
3.382 + \medskip The @{verbatim "-P"} option includes a target for the
3.383 + parent @{verbatim LOGIC} session in the generated @{verbatim
3.384 + IsaMakefile}. The corresponding sources are assumed to be located
3.385 + within the Isabelle distribution.
3.386 +
3.387 + \medskip The @{verbatim "-b"} option sets up the current directory
3.388 + as the base for a new session that provides an actual logic image,
3.389 + as opposed to one that only runs several theories based on an
3.390 + existing image. Note that in the latter case, everything except
3.391 + @{verbatim IsaMakefile} would be placed into a separate directory
3.392 + @{verbatim NAME}, rather than the current one. See
3.393 + \secref{sec:tool-usedir} for further information on \emph{build
3.394 + mode} vs.\ \emph{example mode} of the @{tool usedir} utility.
3.395 +
3.396 + \medskip The @{verbatim "-q"} option enables quiet mode, suppressing
3.397 + further notes on how to proceed.
3.398 +*}
3.399 +
3.400 +
3.401 +subsubsection {* Examples *}
3.402 +
3.403 +text {*
3.404 + The standard setup of a single ``example session'' based on the
3.405 + default logic, with proper document generation is generated like
3.406 + this:
3.407 +\begin{ttbox}
3.408 +isatool mkdir Foo && isatool make
3.409 +\end{ttbox}
3.410 +
3.411 + \noindent The theory sources should be put into the @{verbatim Foo}
3.412 + directory, and its @{verbatim ROOT.ML} should be edited to load all
3.413 + required theories. Invoking @{verbatim "isatool make"} again would
3.414 + run the whole session, generating browser information and the
3.415 + document automatically. The @{verbatim IsaMakefile} is typically
3.416 + tuned manually later, e.g.\ adding source dependencies, or changing
3.417 + the options passed to @{tool usedir}.
3.418 +
3.419 + \medskip Large projects may demand further sessions, potentially
3.420 + with separate logic images being created. This usually requires
3.421 + manual editing of the generated @{verbatim IsaMakefile}, which is
3.422 + meant to cover all of the sub-session directories at the same time
3.423 + (this is the deeper reasong why @{verbatim IsaMakefile} is not made
3.424 + part of the initial session directory created by @{verbatim "isatool
3.425 + mkdir"}). See @{verbatim "src/HOL/IsaMakefile"} of the Isabelle
3.426 + distribution for a full-blown example.
3.427 +*}
3.428 +
3.429 +
3.430 +section {* Running Isabelle sessions \label{sec:tool-usedir} *}
3.431 +
3.432 +text {*
3.433 + The @{tool_def usedir} utility builds object-logic images, or runs
3.434 + example sessions based on existing logics. Its usage is:
3.435 +\begin{ttbox}
3.436 +
3.437 +Usage: usedir [OPTIONS] LOGIC NAME
3.438 +
3.439 + Options are:
3.440 + -C BOOL copy existing document directory to -D PATH (default true)
3.441 + -D PATH dump generated document sources into PATH
3.442 + -M MAX multithreading: maximum number of worker threads (default 1)
3.443 + -P PATH set path for remote theory browsing information
3.444 + -T LEVEL multithreading: trace level (default 0)
3.445 + -V VERSION declare alternative document VERSION
3.446 + -b build mode (output heap image, using current dir)
3.447 + -c BOOL tell ML system to compress output image (default true)
3.448 + -d FORMAT build document as FORMAT (default false)
3.449 + -f NAME use ML file NAME (default ROOT.ML)
3.450 + -g BOOL generate session graph image for document (default false)
3.451 + -i BOOL generate theory browser information (default false)
3.452 + -m MODE add print mode for output
3.453 + -p LEVEL set level of detail for proof objects
3.454 + -r reset session path
3.455 + -s NAME override session NAME
3.456 + -v BOOL be verbose (default false)
3.457 +
3.458 + Build object-logic or run examples. Also creates browsing
3.459 + information (HTML etc.) according to settings.
3.460 +
3.461 + ISABELLE_USEDIR_OPTIONS=
3.462 + HOL_USEDIR_OPTIONS=
3.463 +\end{ttbox}
3.464 +
3.465 + Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
3.466 + setting is implicitly prefixed to \emph{any} @{tool usedir}
3.467 + call. Since the @{verbatim IsaMakefile}s of all object-logics
3.468 + distributed with Isabelle just invoke \texttt{usedir} for the real
3.469 + work, one may control compilation options globally via above
3.470 + variable. In particular, generation of \rmindex{HTML} browsing
3.471 + information and document preparation is controlled here.
3.472 +
3.473 + The @{setting_ref HOL_USEDIR_OPTIONS} setting is specific to the
3.474 + plain and main Isabelle/HOL images; its value is appended to
3.475 + @{setting ISABELLE_USEDIR_OPTIONS} for these particular sessions
3.476 + only.
3.477 +*}
3.478 +
3.479 +
3.480 +subsubsection {* Options *}
3.481 +
3.482 +text {*
3.483 + Basically, there are two different modes of operation: \emph{build
3.484 + mode} (enabled through the @{verbatim "-b"} option) and
3.485 + \emph{example mode} (default).
3.486 +
3.487 + Calling @{tool usedir} with @{verbatim "-b"} runs @{executable
3.488 + "isabelle-process"} with input image @{verbatim LOGIC} and output to
3.489 + @{verbatim NAME}, as provided on the command line. This will be a
3.490 + batch session, running @{verbatim ROOT.ML} from the current
3.491 + directory and then quitting. It is assumed that @{verbatim ROOT.ML}
3.492 + contains all ML commands required to build the logic.
3.493 +
3.494 + In example mode, @{verbatim usedir} runs a read-only session of
3.495 + @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from
3.496 + within directory @{verbatim NAME}. It assumes that this file
3.497 + contains appropriate ML commands to run the desired examples.
3.498 +
3.499 + \medskip The @{verbatim "-i"} option controls theory browser data
3.500 + generation. It may be explicitly turned on or off --- as usual, the
3.501 + last occurrence of @{verbatim "-i"} on the command line wins.
3.502 +
3.503 + The @{verbatim "-P"} option specifies a path (or actual URL) to be
3.504 + prefixed to any \emph{non-local} reference of existing theories.
3.505 + Thus user sessions may easily link to existing Isabelle libraries
3.506 + already present on the WWW.
3.507 +
3.508 + The @{verbatim "-m"} options specifies additional print modes to be
3.509 + activated temporarily while the session is processed.
3.510 +
3.511 + \medskip The @{verbatim "-d"} option controls document preparation.
3.512 + Valid arguments are @{verbatim false} (do not prepare any document;
3.513 + this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz},
3.514 + @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}. The logic
3.515 + session has to provide a properly setup @{verbatim document}
3.516 + directory. See \secref{sec:tool-document} and
3.517 + \secref{sec:tool-latex} for more details.
3.518 +
3.519 + \medskip The @{verbatim "-V"} option declares alternative document
3.520 + versions, consisting of name/tags pairs (cf.\ options @{verbatim
3.521 + "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool). The
3.522 + standard document is equivalent to ``@{verbatim
3.523 + "document=theory,proof,ML"}'', which means that all theory begin/end
3.524 + commands, proof body texts, and ML code will be presented
3.525 + faithfully. An alternative version ``@{verbatim
3.526 + "outline=/proof/ML"}'' would fold proof and ML parts, replacing the
3.527 + original text by a short place-holder. The form ``@{text
3.528 + name}@{verbatim "=-"},'' means to remove document @{text name} from
3.529 + the list of versions to be processed. Any number of @{verbatim
3.530 + "-V"} options may be given; later declarations have precedence over
3.531 + earlier ones.
3.532 +
3.533 + \medskip The @{verbatim "-g"} option produces images of the theory
3.534 + dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
3.535 + generated document, both as @{verbatim session_graph.eps} and
3.536 + @{verbatim session_graph.pdf} at the same time. To include this in
3.537 + the final {\LaTeX} document one could say @{verbatim
3.538 + "\\includegraphics{session_graph}"} in @{verbatim
3.539 + "document/root.tex"} (omitting the file-name extension enables
3.540 + {\LaTeX} to select to correct version, either for the DVI or PDF
3.541 + output path).
3.542 +
3.543 + \medskip The @{verbatim "-D"} option causes the generated document
3.544 + sources to be dumped at location @{verbatim PATH}; this path is
3.545 + relative to the session's main directory. If the @{verbatim "-C"}
3.546 + option is true, this will include a copy of an existing @{verbatim
3.547 + document} directory as provided by the user. For example,
3.548 + @{verbatim "isatool usedir -D generated HOL Foo"} produces a
3.549 + complete set of document sources at @{verbatim "Foo/generated"}.
3.550 + Subsequent invocation of @{verbatim "isatool document
3.551 + Foo/generated"} (see also \secref{sec:tool-document}) will process
3.552 + the final result independently of an Isabelle job. This decoupled
3.553 + mode of operation facilitates debugging of serious {\LaTeX} errors,
3.554 + for example.
3.555 +
3.556 + \medskip The @{verbatim "-p"} option determines the level of detail
3.557 + for internal proof objects, see also the \emph{Isabelle Reference
3.558 + Manual}~\cite{isabelle-ref}.
3.559 +
3.560 + \medskip The @{verbatim "-v"} option causes additional information
3.561 + to be printed while running the session, notably the location of
3.562 + prepared documents.
3.563 +
3.564 + \medskip The @{verbatim "-M"} option specifies the maximum number of
3.565 + parallel threads used for processing independent tasks when checking
3.566 + theory sources (multithreading only works on suitable ML platforms).
3.567 + The special value of ``@{verbatim 0}'' or ``@{verbatim max}'' refers
3.568 + to the number of actual CPU cores of the underlying machine, which
3.569 + is a good starting point for optimal performance tuning. The
3.570 + @{verbatim "-T"} option determines the level of detail in tracing
3.571 + output concerning the internal locking and scheduling in
3.572 + multithreaded operation. This may be helpful in isolating
3.573 + performance bottle-necks, e.g.\ due to excessive wait states when
3.574 + locking critical code sections.
3.575 +
3.576 + \medskip Any @{tool usedir} session is named by some \emph{session
3.577 + identifier}. These accumulate, documenting the way sessions depend
3.578 + on others. For example, consider @{verbatim "Pure/FOL/ex"}, which
3.579 + refers to the examples of FOL, which in turn is built upon Pure.
3.580 +
3.581 + The current session's identifier is by default just the base name of
3.582 + the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim
3.583 + NAME} argument (in example mode). This may be overridden explicitly
3.584 + via the @{verbatim "-s"} option.
3.585 +*}
3.586 +
3.587 +
3.588 +subsubsection {* Examples *}
3.589 +
3.590 +text {*
3.591 + Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's
3.592 + object-logics as a model for your own developments. For example,
3.593 + see @{verbatim "src/FOL/IsaMakefile"}. The Isabelle @{tool_ref
3.594 + mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation
3.595 + of @{tool usedir} as well.
3.596 +*}
3.597 +
3.598 +
3.599 +section {* Preparing Isabelle session documents
3.600 + \label{sec:tool-document} *}
3.601 +
3.602 +text {*
3.603 + The @{tool_def document} utility prepares logic session documents,
3.604 + processing the sources both as provided by the user and generated by
3.605 + Isabelle. Its usage is:
3.606 +\begin{ttbox}
3.607 +Usage: document [OPTIONS] [DIR]
3.608 +
3.609 + Options are:
3.610 + -c cleanup -- be aggressive in removing old stuff
3.611 + -n NAME specify document name (default 'document')
3.612 + -o FORMAT specify output format: dvi (default), dvi.gz, ps,
3.613 + ps.gz, pdf
3.614 + -t TAGS specify tagged region markup
3.615 +
3.616 + Prepare the theory session document in DIR (default 'document')
3.617 + producing the specified output format.
3.618 +\end{ttbox}
3.619 + This tool is usually run automatically as part of the corresponding
3.620 + Isabelle batch process, provided document preparation has been
3.621 + enabled (cf.\ the @{verbatim "-d"} option of the @{tool_ref usedir}
3.622 + tool). It may be manually invoked on the generated browser
3.623 + information document output as well, e.g.\ in case of errors
3.624 + encountered in the batch run.
3.625 +
3.626 + \medskip The @{verbatim "-c"} option tells the @{tool document} tool
3.627 + to dispose the document sources after successful operation. This is
3.628 + the right thing to do for sources generated by an Isabelle process,
3.629 + but take care of your files in manual document preparation!
3.630 +
3.631 + \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify
3.632 + the final output file name and format, the default is ``@{verbatim
3.633 + document.dvi}''. Note that the result will appear in the parent of
3.634 + the target @{verbatim DIR}.
3.635 +
3.636 + \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret
3.637 + tagged Isabelle command regions. Tags are specified as a comma
3.638 + separated list of modifier/name pairs: ``@{verbatim "+"}@{text
3.639 + foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim
3.640 + "-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to
3.641 + fold text tagged as @{text foo}. The builtin default is equivalent
3.642 + to the tag specification ``@{verbatim
3.643 + "/theory,/proof,/ML,+visible,-invisible"}''; see also the {\LaTeX}
3.644 + macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
3.645 + @{verbatim "\\isafoldtag"}, in @{verbatim isabelle.sty}.
3.646 +
3.647 + \medskip Document preparation requires a properly setup ``@{verbatim
3.648 + document}'' directory within the logic session sources. This
3.649 + directory is supposed to contain all the files needed to produce the
3.650 + final document --- apart from the actual theories which are
3.651 + generated by Isabelle.
3.652 +
3.653 + \medskip For most practical purposes, the @{tool document} tool is
3.654 + smart enough to create any of the specified output formats, taking
3.655 + @{verbatim root.tex} supplied by the user as a starting point. This
3.656 + even includes multiple runs of {\LaTeX} to accommodate references
3.657 + and bibliographies (the latter assumes @{verbatim root.bib} within
3.658 + the same directory).
3.659 +
3.660 + In more complex situations, a separate @{verbatim IsaMakefile} for
3.661 + the document sources may be given instead. This should provide
3.662 + targets for any admissible document format; these have to produce
3.663 + corresponding output files named after @{verbatim root} as well,
3.664 + e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}.
3.665 +
3.666 + \medskip When running the session, Isabelle copies the original
3.667 + @{verbatim document} directory into its proper place within
3.668 + @{verbatim ISABELLE_BROWSER_INFO} according to the session path.
3.669 + Then, for any processed theory @{text A} some {\LaTeX} source is
3.670 + generated and put there as @{text A}@{verbatim ".tex"}.
3.671 + Furthermore, a list of all generated theory files is put into
3.672 + @{verbatim session.tex}. Typically, the root {\LaTeX} file provided
3.673 + by the user would include @{verbatim session.tex} to get a document
3.674 + containing all the theories.
3.675 +
3.676 + The {\LaTeX} versions of the theories require some macros defined in
3.677 + @{verbatim isabelle.sty} as distributed with Isabelle. Doing
3.678 + @{verbatim "\\usepackage{isabelle}"} in @{verbatim root.tex} should
3.679 + be fine; the underlying Isabelle @{tool latex} tool already includes
3.680 + an appropriate path specification for {\TeX} inputs.
3.681 +
3.682 + If the text contains any references to Isabelle symbols (such as
3.683 + @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim
3.684 + isabellesym.sty} should be included as well. This package contains
3.685 + a standard set of {\LaTeX} macro definitions @{verbatim
3.686 + "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
3.687 + "<"}@{text foo}@{verbatim ">"}, (see \appref{app:symbols} for a
3.688 + complete list of predefined Isabelle symbols). Users may invent
3.689 + further symbols as well, just by providing {\LaTeX} macros in a
3.690 + similar fashion as in @{verbatim isabellesym.sty} of the
3.691 + distribution.
3.692 +
3.693 + For proper setup of DVI and PDF documents (with hyperlinks and
3.694 + bookmarks), we recommend to include @{verbatim pdfsetup.sty} as
3.695 + well.
3.696 +
3.697 + \medskip As a final step of document preparation within Isabelle,
3.698 + @{verbatim "isatool document -c"} is run on the resulting @{verbatim
3.699 + document} directory. Thus the actual output document is built and
3.700 + installed in its proper place (as linked by the session's @{verbatim
3.701 + index.html} if option @{verbatim "-i"} of @{tool_ref usedir} has
3.702 + been enabled, cf.\ \secref{sec:info}). The generated sources are
3.703 + deleted after successful run of {\LaTeX} and friends. Note that a
3.704 + separate copy of the sources may be retained by passing an option
3.705 + @{verbatim "-D"} to the @{tool usedir} utility when running the
3.706 + session.
3.707 +*}
3.708 +
3.709 +
3.710 +section {* Running {\LaTeX} within the Isabelle environment
3.711 + \label{sec:tool-latex} *}
3.712 +
3.713 +text {*
3.714 + The @{tool_def latex} utility provides the basic interface for
3.715 + Isabelle document preparation. Its usage is:
3.716 +\begin{ttbox}
3.717 +Usage: latex [OPTIONS] [FILE]
3.718 +
3.719 + Options are:
3.720 + -o FORMAT specify output format: dvi (default), dvi.gz, ps,
3.721 + ps.gz, pdf, bbl, idx, sty, syms
3.722 +
3.723 + Run LaTeX (and related tools) on FILE (default root.tex),
3.724 + producing the specified output format.
3.725 +\end{ttbox}
3.726 +
3.727 + Appropriate {\LaTeX}-related programs are run on the input file,
3.728 + according to the given output format: @{executable latex},
3.729 + @{executable pdflatex}, @{executable dvips}, @{executable bibtex}
3.730 + (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim
3.731 + idx}). The actual commands are determined from the settings
3.732 + environment (@{setting ISABELLE_LATEX} etc.).
3.733 +
3.734 + The @{verbatim sty} output format causes the Isabelle style files to
3.735 + be updated from the distribution. This is useful in special
3.736 + situations where the document sources are to be processed another
3.737 + time by separate tools (cf.\ option @{verbatim "-D"} of the @{tool
3.738 + usedir} utility).
3.739 +
3.740 + The @{verbatim syms} output is for internal use; it generates lists
3.741 + of symbols that are available without loading additional {\LaTeX}
3.742 + packages.
3.743 +*}
3.744 +
3.745 +
3.746 +subsubsection {* Examples *}
3.747 +
3.748 +text {*
3.749 + Invoking @{verbatim "isatool latex"} by hand may be occasionally
3.750 + useful when debugging failed attempts of the automatic document
3.751 + preparation stage of batch-mode Isabelle. The abortive process
3.752 + leaves the sources at a certain place within @{setting
3.753 + ISABELLE_BROWSER_INFO}, see the runtime error message for details.
3.754 + This enables users to inspect {\LaTeX} runs in further detail, e.g.\
3.755 + like this:
3.756 +\begin{ttbox}
3.757 + cd ~/isabelle/browser_info/HOL/Test/document
3.758 + isatool latex -o pdf
3.759 +\end{ttbox}
3.760 +*}
3.761 +
3.762 +end
3.763 \ No newline at end of file
4.1 --- a/doc-src/System/Thy/ROOT.ML Mon Sep 15 17:32:12 2008 +0200
4.2 +++ b/doc-src/System/Thy/ROOT.ML Mon Sep 15 19:42:22 2008 +0200
4.3 @@ -5,3 +5,4 @@
4.4 use "../../antiquote_setup.ML";
4.5
4.6 use_thy "Basics";
4.7 +use_thy "Presentation";
5.1 --- a/doc-src/System/present.tex Mon Sep 15 17:32:12 2008 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,647 +0,0 @@
5.4 -
5.5 -%% $Id$
5.6 -
5.7 -\chapter{Presenting theories}\label{ch:present}
5.8 -
5.9 -Isabelle provides several ways to present the outcome of formal developments,
5.10 -including WWW-based browsable libraries or actual printable documents.
5.11 -Presentation is centered around the concept of \emph{logic sessions}. The
5.12 -global session structure is that of a tree, with Isabelle Pure at its root,
5.13 -further object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and
5.14 -application sessions in leaf positions (usually without a separate image).
5.15 -
5.16 -The \texttt{mkdir} (see \S\ref{sec:tool-mkdir}) and \texttt{make} (see
5.17 -\S\ref{sec:tool-make}) tools of Isabelle provide the primary means for
5.18 -managing Isabelle sessions, including proper setup for presentation. Here the
5.19 -\texttt{usedir} (see \S\ref{sec:tool-usedir}) tool takes care to let the
5.20 -\texttt{isabelle} process run any additional stages required for document
5.21 -preparation, notably the tools \texttt{document} (see
5.22 -\S\ref{sec:tool-document}) and \texttt{latex} (see \S\ref{sec:tool-latex}).
5.23 -The complete tool chain for managing batch-mode Isabelle sessions is
5.24 -illustrated in figure~\ref{fig:session-tools}.
5.25 -
5.26 -\begin{figure}[htbp]
5.27 - \begin{center}
5.28 - \begin{tabular}{lp{0.6\textwidth}}
5.29 - \texttt{isatool mkdir} & invoked once by the user to create the initial
5.30 - source setup (common \texttt{IsaMakefile} plus a single session directory); \\
5.31 - \texttt{isatool make} & invoked repeatedly by the user to
5.32 - keep session output up-to-date (HTML, documents etc.); \\
5.33 - \texttt{isatool usedir} & part of the standard \texttt{IsaMakefile} entry of a session; \\
5.34 - \texttt{isabelle} & run through \texttt{isatool usedir}; \\
5.35 - \texttt{isatool document} & run by the Isabelle process if document preparation is enabled; \\
5.36 - \texttt{isatool latex} & universal {\LaTeX} tool wrapper invoked multiple times
5.37 - by \texttt{isatool document}; also useful for manual experiments; \\
5.38 - \end{tabular}
5.39 - \caption{The tool chain of Isabelle session presentation}
5.40 - \label{fig:session-tools}
5.41 - \end{center}
5.42 -\end{figure}
5.43 -
5.44 -
5.45 -\section{Generating theory browser information} \label{sec:info}
5.46 -\index{theory browsing information|bold}
5.47 -
5.48 -As a side-effect of running a logic sessions, Isabelle is able to generate
5.49 -theory browsing information, including HTML documents that show a theory's
5.50 -definition, the theorems proved in its ML file and the relationship with its
5.51 -ancestors and descendants. Besides the HTML file that is generated for every
5.52 -theory, Isabelle stores links to all theories in an index file. These indexes
5.53 -are linked with other indexes to represent the overall tree structure of logic
5.54 -sessions.
5.55 -
5.56 -Isabelle also generates graph files that represent the theory hierarchy of a
5.57 -logic. There is a graph browser Java applet embedded in the generated HTML
5.58 -pages, and also a stand-alone application that allows browsing theory graphs
5.59 -without having to start a WWW client first. The latter version also includes
5.60 -features such as generating Postscript files, which are not available in the
5.61 -applet version. See \S\ref{sec:browse} for further information.
5.62 -
5.63 -\medskip
5.64 -
5.65 -The easiest way to let Isabelle generate theory browsing information for
5.66 -existing sessions is to append ``\texttt{-i true}'' to the
5.67 -\settdx{ISABELLE_USEDIR_OPTIONS} before invoking \texttt{isatool make} (or
5.68 -\texttt{./build} in the distribution). For example, add something like this
5.69 -to your Isabelle settings file
5.70 -\begin{ttbox}
5.71 -ISABELLE_USEDIR_OPTIONS="-i true"
5.72 -\end{ttbox}
5.73 -and then change into the \texttt{src/FOL} directory of the Isabelle
5.74 -distribution and run \texttt{isatool make}, or even \texttt{isatool make all}.
5.75 -The presentation output will appear in \texttt{\$ISABELLE_BROWSER_INFO/FOL},
5.76 -which usually refers to \verb,~/isabelle/browser_info/FOL,. Note that option
5.77 -\texttt{-v true} will make the internal runs of \texttt{usedir} more explicit
5.78 -about such details.
5.79 -
5.80 -Many standard Isabelle sessions (such as \texttt{HOL/ex}) also provide actual
5.81 -printable documents. These are prepared automatically as well if enabled like
5.82 -this, using the \texttt{-d} option
5.83 -\begin{ttbox}
5.84 -ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
5.85 -\end{ttbox}
5.86 -Enabling options \texttt{-i} and \texttt{-d} simultaneausly as shown above
5.87 -causes an appropriate ``document'' link to be included in the HTML index.
5.88 -Documents (or raw document sources) may be generated independently of browser
5.89 -information as well, see \S\ref{sec:tool-document} for further details.
5.90 -
5.91 -\bigskip The theory browsing information is stored in a sub-directory
5.92 -directory determined by the \settdx{ISABELLE_BROWSER_INFO} setting plus a
5.93 -prefix corresponding to the session identifier (according to the tree
5.94 -structure of sub-sessions by default). A complete WWW view of all standard
5.95 -object-logics and examples of the Isabelle distribution is available at the
5.96 -Cambridge or Munich Isabelle sites:
5.97 -\begin{center}\small
5.98 - \begin{tabular}{l}
5.99 - \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
5.100 - \url{http://isabelle.in.tum.de/library/} \\
5.101 - \end{tabular}
5.102 -\end{center}
5.103 -
5.104 -\medskip In order to present your own theories on the web, simply copy the
5.105 -corresponding subdirectory from \texttt{ISABELLE_BROWSER_INFO} to your WWW
5.106 -server, having generated browser info like this:
5.107 -\begin{ttbox}
5.108 -isatool usedir -i true HOL Foo
5.109 -\end{ttbox}
5.110 -This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file
5.111 -to load all your theories, and HOL is your parent logic image (\texttt{isatool
5.112 - mkdir} assists in setting up Isabelle session directories, see
5.113 -\S\ref{sec:tool-mkdir}). Theory browser information for HOL should have been
5.114 -generated already beforehand. Alternatively, one may specify an external link
5.115 -to an existing body of HTML data by giving \texttt{usedir} a \texttt{-P}
5.116 -option like this:
5.117 -\begin{ttbox}
5.118 -isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
5.119 -\end{ttbox}
5.120 -
5.121 -\medskip For production use, the \texttt{usedir} tool is usually invoked in an
5.122 -appropriate \texttt{IsaMakefile}, via the Isabelle \texttt{make} utility.
5.123 -There is a separate \texttt{mkdir} tool to provide easy setup of all this,
5.124 -with only minimal manual editing required.
5.125 -\begin{ttbox}
5.126 -isatool mkdir HOL Foo && isatool make
5.127 -\end{ttbox}
5.128 -See \S\ref{sec:tool-mkdir} for more information on preparing Isabelle session
5.129 -directories, including the setup for documents.
5.130 -
5.131 -
5.132 -\section{Browsing theory graphs} \label{sec:browse}
5.133 -\index{theory graph browser|bold}
5.134 -
5.135 -The Isabelle graph browser is a general tool for visualizing dependency
5.136 -graphs. Certain nodes of the graph (i.e.~theories) can be grouped together in
5.137 -``directories'', whose contents may be hidden, thus enabling the user to
5.138 -collapse irrelevant portions of information. The browser is written in Java,
5.139 -it can be used both as a stand-alone application and as an applet. Note that
5.140 -the option \texttt{-g} of \texttt{isatool usedir} (see
5.141 -\S\ref{sec:tool-usedir}) creates graph presentations in batch mode for
5.142 -inclusion in session documents.
5.143 -
5.144 -
5.145 -\subsection{Invoking the graph browser}
5.146 -
5.147 -The stand-alone version of the graph browser is wrapped up as an
5.148 -Isabelle tool called \tooldx{browser}:
5.149 -\begin{ttbox}
5.150 -Usage: browser [OPTIONS] [GRAPHFILE]
5.151 -
5.152 - Options are:
5.153 - -c cleanup -- remove GRAPHFILE after use
5.154 - -o FILE output to FILE (ps, eps, pdf)
5.155 -\end{ttbox}
5.156 -When no filename is specified, the browser automatically changes to the
5.157 -directory \texttt{ISABELLE_BROWSER_INFO}.
5.158 -
5.159 -\medskip The \texttt{-c} option causes the input file to be removed after use.
5.160 -
5.161 -The \texttt{-o} option indicates batch-mode operation, with the output written
5.162 -to the indicated file; note that \texttt{pdf} produces an \texttt{eps} copy as
5.163 -well.
5.164 -
5.165 -\medskip The applet version of the browser is part of the standard WWW theory
5.166 -presentation, see the link ``theory dependencies'' within each session index.
5.167 -
5.168 -
5.169 -\subsection{Using the graph browser}
5.170 -
5.171 -The browser's main window, which is shown in figure
5.172 -\ref{fig:browserwindow}, consists of two sub-windows: In the left
5.173 -sub-window, the directory tree is displayed. The graph itself is
5.174 -displayed in the right sub-window.
5.175 -\begin{figure}[ht]
5.176 - \includegraphics[width=\textwidth]{browser_screenshot}
5.177 - \caption{\label{fig:browserwindow} Browser main window}
5.178 -\end{figure}
5.179 -
5.180 -
5.181 -\subsubsection*{The directory tree window}
5.182 -
5.183 -We describe the usage of the directory browser and the meaning of the
5.184 -different items in the browser window.
5.185 -\begin{itemize}
5.186 -
5.187 -\item A red arrow before a directory name indicates that the directory
5.188 - is currently ``folded'', i.e.~the nodes in this directory are
5.189 - collapsed to one single node. In the right sub-window, the names of
5.190 - nodes corresponding to folded directories are enclosed in square
5.191 - brackets and displayed in red color.
5.192 -
5.193 -\item A green downward arrow before a directory name indicates that
5.194 - the directory is currently ``unfolded''. It can be folded by
5.195 - clicking on the directory name. Clicking on the name for a second
5.196 - time unfolds the directory again. Alternatively, a directory can
5.197 - also be unfolded by clicking on the corresponding node in the right
5.198 - sub-window.
5.199 -
5.200 -\item Blue arrows stand before ordinary node names. When clicking on such a
5.201 - name (i.e.\ that of a theory), the graph display window focuses to the
5.202 - corresponding node. Double clicking invokes a text viewer window in which
5.203 - the contents of the theory file are displayed.
5.204 -
5.205 -\end{itemize}
5.206 -
5.207 -
5.208 -\subsubsection*{The graph display window}
5.209 -
5.210 -When pointing on an ordinary node, an upward and a downward arrow is
5.211 -shown. Initially, both of these arrows are green. Clicking on the
5.212 -upward or downward arrow collapses all predecessor or successor nodes,
5.213 -respectively. The arrow's color then changes to red, indicating that
5.214 -the predecessor or successor nodes are currently collapsed. The node
5.215 -corresponding to the collapsed nodes has the name ``{\tt [....]}''. To
5.216 -uncollapse the nodes again, simply click on the red arrow or on the
5.217 -node with the name ``{\tt [....]}''. Similar to the directory browser,
5.218 -the contents of theory files can be displayed by double clicking on
5.219 -the corresponding node.
5.220 -
5.221 -
5.222 -\subsubsection*{The ``File'' menu}
5.223 -
5.224 -Please note that due to Java security restrictions this menu is not
5.225 -available in the applet version. The meaning of the menu items is as
5.226 -follows:
5.227 -\begin{description}
5.228 -
5.229 -\item[Open \dots] Open a new graph file.
5.230 -
5.231 -\item[Export to PostScript] Outputs the current graph in Postscript format,
5.232 - appropriately scaled to fit on one single sheet of A4 paper. The resulting
5.233 - file can be printed directly.
5.234 -
5.235 -\item[Export to EPS] Outputs the current graph in Encapsulated Postscript
5.236 - format. The resulting file can be included in other documents.
5.237 -
5.238 -\item[Quit] Quit the graph browser.
5.239 -
5.240 -\end{description}
5.241 -
5.242 -
5.243 -\subsection*{*Syntax of graph definition files}
5.244 -
5.245 -A graph definition file has the following syntax:
5.246 -\begin{eqnarray*}
5.247 - \mbox{\it graph} & = & \{ \: \mbox{\it vertex \tt ;} \: \} ^ + \\
5.248 - vertex & = & \mbox{\it vertexname} \: \mbox{\it vertexID} \: \mbox{\it dirname} \: [ \mbox{\tt +} ]
5.249 - \: \mbox{\it path} \: [ \mbox{\tt <} | \mbox{\tt >} ] \: \{ \: \mbox{\it vertexID} \: \} ^ *
5.250 -\end{eqnarray*}
5.251 -
5.252 -The meaning of the items in a vertex description is as follows:
5.253 -\begin{description}
5.254 -
5.255 -\item[vertexname] The name of the vertex.
5.256 -
5.257 -\item[vertexID] The vertex identifier. Note that there may be two
5.258 - vertices with equal names, whereas identifiers must be unique.
5.259 -
5.260 -\item[dirname] The name of the ``directory'' the vertex should be
5.261 - placed in. A ``{\tt +}'' sign after {\it dirname} indicates that
5.262 - the nodes in the directory are initially visible. Directories are
5.263 - initially invisible by default.
5.264 -
5.265 -\item[path] The path of the corresponding theory file. This is
5.266 - specified relatively to the path of the graph definition file.
5.267 -
5.268 -\item[List of successor/predecessor nodes] A ``{\tt <}'' sign before
5.269 - the list means that successor nodes are listed, a ``{\tt >}'' sign
5.270 - means that predecessor nodes are listed. If neither ``{\tt <}'' nor
5.271 - ``{\tt >}'' is found, the browser assumes that successor nodes are
5.272 - listed.
5.273 -
5.274 -\end{description}
5.275 -
5.276 -
5.277 -\section{Creating Isabelle session directories --- \texttt{isatool mkdir}}
5.278 -\label{sec:tool-mkdir}
5.279 -
5.280 -The \tooldx{mkdir} utility prepares Isabelle session source directories,
5.281 -including a sensible default setup of \texttt{IsaMakefile}, \texttt{ROOT.ML},
5.282 -and a \texttt{document} directory with a minimal \texttt{root.tex} that is
5.283 -sufficient to print all theories of the session (in the order of appearance);
5.284 -see \S\ref{sec:tool-document} for further information on Isabelle document
5.285 -preparation. The usage of \texttt{isatool mkdir} is:
5.286 -\begin{ttbox}
5.287 -Usage: mkdir [OPTIONS] [LOGIC] NAME
5.288 -
5.289 - Options are:
5.290 - -I FILE alternative IsaMakefile output
5.291 - -P include parent logic target
5.292 - -b setup build mode (session outputs heap image)
5.293 - -q quiet mode
5.294 -
5.295 - Prepare session directory, including IsaMakefile and document source,
5.296 - with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
5.297 -\end{ttbox}
5.298 -
5.299 -The \texttt{mkdir} tool is conservative in the sense that any existing
5.300 -\texttt{IsaMakefile} etc.\ is left unchanged. Thus it is safe to invoke it
5.301 -multiple times, although later runs may not have the desired effect.
5.302 -
5.303 -Note that \texttt{mkdir} is unable to change \texttt{IsaMakefile}
5.304 -incrementally --- manual changes are required for multiple sub-sessions. On
5.305 -order to get an initial working session, the only editing needed is to add
5.306 -appropriate \texttt{use_thy} calls to the generated \texttt{ROOT.ML} file.
5.307 -
5.308 -
5.309 -\subsection*{Options}
5.310 -
5.311 -The \texttt{-I} option specifies an alternative to \texttt{IsaMakefile} for
5.312 -dependencies. Note that ``\texttt{-}'' refers to \emph{stdout}, i.e.\
5.313 -``\texttt{-I-}'' provides an easy way to peek at \texttt{mkdir}'s idea of
5.314 -\texttt{make} setup required for some particular of Isabelle session.
5.315 -
5.316 -\medskip The \texttt{-P} option includes a target for the parent
5.317 -\texttt{LOGIC} session in the generated \texttt{IsaMakefile}. The
5.318 -corresponding sources are assumed to be located within the Isabelle
5.319 -distribution.
5.320 -
5.321 -\medskip The \texttt{-b} option sets up the current directory as the base for
5.322 -a new session that provides an actual logic image, as opposed to one that only
5.323 -runs several theories based on an existing image. Note that in the latter
5.324 -case, everything except \texttt{IsaMakefile} would be placed into a separate
5.325 -directory \texttt{NAME}, rather than the current one. See
5.326 -\S\ref{sec:tool-usedir} for further information on \emph{build mode} vs.\
5.327 -\emph{example mode} of the \texttt{usedir} utility.
5.328 -
5.329 -\medskip The \texttt{-q} enables quiet mode, suppressing further notes on how
5.330 -to proceed.
5.331 -
5.332 -
5.333 -\subsection*{Examples}
5.334 -
5.335 -The standard setup of a single ``example session'' based on the default logic,
5.336 -with proper document generation is generated like this:
5.337 -\begin{ttbox}
5.338 -isatool mkdir Foo && isatool make
5.339 -\end{ttbox}
5.340 -\noindent The theory sources should be put into the \texttt{Foo} directory, and its
5.341 -\texttt{ROOT.ML} should be edited to load all required theories. Invoking
5.342 -\texttt{isatool make} again would run the whole session, generating browser
5.343 -information and the document automatically. The \texttt{IsaMakefile} is
5.344 -typically tuned manually later, e.g.\ adding source dependencies, or changing
5.345 -the options passed to \texttt{usedir}.
5.346 -
5.347 -\medskip Large projects may demand further sessions, potentially with separate
5.348 -logic images being created. This usually requires manual editing of the
5.349 -generated \texttt{IsaMakefile}, which is meant to cover all of the sub-session
5.350 -directories at the same time (this is the deeper reasong why
5.351 -\texttt{IsaMakefile} is not made part of the initial session directory created
5.352 -by \texttt{isatool mkdir}). See \texttt{src/HOL/IsaMakefile} of the Isabelle
5.353 -distribution for a full-blown example.
5.354 -
5.355 -
5.356 -\section{Running Isabelle sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir}
5.357 -
5.358 -The \tooldx{usedir} utility builds object-logic images, or runs example
5.359 -sessions based on existing logics. Its usage is:
5.360 -\begin{ttbox}
5.361 -
5.362 -Usage: usedir [OPTIONS] LOGIC NAME
5.363 -
5.364 - Options are:
5.365 - -C BOOL copy existing document directory to -D PATH (default true)
5.366 - -D PATH dump generated document sources into PATH
5.367 - -M MAX multithreading: maximum number of worker threads (default 1)
5.368 - -P PATH set path for remote theory browsing information
5.369 - -T LEVEL multithreading: trace level (default 0)
5.370 - -V VERSION declare alternative document VERSION
5.371 - -b build mode (output heap image, using current dir)
5.372 - -c BOOL tell ML system to compress output image (default true)
5.373 - -d FORMAT build document as FORMAT (default false)
5.374 - -f NAME use ML file NAME (default ROOT.ML)
5.375 - -g BOOL generate session graph image for document (default false)
5.376 - -i BOOL generate theory browser information (default false)
5.377 - -m MODE add print mode for output
5.378 - -p LEVEL set level of detail for proof objects
5.379 - -r reset session path
5.380 - -s NAME override session NAME
5.381 - -v BOOL be verbose (default false)
5.382 -
5.383 - Build object-logic or run examples. Also creates browsing
5.384 - information (HTML etc.) according to settings.
5.385 -
5.386 - ISABELLE_USEDIR_OPTIONS=
5.387 - HOL_USEDIR_OPTIONS=
5.388 -\end{ttbox}
5.389 -
5.390 -Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
5.391 -implicitly prefixed to \emph{any} \texttt{usedir} call. Since the
5.392 -\ttindex{IsaMakefile}s of all object-logics distributed with Isabelle just
5.393 -invoke \texttt{usedir} for the real work, one may control compilation options
5.394 -globally via above variable. In particular, generation of \rmindex{HTML}
5.395 -browsing information and document preparation is controlled here.
5.396 -
5.397 -The \settdx{HOL_USEDIR_OPTIONS} setting is specific to the main
5.398 -Isabelle/HOL image; its value is appended to
5.399 -\verb,ISABELLE_USEDIR_OPTIONS, for that particular session only.
5.400 -
5.401 -
5.402 -\subsection*{Options}
5.403 -
5.404 -Basically, there are two different modes of operation: \emph{build mode}
5.405 -(enabled through the \texttt{-b} option) and \emph{example mode} (default).
5.406 -
5.407 -Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with input
5.408 -image \texttt{LOGIC} and output to \texttt{NAME}, as provided on the command
5.409 -line. This will be a batch session, running \texttt{ROOT.ML} from the current
5.410 -directory and then quitting. It is assumed that \texttt{ROOT.ML} contains all
5.411 -{\ML} commands required to build the logic.
5.412 -
5.413 -In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC}
5.414 -and automatically runs \texttt{ROOT.ML} from within directory \texttt{NAME}.
5.415 -It assumes that this file contains appropriate {\ML} commands to run the
5.416 -desired examples.
5.417 -
5.418 -\medskip The \texttt{-i} option controls theory browser data generation. It
5.419 -may be explicitly turned on or off --- as usual, the last occurrence of
5.420 -\texttt{-i} on the command line wins.
5.421 -
5.422 -The \texttt{-P} option specifies a path (or actual URL) to be prefixed to any
5.423 -\emph{non-local} reference of existing theories. Thus user sessions may
5.424 -easily link to existing Isabelle libraries already present on the WWW.
5.425 -
5.426 -The \texttt{-m} options specifies additional print modes to be activated
5.427 -temporarily while the session is processed.
5.428 -
5.429 -\medskip The \texttt{-d} option controls document preparation. Valid
5.430 -arguments are \texttt{false} (do not prepare any document; this is default),
5.431 -or any of \texttt{dvi}, \texttt{dvi.gz}, \texttt{ps}, \texttt{ps.gz},
5.432 -\texttt{pdf}. The logic session has to provide a properly setup
5.433 -\texttt{document} directory. See \S\ref{sec:tool-document} and
5.434 -\S\ref{sec:tool-latex} for more details.
5.435 -
5.436 -\medskip The \texttt{-V} option declares alternative document versions,
5.437 -consisting of name/tags pairs (cf.\ options \texttt{-n} and \texttt{-t} of the
5.438 -\texttt{document} tool, \S\ref{sec:tool-document}). The standard document is
5.439 -equivalent to ``\texttt{document=theory,proof,ML}'', which means that all
5.440 -theory begin/end commands, proof body texts, and ML code will be presented
5.441 -faithfully. An alternative version ``\texttt{outline=/proof/ML}'' would fold
5.442 -proof and ML parts, replacing the original text by a short place-holder. The
5.443 -form ``$name$\verb,=-,'' means to remove document $name$ from the list of
5.444 -versions to be processed. Any number of \texttt{-V} options may be given;
5.445 -later declarations have precedence over earlier ones.
5.446 -
5.447 -\medskip The \texttt{-g} option produces images of the theory dependency graph
5.448 -(cf.\ \S\ref{sec:browse}) for inclusion in the generated document, both as
5.449 -\texttt{session_graph.eps} and \texttt{session_graph.pdf} at the same time.
5.450 -To include this in the final {\LaTeX} document one could say
5.451 -\verb,\includegraphics{session_graph}, in \texttt{document/root.tex} (omitting
5.452 -the file-name extension enables {\LaTeX} to select to correct version, either
5.453 -for the DVI or PDF output path).
5.454 -
5.455 -\medskip The \texttt{-D} option causes the generated document sources to be
5.456 -dumped at location \texttt{PATH}; this path is relative to the session's main
5.457 -directory. If the \texttt{-C} option is true, this will include a copy of an
5.458 -existing \texttt{document} directory as provided by the user. For example,
5.459 -\texttt{isatool usedir -D generated HOL Foo} produces a complete set of
5.460 -document sources at \texttt{Foo/generated}. Subsequent invocation of
5.461 -\texttt{isatool document Foo/generated} (see also \S\ref{sec:tool-document})
5.462 -will process the final result independently of an Isabelle job. This
5.463 -decoupled mode of operation facilitates debugging of serious {\LaTeX} errors,
5.464 -for example.
5.465 -
5.466 -\medskip The \texttt{-p} option determines the level of detail for internal
5.467 -proof objects, see also the \emph{Isabelle Reference
5.468 - Manual}~\cite{isabelle-ref}.
5.469 -
5.470 -\medskip The \texttt{-v} option causes additional information to be printed
5.471 -while running the session, notably the location of prepared documents.
5.472 -
5.473 -\medskip The \texttt{-M} option specifies the maximum number of
5.474 -parallel threads used for processing independent theory files
5.475 -(multithreading only works on suitable ML platforms). The special
5.476 -value of ``\texttt{0}'' or ``\texttt{max}'' refers to the number of
5.477 -actual CPU cores of the underlying machine, which is a good starting
5.478 -point for optimal performance tuning. The \texttt{-T} option
5.479 -determines the level of detail in tracing output concerning the
5.480 -internal locking and scheduling in multithreaded operation. This may
5.481 -be helpful in isolating performance bottle-necks, e.g.\ due to
5.482 -excessive wait states when locking critical code sections.
5.483 -
5.484 -\medskip Any \texttt{usedir} session is named by some \emph{session
5.485 - identifier}. These accumulate, documenting the way sessions depend on
5.486 -others. For example, consider \texttt{Pure/FOL/ex}, which refers to the
5.487 -examples of FOL, which in turn is built upon Pure.
5.488 -
5.489 -The current session's identifier is by default just the base name of the
5.490 -\texttt{LOGIC} argument (in build mode), or of the \texttt{NAME} argument (in
5.491 -example mode). This may be overridden explicitly via the \texttt{-s} option.
5.492 -
5.493 -
5.494 -\subsection*{Examples}
5.495 -
5.496 -Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
5.497 -object-logics as a model for your own developments. For example, see
5.498 -\texttt{src/FOL/IsaMakefile}. The Isabelle \texttt{mkdir} tool (see
5.499 -\S\ref{sec:tool-mkdir}) creates \texttt{IsaMakefile}s with proper invocation
5.500 -of \texttt{usedir} as well.
5.501 -
5.502 -
5.503 -\section{Preparing Isabelle session documents --- \texttt{isatool document}}
5.504 -\label{sec:tool-document}
5.505 -
5.506 -The \tooldx{document} utility prepares logic session documents, processing the
5.507 -sources both as provided by the user and generated by Isabelle. Its usage is:
5.508 -\begin{ttbox}
5.509 -Usage: document [OPTIONS] [DIR]
5.510 -
5.511 - Options are:
5.512 - -c cleanup -- be aggressive in removing old stuff
5.513 - -n NAME specify document name (default 'document')
5.514 - -o FORMAT specify output format: dvi (default), dvi.gz, ps,
5.515 - ps.gz, pdf
5.516 - -t TAGS specify tagged region markup
5.517 -
5.518 - Prepare the theory session document in DIR (default 'document')
5.519 - producing the specified output format.
5.520 -\end{ttbox}
5.521 -This tool is usually run automatically as part of the corresponding Isabelle
5.522 -batch process, provided document preparation has been enabled (cf.\ the
5.523 -\texttt{-d} option of the \texttt{usedir} utility, \S\ref{sec:tool-usedir}).
5.524 -It may be manually invoked on the generated browser information document
5.525 -output as well, e.g.\ in case of errors encountered in the batch run.
5.526 -
5.527 -\medskip The \texttt{-c} option tells the \texttt{document} tool to dispose
5.528 -the document sources after successful operation. This is the right thing to
5.529 -do for sources generated by an Isabelle process, but take care of your files
5.530 -in manual document preparation!
5.531 -
5.532 -\medskip The \texttt{-n} and \texttt{-o} option specify the final output file
5.533 -name and format, the default is ``\texttt{document.dvi}''. Note that the
5.534 -result will appear in the parent of the target \texttt{DIR}.
5.535 -
5.536 -\medskip The \texttt{-t} option tells {\LaTeX} how to interpret tagged
5.537 -Isabelle command regions. Tags are specified as a comma separated list of
5.538 -modifier/name pairs: ``\verb,+,$foo$'' (or just ``$foo$'') means to keep,
5.539 -``\verb,-,$foo$'' to drop, and ``\verb,/,$foo$'' to fold text tagged as $foo$.
5.540 -The builtin default is equivalent to the tag specification
5.541 -``\texttt{/theory,/proof,/ML,+visible,-invisible}''; see also the {\LaTeX}
5.542 -macros \verb,\isakeeptag,, \verb,\isadroptag,, and \verb,\isafoldtag, in
5.543 -\texttt{isabelle.sty}.
5.544 -
5.545 -\medskip Document preparation requires a properly setup ``\texttt{document}''
5.546 -directory within the logic session sources. This directory is supposed to
5.547 -contain all the files needed to produce the final document --- apart from the
5.548 -actual theories which are generated by Isabelle.
5.549 -
5.550 -\medskip For most practical purposes, the \texttt{document} tool is smart
5.551 -enough to create any of the specified output formats, taking \texttt{root.tex}
5.552 -supplied by the user as a starting point. This even includes multiple runs of
5.553 -{\LaTeX} to accommodate references and bibliographies (the latter assumes
5.554 -\texttt{root.bib} within the same directory).
5.555 -
5.556 -In more complex situations, a separate \texttt{IsaMakefile} for the document
5.557 -sources may be given instead. This should provide targets for any admissible
5.558 -document format; these have to produce corresponding output files named after
5.559 -\texttt{root} as well, e.g.\ \texttt{root.dvi} for target format \texttt{dvi}.
5.560 -
5.561 -\medskip When running the session, Isabelle copies the original
5.562 -\texttt{document} directory into its proper place within
5.563 -\texttt{ISABELLE_BROWSER_INFO} according to the session path. Then, for any
5.564 -processed theory $A$ some {\LaTeX} source is generated and put there as
5.565 -$A$\texttt{.tex}. Furthermore, a list of all generated theory files is put
5.566 -into \texttt{session.tex}. Typically, the root {\LaTeX} file provided by the
5.567 -user would include \texttt{session.tex} to get a document containing all the
5.568 -theories.
5.569 -
5.570 -The {\LaTeX} versions of the theories require some macros defined in
5.571 -\texttt{isabelle.sty} as distributed with Isabelle. Doing
5.572 -\verb,\usepackage{isabelle}, in \texttt{root.tex} should be fine; the
5.573 -underlying Isabelle \texttt{latex} utility already includes an appropriate
5.574 -{\TeX} inputs path.
5.575 -
5.576 -If the text contains any references to Isabelle symbols (such as
5.577 -\verb,\<forall>,) then \texttt{isabellesym.sty} should be included as well.
5.578 -This package contains a standard set of {\LaTeX} macro definitions
5.579 -\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>, (see
5.580 -Appendix~\ref{app:symbols} for a complete list of predefined Isabelle
5.581 -symbols). Users may invent further symbols as well, just by providing
5.582 -{\LaTeX} macros in a similar fashion as in \texttt{isabellesym.sty} of the
5.583 -distribution.
5.584 -
5.585 -For proper setup of PDF documents (with hyperlinks and bookmarks), we
5.586 -recommend to include \verb,pdfsetup.sty, as well. It is safe to do so
5.587 -even without using PDF~\LaTeX.
5.588 -
5.589 -\medskip As a final step of document preparation within Isabelle,
5.590 -\texttt{isatool document -c} is run on the resulting \texttt{document}
5.591 -directory. Thus the actual output document is built and installed in its
5.592 -proper place (as linked by the session's \texttt{index.html} if option
5.593 -\texttt{-i} of \texttt{usedir} has been enabled, cf.\ \S\ref{sec:info}). The
5.594 -generated sources are deleted after successful run of {\LaTeX} and friends.
5.595 -Note that a separate copy of the sources may be retained by passing an option
5.596 -\texttt{-D} to the \texttt{usedir} utility when running the session (see also
5.597 -\S\ref{sec:tool-usedir}).
5.598 -
5.599 -
5.600 -\section{Running {\LaTeX} within the Isabelle environment --- \texttt{isatool latex}}
5.601 -\label{sec:tool-latex}
5.602 -
5.603 -The \tooldx{latex} utility provides the basic interface for Isabelle document
5.604 -preparation. Its usage is:
5.605 -\begin{ttbox}
5.606 -Usage: latex [OPTIONS] [FILE]
5.607 -
5.608 - Options are:
5.609 - -o FORMAT specify output format: dvi (default), dvi.gz, ps,
5.610 - ps.gz, pdf, bbl, idx, sty, syms
5.611 -
5.612 - Run LaTeX (and related tools) on FILE (default root.tex),
5.613 - producing the specified output format.
5.614 -\end{ttbox}
5.615 -Appropriate {\LaTeX}-related programs are run on the input file,
5.616 -according to the given output format: \texttt{latex},
5.617 -\texttt{pdflatex}, \texttt{dvips}, \texttt{bibtex} (for \texttt{bbl}),
5.618 -and \texttt{makeindex} (for \texttt{idx}). The actual commands are
5.619 -determined from the settings environment (\texttt{ISABELLE_LATEX}
5.620 -etc., see \S\ref{sec:settings}).
5.621 -
5.622 -The \texttt{sty} output format causes the Isabelle style files to be updated
5.623 -from the distribution. This is useful in special situations where the
5.624 -document sources are to be processed another time by separate tools (cf.\
5.625 -option \texttt{-D} of the \texttt{usedir} utility, see
5.626 -\S\ref{sec:tool-usedir}).
5.627 -
5.628 -The \texttt{syms} output is for internal use; it generates lists of symbols
5.629 -that are available without loading additional {\LaTeX} packages.
5.630 -
5.631 -
5.632 -\subsubsection*{Examples}
5.633 -
5.634 -Invoking \texttt{isatool latex} by hand may be occasionally useful when
5.635 -debugging failed attempts of the automatic document preparation stage of
5.636 -batch-mode Isabelle. The abortive process leaves the sources at a certain
5.637 -place within \texttt{ISABELLE_BROWSER_INFO}, see the runtime error message for
5.638 -details. This enables users to inspect {\LaTeX} runs in further detail, e.g.\
5.639 -like this:
5.640 -
5.641 -\begin{ttbox}
5.642 - cd ~/isabelle/browser_info/HOL/Test/document
5.643 - isatool latex -o pdf
5.644 -\end{ttbox}
5.645 -
5.646 -
5.647 -%%% Local Variables:
5.648 -%%% mode: latex
5.649 -%%% TeX-master: "system"
5.650 -%%% End:
6.1 --- a/doc-src/System/system.tex Mon Sep 15 17:32:12 2008 +0200
6.2 +++ b/doc-src/System/system.tex Mon Sep 15 19:42:22 2008 +0200
6.3 @@ -26,7 +26,7 @@
6.4 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
6.5
6.6 \author{\emph{Makarius Wenzel} and \emph{Stefan Berghofer} \\
6.7 - TU M\"unchen}
6.8 + TU München}
6.9
6.10 \makeindex
6.11
6.12 @@ -37,7 +37,7 @@
6.13 \pagenumbering{roman} \tableofcontents \clearfirst
6.14
6.15 \input{Thy/document/Basics}
6.16 -\input{present}
6.17 +\input{Thy/document/Presentation}
6.18 \input{misc}
6.19
6.20 \appendix