doc-src/System/Thy/Presentation.thy
author wenzelm
Fri Aug 03 12:37:31 2012 +0200 (2012-08-03 ago)
changeset 48657 63ef2f0cf8bb
parent 48616 be8002ee43d8
child 48722 a5e3ba7cbb2a
permissions -rw-r--r--
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm@28221
     1
theory Presentation
wenzelm@43564
     2
imports Base
wenzelm@28221
     3
begin
wenzelm@28221
     4
wenzelm@28221
     5
chapter {* Presenting theories \label{ch:present} *}
wenzelm@28221
     6
wenzelm@28221
     7
text {*
wenzelm@28221
     8
  Isabelle provides several ways to present the outcome of formal
wenzelm@28221
     9
  developments, including WWW-based browsable libraries or actual
wenzelm@28221
    10
  printable documents.  Presentation is centered around the concept of
wenzelm@28221
    11
  \emph{logic sessions}.  The global session structure is that of a
wenzelm@28221
    12
  tree, with Isabelle Pure at its root, further object-logics derived
wenzelm@28221
    13
  (e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions
wenzelm@28221
    14
  in leaf positions (usually without a separate image).
wenzelm@28221
    15
wenzelm@48602
    16
  The tools @{tool_ref mkdir} and @{tool_ref make} provide the primary
wenzelm@48602
    17
  means for managing Isabelle sessions, including proper setup for
wenzelm@48602
    18
  presentation.  Here @{tool_ref usedir} takes care to let
wenzelm@48602
    19
  @{executable_ref "isabelle-process"} process run any additional
wenzelm@48602
    20
  stages required for document preparation, notably the tools
wenzelm@48602
    21
  @{tool_ref document} and @{tool_ref latex}.  The complete tool chain
wenzelm@48602
    22
  for managing batch-mode Isabelle sessions is illustrated in
wenzelm@28221
    23
  \figref{fig:session-tools}.
wenzelm@28221
    24
wenzelm@28221
    25
  \begin{figure}[htbp]
wenzelm@28221
    26
  \begin{center}
wenzelm@28221
    27
  \begin{tabular}{lp{0.6\textwidth}}
wenzelm@28221
    28
wenzelm@48602
    29
      @{tool_ref mkdir} & invoked once by the user to create the
wenzelm@48602
    30
      initial source setup (common @{verbatim IsaMakefile} plus a
wenzelm@48602
    31
      single session directory); \\
wenzelm@28221
    32
wenzelm@48602
    33
      @{tool make} & invoked repeatedly by the user to keep session
wenzelm@48602
    34
      output up-to-date (HTML, documents etc.); \\
wenzelm@28238
    35
wenzelm@48602
    36
      @{tool usedir} & part of the standard @{verbatim IsaMakefile}
wenzelm@48602
    37
      entry of a session; \\
wenzelm@28221
    38
wenzelm@48602
    39
      @{executable "isabelle-process"} & run through @{tool_ref
wenzelm@48602
    40
      usedir}; \\
wenzelm@28221
    41
wenzelm@48602
    42
      @{tool_ref document} & run by the Isabelle process if document
wenzelm@48602
    43
      preparation is enabled; \\
wenzelm@28221
    44
wenzelm@48602
    45
      @{tool_ref latex} & universal {\LaTeX} tool wrapper invoked
wenzelm@48602
    46
      multiple times by @{tool_ref document}; also useful for manual
wenzelm@48602
    47
      experiments; \\
wenzelm@28221
    48
wenzelm@28221
    49
  \end{tabular}
wenzelm@28221
    50
  \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
wenzelm@28221
    51
  \end{center}
wenzelm@28221
    52
  \end{figure}
wenzelm@28221
    53
*}
wenzelm@28221
    54
wenzelm@28221
    55
wenzelm@28221
    56
section {* Generating theory browser information \label{sec:info} *}
wenzelm@28221
    57
wenzelm@28221
    58
text {*
wenzelm@28221
    59
  \index{theory browsing information|bold}
wenzelm@28221
    60
wenzelm@28221
    61
  As a side-effect of running a logic sessions, Isabelle is able to
wenzelm@28221
    62
  generate theory browsing information, including HTML documents that
wenzelm@28221
    63
  show a theory's definition, the theorems proved in its ML file and
wenzelm@28221
    64
  the relationship with its ancestors and descendants.  Besides the
wenzelm@28221
    65
  HTML file that is generated for every theory, Isabelle stores links
wenzelm@28221
    66
  to all theories in an index file. These indexes are linked with
wenzelm@28221
    67
  other indexes to represent the overall tree structure of logic
wenzelm@28221
    68
  sessions.
wenzelm@28221
    69
wenzelm@28221
    70
  Isabelle also generates graph files that represent the theory
wenzelm@28221
    71
  hierarchy of a logic.  There is a graph browser Java applet embedded
wenzelm@28221
    72
  in the generated HTML pages, and also a stand-alone application that
wenzelm@28221
    73
  allows browsing theory graphs without having to start a WWW client
wenzelm@28221
    74
  first.  The latter version also includes features such as generating
wenzelm@28221
    75
  Postscript files, which are not available in the applet version.
wenzelm@28221
    76
  See \secref{sec:browse} for further information.
wenzelm@28221
    77
wenzelm@28221
    78
  \medskip
wenzelm@28221
    79
wenzelm@28221
    80
  The easiest way to let Isabelle generate theory browsing information
wenzelm@28221
    81
  for existing sessions is to append ``@{verbatim "-i true"}'' to the
wenzelm@48602
    82
  @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{tool make}.
wenzelm@48602
    83
  For example, add something like this to your Isabelle settings file
wenzelm@28221
    84
wenzelm@28221
    85
\begin{ttbox}
wenzelm@28221
    86
ISABELLE_USEDIR_OPTIONS="-i true"
wenzelm@28221
    87
\end{ttbox}
wenzelm@28221
    88
wenzelm@40800
    89
  and then change into the @{file "~~/src/FOL"} directory and run
wenzelm@48602
    90
  @{tool make}, or even @{tool make}~@{verbatim all}.  The
wenzelm@48602
    91
  presentation output will appear in @{verbatim
wenzelm@48602
    92
  "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to something like
wenzelm@48602
    93
  @{verbatim "~/.isabelle/IsabelleXXXX/browser_info/FOL"}.  Note that
wenzelm@48602
    94
  option @{verbatim "-v true"} will make the internal runs of @{tool
wenzelm@48602
    95
  usedir} more explicit about such details.
wenzelm@28221
    96
wenzelm@40800
    97
  Many standard Isabelle sessions (such as @{file "~~/src/HOL/ex"})
wenzelm@28238
    98
  also provide actual printable documents.  These are prepared
wenzelm@28221
    99
  automatically as well if enabled like this, using the @{verbatim
wenzelm@28221
   100
  "-d"} option
wenzelm@28221
   101
\begin{ttbox}
wenzelm@28221
   102
ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
wenzelm@28221
   103
\end{ttbox}
wenzelm@28221
   104
  Enabling options @{verbatim "-i"} and @{verbatim "-d"}
wenzelm@28225
   105
  simultaneously as shown above causes an appropriate ``document''
wenzelm@28221
   106
  link to be included in the HTML index.  Documents (or raw document
wenzelm@28221
   107
  sources) may be generated independently of browser information as
wenzelm@28221
   108
  well, see \secref{sec:tool-document} for further details.
wenzelm@28221
   109
wenzelm@28221
   110
  \bigskip The theory browsing information is stored in a
wenzelm@28221
   111
  sub-directory directory determined by the @{setting_ref
wenzelm@28221
   112
  ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the
wenzelm@28221
   113
  session identifier (according to the tree structure of sub-sessions
wenzelm@28221
   114
  by default).  A complete WWW view of all standard object-logics and
wenzelm@28225
   115
  examples of the Isabelle distribution is available at the usual
wenzelm@28225
   116
  Isabelle sites:
wenzelm@28221
   117
  \begin{center}\small
wenzelm@28221
   118
  \begin{tabular}{l}
wenzelm@28225
   119
    \url{http://isabelle.in.tum.de/dist/library/} \\
wenzelm@28225
   120
    \url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/} \\
wenzelm@28225
   121
    \url{http://mirror.cse.unsw.edu.au/pub/isabelle/dist/library/} \\
wenzelm@28221
   122
  \end{tabular}
wenzelm@28221
   123
  \end{center}
wenzelm@28221
   124
  
wenzelm@28221
   125
  \medskip In order to present your own theories on the web, simply
wenzelm@28221
   126
  copy the corresponding subdirectory from @{setting
wenzelm@28221
   127
  ISABELLE_BROWSER_INFO} to your WWW server, having generated browser
wenzelm@28221
   128
  info like this:
wenzelm@28221
   129
\begin{ttbox}
wenzelm@28504
   130
isabelle usedir -i true HOL Foo
wenzelm@28221
   131
\end{ttbox}
wenzelm@28221
   132
wenzelm@28221
   133
  This assumes that directory @{verbatim Foo} contains some @{verbatim
wenzelm@28221
   134
  ROOT.ML} file to load all your theories, and HOL is your parent
wenzelm@48602
   135
  logic image (@{tool_ref mkdir} assists in setting up Isabelle
wenzelm@48602
   136
  session directories.  Theory browser information for HOL should have
wenzelm@48602
   137
  been generated already beforehand.  Alternatively, one may specify
wenzelm@48602
   138
  an external link to an existing body of HTML data by giving @{tool
wenzelm@48602
   139
  usedir} a @{verbatim "-P"} option like this:
wenzelm@28221
   140
\begin{ttbox}
wenzelm@28504
   141
isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
wenzelm@28221
   142
\end{ttbox}
wenzelm@28221
   143
wenzelm@48602
   144
  \medskip For production use, @{tool usedir} is usually invoked in an
wenzelm@48602
   145
  appropriate @{verbatim IsaMakefile}, via @{tool make}.  There is a
wenzelm@48602
   146
  separate @{tool mkdir} tool to provide easy setup of all this, with
wenzelm@48602
   147
  only minimal manual editing required.
wenzelm@28221
   148
\begin{ttbox}
wenzelm@28504
   149
isabelle mkdir HOL Foo && isabelle make
wenzelm@28221
   150
\end{ttbox}
wenzelm@28221
   151
  See \secref{sec:tool-mkdir} for more information on preparing
wenzelm@28221
   152
  Isabelle session directories, including the setup for documents.
wenzelm@28221
   153
*}
wenzelm@28221
   154
wenzelm@28221
   155
wenzelm@28221
   156
section {* Creating Isabelle session directories
wenzelm@28221
   157
  \label{sec:tool-mkdir} *}
wenzelm@28221
   158
wenzelm@48602
   159
text {* The @{tool_def mkdir} tool prepares Isabelle session source
wenzelm@28221
   160
  directories, including a sensible default setup of @{verbatim
wenzelm@28221
   161
  IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document}
wenzelm@28221
   162
  directory with a minimal @{verbatim root.tex} that is sufficient to
wenzelm@28221
   163
  print all theories of the session (in the order of appearance); see
wenzelm@28221
   164
  \secref{sec:tool-document} for further information on Isabelle
wenzelm@48602
   165
  document preparation.  The usage of @{tool mkdir} is:
wenzelm@28221
   166
wenzelm@28221
   167
\begin{ttbox}
wenzelm@48602
   168
Usage: isabelle mkdir [OPTIONS] [LOGIC] NAME
wenzelm@28221
   169
wenzelm@28221
   170
  Options are:
wenzelm@28221
   171
    -I FILE      alternative IsaMakefile output
wenzelm@28221
   172
    -P           include parent logic target
wenzelm@28221
   173
    -b           setup build mode (session outputs heap image)
wenzelm@28221
   174
    -q           quiet mode
wenzelm@28221
   175
wenzelm@28221
   176
  Prepare session directory, including IsaMakefile and document source,
wenzelm@28221
   177
  with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
wenzelm@28221
   178
\end{ttbox}
wenzelm@28221
   179
wenzelm@28221
   180
  The @{tool mkdir} tool is conservative in the sense that any
wenzelm@28221
   181
  existing @{verbatim IsaMakefile} etc.\ is left unchanged.  Thus it
wenzelm@28221
   182
  is safe to invoke it multiple times, although later runs may not
wenzelm@28221
   183
  have the desired effect.
wenzelm@28221
   184
wenzelm@28221
   185
  Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile}
wenzelm@28221
   186
  incrementally --- manual changes are required for multiple
wenzelm@28221
   187
  sub-sessions.  On order to get an initial working session, the only
wenzelm@28221
   188
  editing needed is to add appropriate @{ML use_thy} calls to the
wenzelm@28221
   189
  generated @{verbatim ROOT.ML} file.
wenzelm@28221
   190
*}
wenzelm@28221
   191
wenzelm@28221
   192
wenzelm@28221
   193
subsubsection {* Options *}
wenzelm@28221
   194
wenzelm@28221
   195
text {*
wenzelm@28221
   196
  The @{verbatim "-I"} option specifies an alternative to @{verbatim
wenzelm@28221
   197
  IsaMakefile} for dependencies.  Note that ``@{verbatim "-"}'' refers
wenzelm@28221
   198
  to \emph{stdout}, i.e.\ ``@{verbatim "-I-"}'' provides an easy way
wenzelm@28221
   199
  to peek at @{tool mkdir}'s idea of @{tool make} setup required for
wenzelm@28221
   200
  some particular of Isabelle session.
wenzelm@28221
   201
wenzelm@28221
   202
  \medskip The @{verbatim "-P"} option includes a target for the
wenzelm@28221
   203
  parent @{verbatim LOGIC} session in the generated @{verbatim
wenzelm@28221
   204
  IsaMakefile}.  The corresponding sources are assumed to be located
wenzelm@28221
   205
  within the Isabelle distribution.
wenzelm@28221
   206
wenzelm@28221
   207
  \medskip The @{verbatim "-b"} option sets up the current directory
wenzelm@28221
   208
  as the base for a new session that provides an actual logic image,
wenzelm@28221
   209
  as opposed to one that only runs several theories based on an
wenzelm@28221
   210
  existing image.  Note that in the latter case, everything except
wenzelm@28221
   211
  @{verbatim IsaMakefile} would be placed into a separate directory
wenzelm@28221
   212
  @{verbatim NAME}, rather than the current one.  See
wenzelm@28221
   213
  \secref{sec:tool-usedir} for further information on \emph{build
wenzelm@48602
   214
  mode} vs.\ \emph{example mode} of @{tool usedir}.
wenzelm@28221
   215
wenzelm@28221
   216
  \medskip The @{verbatim "-q"} option enables quiet mode, suppressing
wenzelm@28221
   217
  further notes on how to proceed.
wenzelm@28221
   218
*}
wenzelm@28221
   219
wenzelm@28221
   220
wenzelm@28221
   221
subsubsection {* Examples *}
wenzelm@28221
   222
wenzelm@28221
   223
text {*
wenzelm@28221
   224
  The standard setup of a single ``example session'' based on the
wenzelm@28221
   225
  default logic, with proper document generation is generated like
wenzelm@28221
   226
  this:
wenzelm@28221
   227
\begin{ttbox}
wenzelm@28504
   228
isabelle mkdir Foo && isabelle make
wenzelm@28221
   229
\end{ttbox}
wenzelm@28221
   230
wenzelm@28221
   231
  \noindent The theory sources should be put into the @{verbatim Foo}
wenzelm@28221
   232
  directory, and its @{verbatim ROOT.ML} should be edited to load all
wenzelm@48602
   233
  required theories.  Invoking @{tool make} again would run the whole
wenzelm@48602
   234
  session, generating browser information and the document
wenzelm@48602
   235
  automatically.  The @{verbatim IsaMakefile} is typically tuned
wenzelm@48602
   236
  manually later, e.g.\ adding source dependencies, or changing the
wenzelm@48602
   237
  options passed to @{tool usedir}.
wenzelm@28221
   238
wenzelm@28221
   239
  \medskip Large projects may demand further sessions, potentially
wenzelm@28221
   240
  with separate logic images being created.  This usually requires
wenzelm@28221
   241
  manual editing of the generated @{verbatim IsaMakefile}, which is
wenzelm@28221
   242
  meant to cover all of the sub-session directories at the same time
wenzelm@28221
   243
  (this is the deeper reasong why @{verbatim IsaMakefile} is not made
wenzelm@48602
   244
  part of the initial session directory created by @{tool mkdir}).
wenzelm@48602
   245
  See @{file "~~/src/HOL/IsaMakefile"} for a full-blown example.  *}
wenzelm@28221
   246
wenzelm@28221
   247
wenzelm@28221
   248
section {* Running Isabelle sessions \label{sec:tool-usedir} *}
wenzelm@28221
   249
wenzelm@48602
   250
text {* The @{tool_def usedir} tool builds object-logic images, or
wenzelm@48602
   251
  runs example sessions based on existing logics. Its usage is:
wenzelm@28221
   252
\begin{ttbox}
wenzelm@48602
   253
Usage: isabelle usedir [OPTIONS] LOGIC NAME
wenzelm@28221
   254
wenzelm@28221
   255
  Options are:
wenzelm@28221
   256
    -C BOOL      copy existing document directory to -D PATH (default true)
wenzelm@28221
   257
    -D PATH      dump generated document sources into PATH
wenzelm@28221
   258
    -M MAX       multithreading: maximum number of worker threads (default 1)
wenzelm@28221
   259
    -P PATH      set path for remote theory browsing information
wenzelm@41819
   260
    -Q INT       set threshold for sub-proof parallelization (default 50)
wenzelm@28221
   261
    -T LEVEL     multithreading: trace level (default 0)
wenzelm@42004
   262
    -V VARIANT   declare alternative document VARIANT
wenzelm@28221
   263
    -b           build mode (output heap image, using current dir)
wenzelm@28221
   264
    -d FORMAT    build document as FORMAT (default false)
wenzelm@28221
   265
    -f NAME      use ML file NAME (default ROOT.ML)
wenzelm@28221
   266
    -g BOOL      generate session graph image for document (default false)
wenzelm@28221
   267
    -i BOOL      generate theory browser information (default false)
wenzelm@28221
   268
    -m MODE      add print mode for output
wenzelm@32061
   269
    -p LEVEL     set level of detail for proof objects (default 0)
wenzelm@32061
   270
    -q LEVEL     set level of parallel proof checking (default 1)
wenzelm@28221
   271
    -r           reset session path
wenzelm@28221
   272
    -s NAME      override session NAME
wenzelm@31688
   273
    -t BOOL      internal session timing (default false)
wenzelm@28221
   274
    -v BOOL      be verbose (default false)
wenzelm@28221
   275
wenzelm@28221
   276
  Build object-logic or run examples. Also creates browsing
wenzelm@28221
   277
  information (HTML etc.) according to settings.
wenzelm@28221
   278
wenzelm@47978
   279
  ISABELLE_USEDIR_OPTIONS=...
wenzelm@29435
   280
wenzelm@47978
   281
  ML_PLATFORM=...
wenzelm@47978
   282
  ML_HOME=...
wenzelm@47978
   283
  ML_SYSTEM=...
wenzelm@47978
   284
  ML_OPTIONS=...
wenzelm@28221
   285
\end{ttbox}
wenzelm@28221
   286
wenzelm@28221
   287
  Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
wenzelm@28221
   288
  setting is implicitly prefixed to \emph{any} @{tool usedir}
wenzelm@28221
   289
  call. Since the @{verbatim IsaMakefile}s of all object-logics
wenzelm@28238
   290
  distributed with Isabelle just invoke @{tool usedir} for the real
wenzelm@28221
   291
  work, one may control compilation options globally via above
wenzelm@28221
   292
  variable. In particular, generation of \rmindex{HTML} browsing
wenzelm@28221
   293
  information and document preparation is controlled here.
wenzelm@28221
   294
*}
wenzelm@28221
   295
wenzelm@28221
   296
wenzelm@28221
   297
subsubsection {* Options *}
wenzelm@28221
   298
wenzelm@28221
   299
text {*
wenzelm@28221
   300
  Basically, there are two different modes of operation: \emph{build
wenzelm@28221
   301
  mode} (enabled through the @{verbatim "-b"} option) and
wenzelm@28221
   302
  \emph{example mode} (default).
wenzelm@28221
   303
wenzelm@28221
   304
  Calling @{tool usedir} with @{verbatim "-b"} runs @{executable
wenzelm@28221
   305
  "isabelle-process"} with input image @{verbatim LOGIC} and output to
wenzelm@28221
   306
  @{verbatim NAME}, as provided on the command line. This will be a
wenzelm@28221
   307
  batch session, running @{verbatim ROOT.ML} from the current
wenzelm@28221
   308
  directory and then quitting.  It is assumed that @{verbatim ROOT.ML}
wenzelm@28221
   309
  contains all ML commands required to build the logic.
wenzelm@28221
   310
wenzelm@28238
   311
  In example mode, @{tool usedir} runs a read-only session of
wenzelm@28221
   312
  @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from
wenzelm@28221
   313
  within directory @{verbatim NAME}.  It assumes that this file
wenzelm@28221
   314
  contains appropriate ML commands to run the desired examples.
wenzelm@28221
   315
wenzelm@28221
   316
  \medskip The @{verbatim "-i"} option controls theory browser data
wenzelm@28221
   317
  generation. It may be explicitly turned on or off --- as usual, the
wenzelm@28221
   318
  last occurrence of @{verbatim "-i"} on the command line wins.
wenzelm@28221
   319
wenzelm@28221
   320
  The @{verbatim "-P"} option specifies a path (or actual URL) to be
wenzelm@28221
   321
  prefixed to any \emph{non-local} reference of existing theories.
wenzelm@28221
   322
  Thus user sessions may easily link to existing Isabelle libraries
wenzelm@28221
   323
  already present on the WWW.
wenzelm@28221
   324
wenzelm@28221
   325
  The @{verbatim "-m"} options specifies additional print modes to be
wenzelm@28221
   326
  activated temporarily while the session is processed.
wenzelm@28221
   327
wenzelm@28221
   328
  \medskip The @{verbatim "-d"} option controls document preparation.
wenzelm@28221
   329
  Valid arguments are @{verbatim false} (do not prepare any document;
wenzelm@28221
   330
  this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz},
wenzelm@28221
   331
  @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}.  The logic
wenzelm@28221
   332
  session has to provide a properly setup @{verbatim document}
wenzelm@28221
   333
  directory.  See \secref{sec:tool-document} and
wenzelm@28221
   334
  \secref{sec:tool-latex} for more details.
wenzelm@28221
   335
wenzelm@28221
   336
  \medskip The @{verbatim "-V"} option declares alternative document
wenzelm@42004
   337
  variants, consisting of name/tags pairs (cf.\ options @{verbatim
wenzelm@48602
   338
  "-n"} and @{verbatim "-t"} of @{tool_ref document}).  The standard
wenzelm@48602
   339
  document is equivalent to ``@{verbatim
wenzelm@28221
   340
  "document=theory,proof,ML"}'', which means that all theory begin/end
wenzelm@28221
   341
  commands, proof body texts, and ML code will be presented
wenzelm@48616
   342
  faithfully.
wenzelm@48616
   343
wenzelm@48616
   344
  An alternative variant ``@{verbatim "outline=/proof/ML"}'' would
wenzelm@48616
   345
  fold proof and ML parts, replacing the original text by a short
wenzelm@48616
   346
  place-holder.  The form ``@{text name}@{verbatim "=-"},'' means to
wenzelm@48616
   347
  remove document @{text name} from the list of variants to be
wenzelm@48616
   348
  processed.  Any number of @{verbatim "-V"} options may be given;
wenzelm@48616
   349
  later declarations have precedence over earlier ones.
wenzelm@48616
   350
wenzelm@48616
   351
  Some document variant @{text name} may use an alternative {\LaTeX}
wenzelm@48616
   352
  entry point called @{verbatim "document/root_"}@{text
wenzelm@48616
   353
  "name"}@{verbatim ".tex"} if that file exists; otherwise the common
wenzelm@48616
   354
  @{verbatim "document/root.tex"} is used.
wenzelm@28221
   355
wenzelm@28221
   356
  \medskip The @{verbatim "-g"} option produces images of the theory
wenzelm@28221
   357
  dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
wenzelm@28221
   358
  generated document, both as @{verbatim session_graph.eps} and
wenzelm@28221
   359
  @{verbatim session_graph.pdf} at the same time.  To include this in
wenzelm@28221
   360
  the final {\LaTeX} document one could say @{verbatim
wenzelm@28221
   361
  "\\includegraphics{session_graph}"} in @{verbatim
wenzelm@28221
   362
  "document/root.tex"} (omitting the file-name extension enables
wenzelm@28221
   363
  {\LaTeX} to select to correct version, either for the DVI or PDF
wenzelm@28221
   364
  output path).
wenzelm@28221
   365
wenzelm@28221
   366
  \medskip The @{verbatim "-D"} option causes the generated document
wenzelm@28221
   367
  sources to be dumped at location @{verbatim PATH}; this path is
wenzelm@28221
   368
  relative to the session's main directory.  If the @{verbatim "-C"}
wenzelm@28221
   369
  option is true, this will include a copy of an existing @{verbatim
wenzelm@48602
   370
  document} directory as provided by the user.  For example, @{tool
wenzelm@48602
   371
  usedir}~@{verbatim "-D generated HOL Foo"} produces a complete set
wenzelm@48602
   372
  of document sources at @{verbatim "Foo/generated"}.  Subsequent
wenzelm@48602
   373
  invocation of @{tool document}~@{verbatim "Foo/generated"} (see also
wenzelm@28238
   374
  \secref{sec:tool-document}) will process the final result
wenzelm@28238
   375
  independently of an Isabelle job.  This decoupled mode of operation
wenzelm@28238
   376
  facilitates debugging of serious {\LaTeX} errors, for example.
wenzelm@28221
   377
wenzelm@28221
   378
  \medskip The @{verbatim "-p"} option determines the level of detail
wenzelm@28221
   379
  for internal proof objects, see also the \emph{Isabelle Reference
wenzelm@28221
   380
  Manual}~\cite{isabelle-ref}.
wenzelm@28221
   381
wenzelm@32061
   382
  \medskip The @{verbatim "-q"} option specifies the level of parallel
wenzelm@32061
   383
  proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel
wenzelm@32061
   384
  proofs (default), @{verbatim 2} toplevel and nested Isar proofs.
wenzelm@41703
   385
  The option @{verbatim "-Q"} specifies a threshold for @{verbatim
wenzelm@41703
   386
  "-q2"}: nested proofs are only parallelized when the current number
wenzelm@41819
   387
  of forked proofs falls below the given value (default 50),
wenzelm@41819
   388
  multiplied by the number of worker threads (see option @{verbatim
wenzelm@41819
   389
  "-M"}).
wenzelm@32061
   390
wenzelm@31688
   391
  \medskip The @{verbatim "-t"} option produces a more detailed
wenzelm@31688
   392
  internal timing report of the session.
wenzelm@31688
   393
wenzelm@28221
   394
  \medskip The @{verbatim "-v"} option causes additional information
wenzelm@28221
   395
  to be printed while running the session, notably the location of
wenzelm@28221
   396
  prepared documents.
wenzelm@28221
   397
wenzelm@28221
   398
  \medskip The @{verbatim "-M"} option specifies the maximum number of
wenzelm@41819
   399
  parallel worker threads used for processing independent tasks when
wenzelm@41819
   400
  checking theory sources (multithreading only works on suitable ML
wenzelm@41819
   401
  platforms).  The special value of @{verbatim 0} or @{verbatim max}
wenzelm@41819
   402
  refers to the number of actual CPU cores of the underlying machine,
wenzelm@41819
   403
  which is a good starting point for optimal performance tuning.  The
wenzelm@41819
   404
  @{verbatim "-T"} option determines the level of detail in tracing
wenzelm@41819
   405
  output concerning the internal locking and scheduling in
wenzelm@41819
   406
  multithreaded operation.  This may be helpful in isolating
wenzelm@41819
   407
  performance bottle-necks, e.g.\ due to excessive wait states when
wenzelm@41819
   408
  locking critical code sections.
wenzelm@28221
   409
wenzelm@28221
   410
  \medskip Any @{tool usedir} session is named by some \emph{session
wenzelm@28221
   411
  identifier}. These accumulate, documenting the way sessions depend
wenzelm@28221
   412
  on others. For example, consider @{verbatim "Pure/FOL/ex"}, which
wenzelm@28221
   413
  refers to the examples of FOL, which in turn is built upon Pure.
wenzelm@28221
   414
wenzelm@28221
   415
  The current session's identifier is by default just the base name of
wenzelm@28221
   416
  the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim
wenzelm@28221
   417
  NAME} argument (in example mode). This may be overridden explicitly
wenzelm@28221
   418
  via the @{verbatim "-s"} option.
wenzelm@28221
   419
*}
wenzelm@28221
   420
wenzelm@28221
   421
wenzelm@28221
   422
subsubsection {* Examples *}
wenzelm@28221
   423
wenzelm@48602
   424
text {* Refer to the @{verbatim IsaMakefile}s of the Isabelle
wenzelm@48602
   425
  distribution's object-logics as a model for your own developments.
wenzelm@48602
   426
  For example, see @{file "~~/src/FOL/IsaMakefile"}.  The @{tool_ref
wenzelm@28221
   427
  mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation
wenzelm@48602
   428
  of @{tool usedir} as well.  *}
wenzelm@28221
   429
wenzelm@28221
   430
wenzelm@28221
   431
section {* Preparing Isabelle session documents
wenzelm@28221
   432
  \label{sec:tool-document} *}
wenzelm@28221
   433
wenzelm@48602
   434
text {* The @{tool_def document} tool prepares logic session
wenzelm@48602
   435
  documents, processing the sources both as provided by the user and
wenzelm@48602
   436
  generated by Isabelle.  Its usage is:
wenzelm@28221
   437
\begin{ttbox}
wenzelm@48602
   438
Usage: isabelle document [OPTIONS] [DIR]
wenzelm@28221
   439
wenzelm@28221
   440
  Options are:
wenzelm@28221
   441
    -c           cleanup -- be aggressive in removing old stuff
wenzelm@28221
   442
    -n NAME      specify document name (default 'document')
wenzelm@28221
   443
    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
wenzelm@28221
   444
                 ps.gz, pdf
wenzelm@28221
   445
    -t TAGS      specify tagged region markup
wenzelm@28221
   446
wenzelm@28221
   447
  Prepare the theory session document in DIR (default 'document')
wenzelm@28221
   448
  producing the specified output format.
wenzelm@28221
   449
\end{ttbox}
wenzelm@28221
   450
  This tool is usually run automatically as part of the corresponding
wenzelm@28221
   451
  Isabelle batch process, provided document preparation has been
wenzelm@48602
   452
  enabled (cf.\ the @{verbatim "-d"} option of @{tool_ref usedir}).
wenzelm@48602
   453
  It may be manually invoked on the generated browser information
wenzelm@48602
   454
  document output as well, e.g.\ in case of errors encountered in the
wenzelm@48602
   455
  batch run.
wenzelm@28221
   456
wenzelm@48602
   457
  \medskip The @{verbatim "-c"} option tells @{tool document} to
wenzelm@48602
   458
  dispose the document sources after successful operation.  This is
wenzelm@28221
   459
  the right thing to do for sources generated by an Isabelle process,
wenzelm@28221
   460
  but take care of your files in manual document preparation!
wenzelm@28221
   461
wenzelm@28221
   462
  \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify
wenzelm@28221
   463
  the final output file name and format, the default is ``@{verbatim
wenzelm@28221
   464
  document.dvi}''.  Note that the result will appear in the parent of
wenzelm@28221
   465
  the target @{verbatim DIR}.
wenzelm@28221
   466
wenzelm@28221
   467
  \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret
wenzelm@28221
   468
  tagged Isabelle command regions.  Tags are specified as a comma
wenzelm@28221
   469
  separated list of modifier/name pairs: ``@{verbatim "+"}@{text
wenzelm@28221
   470
  foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim
wenzelm@28221
   471
  "-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to
wenzelm@28221
   472
  fold text tagged as @{text foo}.  The builtin default is equivalent
wenzelm@28221
   473
  to the tag specification ``@{verbatim
wenzelm@30113
   474
  "+theory,+proof,+ML,+visible,-invisible"}''; see also the {\LaTeX}
wenzelm@28221
   475
  macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
wenzelm@40800
   476
  @{verbatim "\\isafoldtag"}, in @{file
wenzelm@28238
   477
  "~~/lib/texinputs/isabelle.sty"}.
wenzelm@28221
   478
wenzelm@28221
   479
  \medskip Document preparation requires a properly setup ``@{verbatim
wenzelm@28221
   480
  document}'' directory within the logic session sources.  This
wenzelm@28221
   481
  directory is supposed to contain all the files needed to produce the
wenzelm@28221
   482
  final document --- apart from the actual theories which are
wenzelm@28221
   483
  generated by Isabelle.
wenzelm@28221
   484
wenzelm@48602
   485
  \medskip For most practical purposes, @{tool document} is smart
wenzelm@48602
   486
  enough to create any of the specified output formats, taking
wenzelm@28221
   487
  @{verbatim root.tex} supplied by the user as a starting point.  This
wenzelm@28221
   488
  even includes multiple runs of {\LaTeX} to accommodate references
wenzelm@28221
   489
  and bibliographies (the latter assumes @{verbatim root.bib} within
wenzelm@28221
   490
  the same directory).
wenzelm@28221
   491
wenzelm@48657
   492
  In more complex situations, a separate @{verbatim build} script for
wenzelm@48657
   493
  the document sources may be given.  It is invoked with command-line
wenzelm@48657
   494
  arguments for the document format and the document variant name.
wenzelm@48657
   495
  The script needs to produce corresponding output files, e.g.\
wenzelm@48657
   496
  @{verbatim root.pdf} for target format @{verbatim pdf} (and default
wenzelm@48657
   497
  default variants).  The main work can be again delegated to @{tool
wenzelm@48657
   498
  latex}.
wenzelm@28221
   499
wenzelm@42009
   500
  \medskip When running the session, Isabelle copies the content of
wenzelm@42009
   501
  the original @{verbatim document} directory into its proper place
wenzelm@42009
   502
  within @{setting ISABELLE_BROWSER_INFO}, according to the session
wenzelm@42009
   503
  path and document variant.  Then, for any processed theory @{text A}
wenzelm@42009
   504
  some {\LaTeX} source is generated and put there as @{text
wenzelm@42009
   505
  A}@{verbatim ".tex"}.  Furthermore, a list of all generated theory
wenzelm@42009
   506
  files is put into @{verbatim session.tex}.  Typically, the root
wenzelm@42009
   507
  {\LaTeX} file provided by the user would include @{verbatim
wenzelm@42009
   508
  session.tex} to get a document containing all the theories.
wenzelm@28221
   509
wenzelm@28221
   510
  The {\LaTeX} versions of the theories require some macros defined in
wenzelm@40800
   511
  @{file "~~/lib/texinputs/isabelle.sty"}.  Doing @{verbatim
wenzelm@28238
   512
  "\\usepackage{isabelle}"} in @{verbatim root.tex} should be fine;
wenzelm@48602
   513
  the underlying @{tool latex} already includes an appropriate path
wenzelm@48602
   514
  specification for {\TeX} inputs.
wenzelm@28221
   515
wenzelm@28221
   516
  If the text contains any references to Isabelle symbols (such as
wenzelm@28221
   517
  @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim
wenzelm@28238
   518
  "isabellesym.sty"} should be included as well.  This package
wenzelm@28238
   519
  contains a standard set of {\LaTeX} macro definitions @{verbatim
wenzelm@28221
   520
  "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
wenzelm@28838
   521
  "<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a
wenzelm@28838
   522
  complete list of predefined Isabelle symbols.  Users may invent
wenzelm@28221
   523
  further symbols as well, just by providing {\LaTeX} macros in a
wenzelm@40800
   524
  similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of
wenzelm@28238
   525
  the distribution.
wenzelm@28221
   526
wenzelm@28221
   527
  For proper setup of DVI and PDF documents (with hyperlinks and
wenzelm@40800
   528
  bookmarks), we recommend to include @{file
wenzelm@28238
   529
  "~~/lib/texinputs/pdfsetup.sty"} as well.
wenzelm@28221
   530
wenzelm@28221
   531
  \medskip As a final step of document preparation within Isabelle,
wenzelm@48602
   532
  @{tool document}~@{verbatim "-c"} is run on the resulting @{verbatim
wenzelm@48602
   533
  document} directory.  Thus the actual output document is built and
wenzelm@48602
   534
  installed in its proper place (as linked by the session's @{verbatim
wenzelm@48602
   535
  index.html} if option @{verbatim "-i"} of @{tool_ref usedir} has
wenzelm@48602
   536
  been enabled, cf.\ \secref{sec:info}).  The generated sources are
wenzelm@48602
   537
  deleted after successful run of {\LaTeX} and friends.  Note that a
wenzelm@48602
   538
  separate copy of the sources may be retained by passing an option
wenzelm@48602
   539
  @{verbatim "-D"} to @{tool usedir} when running the session.  *}
wenzelm@28221
   540
wenzelm@28221
   541
wenzelm@28221
   542
section {* Running {\LaTeX} within the Isabelle environment
wenzelm@28221
   543
  \label{sec:tool-latex} *}
wenzelm@28221
   544
wenzelm@48602
   545
text {* The @{tool_def latex} tool provides the basic interface for
wenzelm@28221
   546
  Isabelle document preparation.  Its usage is:
wenzelm@28221
   547
\begin{ttbox}
wenzelm@48602
   548
Usage: isabelle latex [OPTIONS] [FILE]
wenzelm@28221
   549
wenzelm@28221
   550
  Options are:
wenzelm@28221
   551
    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
wenzelm@28221
   552
                 ps.gz, pdf, bbl, idx, sty, syms
wenzelm@28221
   553
wenzelm@28221
   554
  Run LaTeX (and related tools) on FILE (default root.tex),
wenzelm@28221
   555
  producing the specified output format.
wenzelm@28221
   556
\end{ttbox}
wenzelm@28221
   557
wenzelm@28221
   558
  Appropriate {\LaTeX}-related programs are run on the input file,
wenzelm@28221
   559
  according to the given output format: @{executable latex},
wenzelm@28221
   560
  @{executable pdflatex}, @{executable dvips}, @{executable bibtex}
wenzelm@28221
   561
  (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim
wenzelm@28221
   562
  idx}).  The actual commands are determined from the settings
wenzelm@28221
   563
  environment (@{setting ISABELLE_LATEX} etc.).
wenzelm@28221
   564
wenzelm@28221
   565
  The @{verbatim sty} output format causes the Isabelle style files to
wenzelm@28221
   566
  be updated from the distribution.  This is useful in special
wenzelm@28221
   567
  situations where the document sources are to be processed another
wenzelm@48602
   568
  time by separate tools (cf.\ option @{verbatim "-D"} of @{tool
wenzelm@48602
   569
  usedir}).
wenzelm@28221
   570
wenzelm@28221
   571
  The @{verbatim syms} output is for internal use; it generates lists
wenzelm@28221
   572
  of symbols that are available without loading additional {\LaTeX}
wenzelm@28221
   573
  packages.
wenzelm@28221
   574
*}
wenzelm@28221
   575
wenzelm@28221
   576
wenzelm@28221
   577
subsubsection {* Examples *}
wenzelm@28221
   578
wenzelm@48602
   579
text {* Invoking @{tool latex} by hand may be occasionally useful when
wenzelm@48602
   580
  debugging failed attempts of the automatic document preparation
wenzelm@48602
   581
  stage of batch-mode Isabelle.  The abortive process leaves the
wenzelm@48602
   582
  sources at a certain place within @{setting ISABELLE_BROWSER_INFO},
wenzelm@48602
   583
  see the runtime error message for details.  This enables users to
wenzelm@48602
   584
  inspect {\LaTeX} runs in further detail, e.g.\ like this:
wenzelm@48602
   585
wenzelm@28221
   586
\begin{ttbox}
wenzelm@40387
   587
  cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
wenzelm@28504
   588
  isabelle latex -o pdf
wenzelm@28221
   589
\end{ttbox}
wenzelm@28221
   590
*}
wenzelm@28221
   591
wenzelm@28221
   592
end