doc-src/System/Thy/Presentation.thy
changeset 28221 ca9fdab0f971
child 28225 5d1fc22bccdf
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/System/Thy/Presentation.thy	Mon Sep 15 19:42:22 2008 +0200
     1.3 @@ -0,0 +1,759 @@
     1.4 +(* $Id$ *)
     1.5 +
     1.6 +theory Presentation
     1.7 +imports Pure
     1.8 +begin
     1.9 +
    1.10 +chapter {* Presenting theories \label{ch:present} *}
    1.11 +
    1.12 +text {*
    1.13 +  Isabelle provides several ways to present the outcome of formal
    1.14 +  developments, including WWW-based browsable libraries or actual
    1.15 +  printable documents.  Presentation is centered around the concept of
    1.16 +  \emph{logic sessions}.  The global session structure is that of a
    1.17 +  tree, with Isabelle Pure at its root, further object-logics derived
    1.18 +  (e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions
    1.19 +  in leaf positions (usually without a separate image).
    1.20 +
    1.21 +  The Isabelle tools @{tool_ref mkdir} and @{tool_ref make} provide
    1.22 +  the primary means for managing Isabelle sessions, including proper
    1.23 +  setup for presentation.  Here the @{tool_ref usedir} tool takes care
    1.24 +  to let @{executable_ref "isabelle-process"} process run any
    1.25 +  additional stages required for document preparation, notably the
    1.26 +  tools @{tool_ref document} and @{tool_ref latex}.  The complete tool
    1.27 +  chain for managing batch-mode Isabelle sessions is illustrated in
    1.28 +  \figref{fig:session-tools}.
    1.29 +
    1.30 +  \begin{figure}[htbp]
    1.31 +  \begin{center}
    1.32 +  \begin{tabular}{lp{0.6\textwidth}}
    1.33 +
    1.34 +      @{verbatim "isatool mkdir"} & invoked once by the user to create
    1.35 +      the initial source setup (common @{verbatim IsaMakefile} plus a
    1.36 +      single session directory); \\
    1.37 +
    1.38 +      @{verbatim "isatool make"} & invoked repeatedly by the user to
    1.39 +      keep session output up-to-date (HTML, documents etc.); \\
    1.40 +
    1.41 +      @{verbatim "isatool usedir"} & part of the standard @{verbatim
    1.42 +      IsaMakefile} entry of a session; \\
    1.43 +
    1.44 +      @{verbatim "isabelle-process"} & run through @{verbatim "isatool
    1.45 +      usedir"}; \\
    1.46 +
    1.47 +      @{verbatim "isatool document"} & run by the Isabelle process if
    1.48 +      document preparation is enabled; \\
    1.49 +
    1.50 +      @{verbatim "isatool latex"} & universal {\LaTeX} tool wrapper
    1.51 +      invoked multiple times by @{verbatim "isatool document"}; also
    1.52 +      useful for manual experiments; \\
    1.53 +
    1.54 +  \end{tabular}
    1.55 +  \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
    1.56 +  \end{center}
    1.57 +  \end{figure}
    1.58 +*}
    1.59 +
    1.60 +
    1.61 +section {* Generating theory browser information \label{sec:info} *}
    1.62 +
    1.63 +text {*
    1.64 +  \index{theory browsing information|bold}
    1.65 +
    1.66 +  As a side-effect of running a logic sessions, Isabelle is able to
    1.67 +  generate theory browsing information, including HTML documents that
    1.68 +  show a theory's definition, the theorems proved in its ML file and
    1.69 +  the relationship with its ancestors and descendants.  Besides the
    1.70 +  HTML file that is generated for every theory, Isabelle stores links
    1.71 +  to all theories in an index file. These indexes are linked with
    1.72 +  other indexes to represent the overall tree structure of logic
    1.73 +  sessions.
    1.74 +
    1.75 +  Isabelle also generates graph files that represent the theory
    1.76 +  hierarchy of a logic.  There is a graph browser Java applet embedded
    1.77 +  in the generated HTML pages, and also a stand-alone application that
    1.78 +  allows browsing theory graphs without having to start a WWW client
    1.79 +  first.  The latter version also includes features such as generating
    1.80 +  Postscript files, which are not available in the applet version.
    1.81 +  See \secref{sec:browse} for further information.
    1.82 +
    1.83 +  \medskip
    1.84 +
    1.85 +  The easiest way to let Isabelle generate theory browsing information
    1.86 +  for existing sessions is to append ``@{verbatim "-i true"}'' to the
    1.87 +  @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim
    1.88 +  "isatool make"} (or @{verbatim "./build"} in the distribution).  For
    1.89 +  example, add something like this to your Isabelle settings file
    1.90 +
    1.91 +\begin{ttbox}
    1.92 +ISABELLE_USEDIR_OPTIONS="-i true"
    1.93 +\end{ttbox}
    1.94 +
    1.95 +  and then change into the @{verbatim "src/FOL"} directory of the
    1.96 +  Isabelle distribution and run @{verbatim "isatool make"}, or even
    1.97 +  @{verbatim "isatool make all"}.  The presentation output will appear
    1.98 +  in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
    1.99 +  @{verbatim "~/isabelle/browser_info/FOL"}.  Note that option
   1.100 +  @{verbatim "-v true"} will make the internal runs of @{tool usedir}
   1.101 +  more explicit about such details.
   1.102 +
   1.103 +  Many standard Isabelle sessions (such as @{verbatim "HOL/ex"}) also
   1.104 +  provide actual printable documents.  These are prepared
   1.105 +  automatically as well if enabled like this, using the @{verbatim
   1.106 +  "-d"} option
   1.107 +\begin{ttbox}
   1.108 +ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
   1.109 +\end{ttbox}
   1.110 +  Enabling options @{verbatim "-i"} and @{verbatim "-d"}
   1.111 +  simultaneausly as shown above causes an appropriate ``document''
   1.112 +  link to be included in the HTML index.  Documents (or raw document
   1.113 +  sources) may be generated independently of browser information as
   1.114 +  well, see \secref{sec:tool-document} for further details.
   1.115 +
   1.116 +  \bigskip The theory browsing information is stored in a
   1.117 +  sub-directory directory determined by the @{setting_ref
   1.118 +  ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the
   1.119 +  session identifier (according to the tree structure of sub-sessions
   1.120 +  by default).  A complete WWW view of all standard object-logics and
   1.121 +  examples of the Isabelle distribution is available at the Cambridge
   1.122 +  or Munich Isabelle sites:
   1.123 +  \begin{center}\small
   1.124 +  \begin{tabular}{l}
   1.125 +    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
   1.126 +    \url{http://isabelle.in.tum.de/library/} \\
   1.127 +  \end{tabular}
   1.128 +  \end{center}
   1.129 +  
   1.130 +  \medskip In order to present your own theories on the web, simply
   1.131 +  copy the corresponding subdirectory from @{setting
   1.132 +  ISABELLE_BROWSER_INFO} to your WWW server, having generated browser
   1.133 +  info like this:
   1.134 +\begin{ttbox}
   1.135 +isatool usedir -i true HOL Foo
   1.136 +\end{ttbox}
   1.137 +
   1.138 +  This assumes that directory @{verbatim Foo} contains some @{verbatim
   1.139 +  ROOT.ML} file to load all your theories, and HOL is your parent
   1.140 +  logic image (@{verbatim isatool}~@{tool_ref mkdir} assists in
   1.141 +  setting up Isabelle session directories.  Theory browser information
   1.142 +  for HOL should have been generated already beforehand.
   1.143 +  Alternatively, one may specify an external link to an existing body
   1.144 +  of HTML data by giving @{tool usedir} a @{verbatim "-P"} option like
   1.145 +  this:
   1.146 +\begin{ttbox}
   1.147 +isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
   1.148 +\end{ttbox}
   1.149 +
   1.150 +  \medskip For production use, the @{tool usedir} tool is usually
   1.151 +  invoked in an appropriate @{verbatim IsaMakefile}, via the Isabelle
   1.152 +  @{tool make} tool.  There is a separate @{tool mkdir} tool to
   1.153 +  provide easy setup of all this, with only minimal manual editing
   1.154 +  required.
   1.155 +\begin{ttbox}
   1.156 +isatool mkdir HOL Foo && isatool make
   1.157 +\end{ttbox}
   1.158 +  See \secref{sec:tool-mkdir} for more information on preparing
   1.159 +  Isabelle session directories, including the setup for documents.
   1.160 +*}
   1.161 +
   1.162 +
   1.163 +section {* Browsing theory graphs \label{sec:browse} *}
   1.164 +
   1.165 +text {*
   1.166 +  \index{theory graph browser|bold} 
   1.167 +
   1.168 +  The Isabelle graph browser is a general tool for visualizing
   1.169 +  dependency graphs.  Certain nodes of the graph (i.e.~theories) can
   1.170 +  be grouped together in ``directories'', whose contents may be
   1.171 +  hidden, thus enabling the user to collapse irrelevant portions of
   1.172 +  information.  The browser is written in Java, it can be used both as
   1.173 +  a stand-alone application and as an applet.  Note that the option
   1.174 +  @{verbatim "-g"} of @{verbatim isatool}~@{tool_ref usedir} creates
   1.175 +  graph presentations in batch mode for inclusion in session
   1.176 +  documents.
   1.177 +*}
   1.178 +
   1.179 +
   1.180 +subsection {* Invoking the graph browser *}
   1.181 +
   1.182 +text {*
   1.183 +  The stand-alone version of the graph browser is wrapped up as an
   1.184 +  Isabelle tool called @{tool_def browser}:
   1.185 +
   1.186 +\begin{ttbox}
   1.187 +Usage: browser [OPTIONS] [GRAPHFILE]
   1.188 +
   1.189 +  Options are:
   1.190 +    -c           cleanup -- remove GRAPHFILE after use
   1.191 +    -o FILE      output to FILE (ps, eps, pdf)
   1.192 +\end{ttbox}
   1.193 +  When no filename is specified, the browser automatically changes to
   1.194 +  the directory @{setting ISABELLE_BROWSER_INFO}.
   1.195 +
   1.196 +  \medskip The @{verbatim "-c"} option causes the input file to be
   1.197 +  removed after use.
   1.198 +
   1.199 +  The @{verbatim "-o"} option indicates batch-mode operation, with the
   1.200 +  output written to the indicated file; note that @{verbatim pdf}
   1.201 +  produces an @{verbatim eps} copy as well.
   1.202 +
   1.203 +  \medskip The applet version of the browser is part of the standard
   1.204 +  WWW theory presentation, see the link ``theory dependencies'' within
   1.205 +  each session index.
   1.206 +*}
   1.207 +
   1.208 +
   1.209 +subsection {* Using the graph browser *}
   1.210 +
   1.211 +text {*
   1.212 +  The browser's main window, which is shown in
   1.213 +  \figref{fig:browserwindow}, consists of two sub-windows.  In the
   1.214 +  left sub-window, the directory tree is displayed. The graph itself
   1.215 +  is displayed in the right sub-window.
   1.216 +
   1.217 +  \begin{figure}[ht]
   1.218 +  \includegraphics[width=\textwidth]{browser_screenshot}
   1.219 +  \caption{\label{fig:browserwindow} Browser main window}
   1.220 +  \end{figure}
   1.221 +*}
   1.222 +
   1.223 +
   1.224 +subsubsection {* The directory tree window *}
   1.225 +
   1.226 +text {*
   1.227 +  We describe the usage of the directory browser and the meaning of
   1.228 +  the different items in the browser window.
   1.229 +
   1.230 +  \begin{itemize}
   1.231 +  
   1.232 +  \item A red arrow before a directory name indicates that the
   1.233 +  directory is currently ``folded'', i.e.~the nodes in this directory
   1.234 +  are collapsed to one single node. In the right sub-window, the names
   1.235 +  of nodes corresponding to folded directories are enclosed in square
   1.236 +  brackets and displayed in red color.
   1.237 +  
   1.238 +  \item A green downward arrow before a directory name indicates that
   1.239 +  the directory is currently ``unfolded''. It can be folded by
   1.240 +  clicking on the directory name.  Clicking on the name for a second
   1.241 +  time unfolds the directory again.  Alternatively, a directory can
   1.242 +  also be unfolded by clicking on the corresponding node in the right
   1.243 +  sub-window.
   1.244 +  
   1.245 +  \item Blue arrows stand before ordinary node names. When clicking on
   1.246 +  such a name (i.e.\ that of a theory), the graph display window
   1.247 +  focuses to the corresponding node. Double clicking invokes a text
   1.248 +  viewer window in which the contents of the theory file are
   1.249 +  displayed.
   1.250 +
   1.251 +  \end{itemize}
   1.252 +*}
   1.253 +
   1.254 +
   1.255 +subsubsection {* The graph display window *}
   1.256 +
   1.257 +text {*
   1.258 +  When pointing on an ordinary node, an upward and a downward arrow is
   1.259 +  shown.  Initially, both of these arrows are green. Clicking on the
   1.260 +  upward or downward arrow collapses all predecessor or successor
   1.261 +  nodes, respectively. The arrow's color then changes to red,
   1.262 +  indicating that the predecessor or successor nodes are currently
   1.263 +  collapsed. The node corresponding to the collapsed nodes has the
   1.264 +  name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply
   1.265 +  click on the red arrow or on the node with the name ``@{verbatim
   1.266 +  "[....]"}''. Similar to the directory browser, the contents of
   1.267 +  theory files can be displayed by double clicking on the
   1.268 +  corresponding node.
   1.269 +*}
   1.270 +
   1.271 +
   1.272 +subsubsection {* The ``File'' menu *}
   1.273 +
   1.274 +text {*
   1.275 +  Due to Java Applet security restrictions this menu is only available
   1.276 +  in the full application version. The meaning of the menu items is as
   1.277 +  follows:
   1.278 +
   1.279 +  \begin{description}
   1.280 +  
   1.281 +  \item[Open \dots] Open a new graph file.
   1.282 +  
   1.283 +  \item[Export to PostScript] Outputs the current graph in Postscript
   1.284 +  format, appropriately scaled to fit on one single sheet of A4 paper.
   1.285 +  The resulting file can be printed directly.
   1.286 +  
   1.287 +  \item[Export to EPS] Outputs the current graph in Encapsulated
   1.288 +  Postscript format. The resulting file can be included in other
   1.289 +  documents.
   1.290 +
   1.291 +  \item[Quit] Quit the graph browser.
   1.292 +
   1.293 +  \end{description}
   1.294 +*}
   1.295 +
   1.296 +
   1.297 +subsection {* Syntax of graph definition files *}
   1.298 +
   1.299 +text {*
   1.300 +  A graph definition file has the following syntax:
   1.301 +
   1.302 +  \begin{tabular}{rcl}
   1.303 +    @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\
   1.304 +    @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"}
   1.305 +  \end{tabular}
   1.306 +
   1.307 +  The meaning of the items in a vertex description is as follows:
   1.308 +
   1.309 +  \begin{description}
   1.310 +  
   1.311 +  \item[@{text vertex_name}] The name of the vertex.
   1.312 +  
   1.313 +  \item[@{text vertex_ID}] The vertex identifier. Note that there may
   1.314 +  be several vertices with equal names, whereas identifiers must be
   1.315 +  unique.
   1.316 +  
   1.317 +  \item[@{text dir_name}] The name of the ``directory'' the vertex
   1.318 +  should be placed in.  A ``@{verbatim "+"}'' sign after @{text
   1.319 +  dir_name} indicates that the nodes in the directory are initially
   1.320 +  visible. Directories are initially invisible by default.
   1.321 +  
   1.322 +  \item[@{text path}] The path of the corresponding theory file. This
   1.323 +  is specified relatively to the path of the graph definition file.
   1.324 +  
   1.325 +  \item[List of successor/predecessor nodes] A ``@{verbatim "<"}''
   1.326 +  sign before the list means that successor nodes are listed, a
   1.327 +  ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
   1.328 +  neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
   1.329 +  browser assumes that successor nodes are listed.
   1.330 +
   1.331 +  \end{description}
   1.332 +*}
   1.333 +
   1.334 +
   1.335 +section {* Creating Isabelle session directories
   1.336 +  \label{sec:tool-mkdir} *}
   1.337 +
   1.338 +text {*
   1.339 +  The @{tool_def mkdir} utility prepares Isabelle session source
   1.340 +  directories, including a sensible default setup of @{verbatim
   1.341 +  IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document}
   1.342 +  directory with a minimal @{verbatim root.tex} that is sufficient to
   1.343 +  print all theories of the session (in the order of appearance); see
   1.344 +  \secref{sec:tool-document} for further information on Isabelle
   1.345 +  document preparation.  The usage of @{verbatim "isatool mkdir"} is:
   1.346 +
   1.347 +\begin{ttbox}
   1.348 +Usage: mkdir [OPTIONS] [LOGIC] NAME
   1.349 +
   1.350 +  Options are:
   1.351 +    -I FILE      alternative IsaMakefile output
   1.352 +    -P           include parent logic target
   1.353 +    -b           setup build mode (session outputs heap image)
   1.354 +    -q           quiet mode
   1.355 +
   1.356 +  Prepare session directory, including IsaMakefile and document source,
   1.357 +  with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
   1.358 +\end{ttbox}
   1.359 +
   1.360 +  The @{tool mkdir} tool is conservative in the sense that any
   1.361 +  existing @{verbatim IsaMakefile} etc.\ is left unchanged.  Thus it
   1.362 +  is safe to invoke it multiple times, although later runs may not
   1.363 +  have the desired effect.
   1.364 +
   1.365 +  Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile}
   1.366 +  incrementally --- manual changes are required for multiple
   1.367 +  sub-sessions.  On order to get an initial working session, the only
   1.368 +  editing needed is to add appropriate @{ML use_thy} calls to the
   1.369 +  generated @{verbatim ROOT.ML} file.
   1.370 +*}
   1.371 +
   1.372 +
   1.373 +subsubsection {* Options *}
   1.374 +
   1.375 +text {*
   1.376 +  The @{verbatim "-I"} option specifies an alternative to @{verbatim
   1.377 +  IsaMakefile} for dependencies.  Note that ``@{verbatim "-"}'' refers
   1.378 +  to \emph{stdout}, i.e.\ ``@{verbatim "-I-"}'' provides an easy way
   1.379 +  to peek at @{tool mkdir}'s idea of @{tool make} setup required for
   1.380 +  some particular of Isabelle session.
   1.381 +
   1.382 +  \medskip The @{verbatim "-P"} option includes a target for the
   1.383 +  parent @{verbatim LOGIC} session in the generated @{verbatim
   1.384 +  IsaMakefile}.  The corresponding sources are assumed to be located
   1.385 +  within the Isabelle distribution.
   1.386 +
   1.387 +  \medskip The @{verbatim "-b"} option sets up the current directory
   1.388 +  as the base for a new session that provides an actual logic image,
   1.389 +  as opposed to one that only runs several theories based on an
   1.390 +  existing image.  Note that in the latter case, everything except
   1.391 +  @{verbatim IsaMakefile} would be placed into a separate directory
   1.392 +  @{verbatim NAME}, rather than the current one.  See
   1.393 +  \secref{sec:tool-usedir} for further information on \emph{build
   1.394 +  mode} vs.\ \emph{example mode} of the @{tool usedir} utility.
   1.395 +
   1.396 +  \medskip The @{verbatim "-q"} option enables quiet mode, suppressing
   1.397 +  further notes on how to proceed.
   1.398 +*}
   1.399 +
   1.400 +
   1.401 +subsubsection {* Examples *}
   1.402 +
   1.403 +text {*
   1.404 +  The standard setup of a single ``example session'' based on the
   1.405 +  default logic, with proper document generation is generated like
   1.406 +  this:
   1.407 +\begin{ttbox}
   1.408 +isatool mkdir Foo && isatool make
   1.409 +\end{ttbox}
   1.410 +
   1.411 +  \noindent The theory sources should be put into the @{verbatim Foo}
   1.412 +  directory, and its @{verbatim ROOT.ML} should be edited to load all
   1.413 +  required theories.  Invoking @{verbatim "isatool make"} again would
   1.414 +  run the whole session, generating browser information and the
   1.415 +  document automatically.  The @{verbatim IsaMakefile} is typically
   1.416 +  tuned manually later, e.g.\ adding source dependencies, or changing
   1.417 +  the options passed to @{tool usedir}.
   1.418 +
   1.419 +  \medskip Large projects may demand further sessions, potentially
   1.420 +  with separate logic images being created.  This usually requires
   1.421 +  manual editing of the generated @{verbatim IsaMakefile}, which is
   1.422 +  meant to cover all of the sub-session directories at the same time
   1.423 +  (this is the deeper reasong why @{verbatim IsaMakefile} is not made
   1.424 +  part of the initial session directory created by @{verbatim "isatool
   1.425 +  mkdir"}).  See @{verbatim "src/HOL/IsaMakefile"} of the Isabelle
   1.426 +  distribution for a full-blown example.
   1.427 +*}
   1.428 +
   1.429 +
   1.430 +section {* Running Isabelle sessions \label{sec:tool-usedir} *}
   1.431 +
   1.432 +text {*
   1.433 +  The @{tool_def usedir} utility builds object-logic images, or runs
   1.434 +  example sessions based on existing logics. Its usage is:
   1.435 +\begin{ttbox}
   1.436 +
   1.437 +Usage: usedir [OPTIONS] LOGIC NAME
   1.438 +
   1.439 +  Options are:
   1.440 +    -C BOOL      copy existing document directory to -D PATH (default true)
   1.441 +    -D PATH      dump generated document sources into PATH
   1.442 +    -M MAX       multithreading: maximum number of worker threads (default 1)
   1.443 +    -P PATH      set path for remote theory browsing information
   1.444 +    -T LEVEL     multithreading: trace level (default 0)
   1.445 +    -V VERSION   declare alternative document VERSION
   1.446 +    -b           build mode (output heap image, using current dir)
   1.447 +    -c BOOL      tell ML system to compress output image (default true)
   1.448 +    -d FORMAT    build document as FORMAT (default false)
   1.449 +    -f NAME      use ML file NAME (default ROOT.ML)
   1.450 +    -g BOOL      generate session graph image for document (default false)
   1.451 +    -i BOOL      generate theory browser information (default false)
   1.452 +    -m MODE      add print mode for output
   1.453 +    -p LEVEL     set level of detail for proof objects
   1.454 +    -r           reset session path
   1.455 +    -s NAME      override session NAME
   1.456 +    -v BOOL      be verbose (default false)
   1.457 +
   1.458 +  Build object-logic or run examples. Also creates browsing
   1.459 +  information (HTML etc.) according to settings.
   1.460 +
   1.461 +  ISABELLE_USEDIR_OPTIONS=
   1.462 +  HOL_USEDIR_OPTIONS=
   1.463 +\end{ttbox}
   1.464 +
   1.465 +  Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
   1.466 +  setting is implicitly prefixed to \emph{any} @{tool usedir}
   1.467 +  call. Since the @{verbatim IsaMakefile}s of all object-logics
   1.468 +  distributed with Isabelle just invoke \texttt{usedir} for the real
   1.469 +  work, one may control compilation options globally via above
   1.470 +  variable. In particular, generation of \rmindex{HTML} browsing
   1.471 +  information and document preparation is controlled here.
   1.472 +
   1.473 +  The @{setting_ref HOL_USEDIR_OPTIONS} setting is specific to the
   1.474 +  plain and main Isabelle/HOL images; its value is appended to
   1.475 +  @{setting ISABELLE_USEDIR_OPTIONS} for these particular sessions
   1.476 +  only.
   1.477 +*}
   1.478 +
   1.479 +
   1.480 +subsubsection {* Options *}
   1.481 +
   1.482 +text {*
   1.483 +  Basically, there are two different modes of operation: \emph{build
   1.484 +  mode} (enabled through the @{verbatim "-b"} option) and
   1.485 +  \emph{example mode} (default).
   1.486 +
   1.487 +  Calling @{tool usedir} with @{verbatim "-b"} runs @{executable
   1.488 +  "isabelle-process"} with input image @{verbatim LOGIC} and output to
   1.489 +  @{verbatim NAME}, as provided on the command line. This will be a
   1.490 +  batch session, running @{verbatim ROOT.ML} from the current
   1.491 +  directory and then quitting.  It is assumed that @{verbatim ROOT.ML}
   1.492 +  contains all ML commands required to build the logic.
   1.493 +
   1.494 +  In example mode, @{verbatim usedir} runs a read-only session of
   1.495 +  @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from
   1.496 +  within directory @{verbatim NAME}.  It assumes that this file
   1.497 +  contains appropriate ML commands to run the desired examples.
   1.498 +
   1.499 +  \medskip The @{verbatim "-i"} option controls theory browser data
   1.500 +  generation. It may be explicitly turned on or off --- as usual, the
   1.501 +  last occurrence of @{verbatim "-i"} on the command line wins.
   1.502 +
   1.503 +  The @{verbatim "-P"} option specifies a path (or actual URL) to be
   1.504 +  prefixed to any \emph{non-local} reference of existing theories.
   1.505 +  Thus user sessions may easily link to existing Isabelle libraries
   1.506 +  already present on the WWW.
   1.507 +
   1.508 +  The @{verbatim "-m"} options specifies additional print modes to be
   1.509 +  activated temporarily while the session is processed.
   1.510 +
   1.511 +  \medskip The @{verbatim "-d"} option controls document preparation.
   1.512 +  Valid arguments are @{verbatim false} (do not prepare any document;
   1.513 +  this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz},
   1.514 +  @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}.  The logic
   1.515 +  session has to provide a properly setup @{verbatim document}
   1.516 +  directory.  See \secref{sec:tool-document} and
   1.517 +  \secref{sec:tool-latex} for more details.
   1.518 +
   1.519 +  \medskip The @{verbatim "-V"} option declares alternative document
   1.520 +  versions, consisting of name/tags pairs (cf.\ options @{verbatim
   1.521 +  "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool).  The
   1.522 +  standard document is equivalent to ``@{verbatim
   1.523 +  "document=theory,proof,ML"}'', which means that all theory begin/end
   1.524 +  commands, proof body texts, and ML code will be presented
   1.525 +  faithfully.  An alternative version ``@{verbatim
   1.526 +  "outline=/proof/ML"}'' would fold proof and ML parts, replacing the
   1.527 +  original text by a short place-holder.  The form ``@{text
   1.528 +  name}@{verbatim "=-"},'' means to remove document @{text name} from
   1.529 +  the list of versions to be processed.  Any number of @{verbatim
   1.530 +  "-V"} options may be given; later declarations have precedence over
   1.531 +  earlier ones.
   1.532 +
   1.533 +  \medskip The @{verbatim "-g"} option produces images of the theory
   1.534 +  dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
   1.535 +  generated document, both as @{verbatim session_graph.eps} and
   1.536 +  @{verbatim session_graph.pdf} at the same time.  To include this in
   1.537 +  the final {\LaTeX} document one could say @{verbatim
   1.538 +  "\\includegraphics{session_graph}"} in @{verbatim
   1.539 +  "document/root.tex"} (omitting the file-name extension enables
   1.540 +  {\LaTeX} to select to correct version, either for the DVI or PDF
   1.541 +  output path).
   1.542 +
   1.543 +  \medskip The @{verbatim "-D"} option causes the generated document
   1.544 +  sources to be dumped at location @{verbatim PATH}; this path is
   1.545 +  relative to the session's main directory.  If the @{verbatim "-C"}
   1.546 +  option is true, this will include a copy of an existing @{verbatim
   1.547 +  document} directory as provided by the user.  For example,
   1.548 +  @{verbatim "isatool usedir -D generated HOL Foo"} produces a
   1.549 +  complete set of document sources at @{verbatim "Foo/generated"}.
   1.550 +  Subsequent invocation of @{verbatim "isatool document
   1.551 +  Foo/generated"} (see also \secref{sec:tool-document}) will process
   1.552 +  the final result independently of an Isabelle job.  This decoupled
   1.553 +  mode of operation facilitates debugging of serious {\LaTeX} errors,
   1.554 +  for example.
   1.555 +
   1.556 +  \medskip The @{verbatim "-p"} option determines the level of detail
   1.557 +  for internal proof objects, see also the \emph{Isabelle Reference
   1.558 +  Manual}~\cite{isabelle-ref}.
   1.559 +
   1.560 +  \medskip The @{verbatim "-v"} option causes additional information
   1.561 +  to be printed while running the session, notably the location of
   1.562 +  prepared documents.
   1.563 +
   1.564 +  \medskip The @{verbatim "-M"} option specifies the maximum number of
   1.565 +  parallel threads used for processing independent tasks when checking
   1.566 +  theory sources (multithreading only works on suitable ML platforms).
   1.567 +  The special value of ``@{verbatim 0}'' or ``@{verbatim max}'' refers
   1.568 +  to the number of actual CPU cores of the underlying machine, which
   1.569 +  is a good starting point for optimal performance tuning.  The
   1.570 +  @{verbatim "-T"} option determines the level of detail in tracing
   1.571 +  output concerning the internal locking and scheduling in
   1.572 +  multithreaded operation.  This may be helpful in isolating
   1.573 +  performance bottle-necks, e.g.\ due to excessive wait states when
   1.574 +  locking critical code sections.
   1.575 +
   1.576 +  \medskip Any @{tool usedir} session is named by some \emph{session
   1.577 +  identifier}. These accumulate, documenting the way sessions depend
   1.578 +  on others. For example, consider @{verbatim "Pure/FOL/ex"}, which
   1.579 +  refers to the examples of FOL, which in turn is built upon Pure.
   1.580 +
   1.581 +  The current session's identifier is by default just the base name of
   1.582 +  the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim
   1.583 +  NAME} argument (in example mode). This may be overridden explicitly
   1.584 +  via the @{verbatim "-s"} option.
   1.585 +*}
   1.586 +
   1.587 +
   1.588 +subsubsection {* Examples *}
   1.589 +
   1.590 +text {*
   1.591 +  Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's
   1.592 +  object-logics as a model for your own developments.  For example,
   1.593 +  see @{verbatim "src/FOL/IsaMakefile"}.  The Isabelle @{tool_ref
   1.594 +  mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation
   1.595 +  of @{tool usedir} as well.
   1.596 +*}
   1.597 +
   1.598 +
   1.599 +section {* Preparing Isabelle session documents
   1.600 +  \label{sec:tool-document} *}
   1.601 +
   1.602 +text {*
   1.603 +  The @{tool_def document} utility prepares logic session documents,
   1.604 +  processing the sources both as provided by the user and generated by
   1.605 +  Isabelle.  Its usage is:
   1.606 +\begin{ttbox}
   1.607 +Usage: document [OPTIONS] [DIR]
   1.608 +
   1.609 +  Options are:
   1.610 +    -c           cleanup -- be aggressive in removing old stuff
   1.611 +    -n NAME      specify document name (default 'document')
   1.612 +    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
   1.613 +                 ps.gz, pdf
   1.614 +    -t TAGS      specify tagged region markup
   1.615 +
   1.616 +  Prepare the theory session document in DIR (default 'document')
   1.617 +  producing the specified output format.
   1.618 +\end{ttbox}
   1.619 +  This tool is usually run automatically as part of the corresponding
   1.620 +  Isabelle batch process, provided document preparation has been
   1.621 +  enabled (cf.\ the @{verbatim "-d"} option of the @{tool_ref usedir}
   1.622 +  tool).  It may be manually invoked on the generated browser
   1.623 +  information document output as well, e.g.\ in case of errors
   1.624 +  encountered in the batch run.
   1.625 +
   1.626 +  \medskip The @{verbatim "-c"} option tells the @{tool document} tool
   1.627 +  to dispose the document sources after successful operation.  This is
   1.628 +  the right thing to do for sources generated by an Isabelle process,
   1.629 +  but take care of your files in manual document preparation!
   1.630 +
   1.631 +  \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify
   1.632 +  the final output file name and format, the default is ``@{verbatim
   1.633 +  document.dvi}''.  Note that the result will appear in the parent of
   1.634 +  the target @{verbatim DIR}.
   1.635 +
   1.636 +  \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret
   1.637 +  tagged Isabelle command regions.  Tags are specified as a comma
   1.638 +  separated list of modifier/name pairs: ``@{verbatim "+"}@{text
   1.639 +  foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim
   1.640 +  "-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to
   1.641 +  fold text tagged as @{text foo}.  The builtin default is equivalent
   1.642 +  to the tag specification ``@{verbatim
   1.643 +  "/theory,/proof,/ML,+visible,-invisible"}''; see also the {\LaTeX}
   1.644 +  macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
   1.645 +  @{verbatim "\\isafoldtag"}, in @{verbatim isabelle.sty}.
   1.646 +
   1.647 +  \medskip Document preparation requires a properly setup ``@{verbatim
   1.648 +  document}'' directory within the logic session sources.  This
   1.649 +  directory is supposed to contain all the files needed to produce the
   1.650 +  final document --- apart from the actual theories which are
   1.651 +  generated by Isabelle.
   1.652 +
   1.653 +  \medskip For most practical purposes, the @{tool document} tool is
   1.654 +  smart enough to create any of the specified output formats, taking
   1.655 +  @{verbatim root.tex} supplied by the user as a starting point.  This
   1.656 +  even includes multiple runs of {\LaTeX} to accommodate references
   1.657 +  and bibliographies (the latter assumes @{verbatim root.bib} within
   1.658 +  the same directory).
   1.659 +
   1.660 +  In more complex situations, a separate @{verbatim IsaMakefile} for
   1.661 +  the document sources may be given instead.  This should provide
   1.662 +  targets for any admissible document format; these have to produce
   1.663 +  corresponding output files named after @{verbatim root} as well,
   1.664 +  e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}.
   1.665 +
   1.666 +  \medskip When running the session, Isabelle copies the original
   1.667 +  @{verbatim document} directory into its proper place within
   1.668 +  @{verbatim ISABELLE_BROWSER_INFO} according to the session path.
   1.669 +  Then, for any processed theory @{text A} some {\LaTeX} source is
   1.670 +  generated and put there as @{text A}@{verbatim ".tex"}.
   1.671 +  Furthermore, a list of all generated theory files is put into
   1.672 +  @{verbatim session.tex}.  Typically, the root {\LaTeX} file provided
   1.673 +  by the user would include @{verbatim session.tex} to get a document
   1.674 +  containing all the theories.
   1.675 +
   1.676 +  The {\LaTeX} versions of the theories require some macros defined in
   1.677 +  @{verbatim isabelle.sty} as distributed with Isabelle.  Doing
   1.678 +  @{verbatim "\\usepackage{isabelle}"} in @{verbatim root.tex} should
   1.679 +  be fine; the underlying Isabelle @{tool latex} tool already includes
   1.680 +  an appropriate path specification for {\TeX} inputs.
   1.681 +
   1.682 +  If the text contains any references to Isabelle symbols (such as
   1.683 +  @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim
   1.684 +  isabellesym.sty} should be included as well.  This package contains
   1.685 +  a standard set of {\LaTeX} macro definitions @{verbatim
   1.686 +  "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
   1.687 +  "<"}@{text foo}@{verbatim ">"}, (see \appref{app:symbols} for a
   1.688 +  complete list of predefined Isabelle symbols).  Users may invent
   1.689 +  further symbols as well, just by providing {\LaTeX} macros in a
   1.690 +  similar fashion as in @{verbatim isabellesym.sty} of the
   1.691 +  distribution.
   1.692 +
   1.693 +  For proper setup of DVI and PDF documents (with hyperlinks and
   1.694 +  bookmarks), we recommend to include @{verbatim pdfsetup.sty} as
   1.695 +  well.
   1.696 +
   1.697 +  \medskip As a final step of document preparation within Isabelle,
   1.698 +  @{verbatim "isatool document -c"} is run on the resulting @{verbatim
   1.699 +  document} directory.  Thus the actual output document is built and
   1.700 +  installed in its proper place (as linked by the session's @{verbatim
   1.701 +  index.html} if option @{verbatim "-i"} of @{tool_ref usedir} has
   1.702 +  been enabled, cf.\ \secref{sec:info}).  The generated sources are
   1.703 +  deleted after successful run of {\LaTeX} and friends.  Note that a
   1.704 +  separate copy of the sources may be retained by passing an option
   1.705 +  @{verbatim "-D"} to the @{tool usedir} utility when running the
   1.706 +  session.
   1.707 +*}
   1.708 +
   1.709 +
   1.710 +section {* Running {\LaTeX} within the Isabelle environment
   1.711 +  \label{sec:tool-latex} *}
   1.712 +
   1.713 +text {*
   1.714 +  The @{tool_def latex} utility provides the basic interface for
   1.715 +  Isabelle document preparation.  Its usage is:
   1.716 +\begin{ttbox}
   1.717 +Usage: latex [OPTIONS] [FILE]
   1.718 +
   1.719 +  Options are:
   1.720 +    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
   1.721 +                 ps.gz, pdf, bbl, idx, sty, syms
   1.722 +
   1.723 +  Run LaTeX (and related tools) on FILE (default root.tex),
   1.724 +  producing the specified output format.
   1.725 +\end{ttbox}
   1.726 +
   1.727 +  Appropriate {\LaTeX}-related programs are run on the input file,
   1.728 +  according to the given output format: @{executable latex},
   1.729 +  @{executable pdflatex}, @{executable dvips}, @{executable bibtex}
   1.730 +  (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim
   1.731 +  idx}).  The actual commands are determined from the settings
   1.732 +  environment (@{setting ISABELLE_LATEX} etc.).
   1.733 +
   1.734 +  The @{verbatim sty} output format causes the Isabelle style files to
   1.735 +  be updated from the distribution.  This is useful in special
   1.736 +  situations where the document sources are to be processed another
   1.737 +  time by separate tools (cf.\ option @{verbatim "-D"} of the @{tool
   1.738 +  usedir} utility).
   1.739 +
   1.740 +  The @{verbatim syms} output is for internal use; it generates lists
   1.741 +  of symbols that are available without loading additional {\LaTeX}
   1.742 +  packages.
   1.743 +*}
   1.744 +
   1.745 +
   1.746 +subsubsection {* Examples *}
   1.747 +
   1.748 +text {*
   1.749 +  Invoking @{verbatim "isatool latex"} by hand may be occasionally
   1.750 +  useful when debugging failed attempts of the automatic document
   1.751 +  preparation stage of batch-mode Isabelle.  The abortive process
   1.752 +  leaves the sources at a certain place within @{setting
   1.753 +  ISABELLE_BROWSER_INFO}, see the runtime error message for details.
   1.754 +  This enables users to inspect {\LaTeX} runs in further detail, e.g.\
   1.755 +  like this:
   1.756 +\begin{ttbox}
   1.757 +  cd ~/isabelle/browser_info/HOL/Test/document
   1.758 +  isatool latex -o pdf
   1.759 +\end{ttbox}
   1.760 +*}
   1.761 +
   1.762 +end
   1.763 \ No newline at end of file