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