doc-src/System/Thy/Presentation.thy
author wenzelm
Wed Aug 15 12:36:38 2012 +0200 (2012-08-15 ago)
changeset 48814 d488a5f25bf6
parent 48722 a5e3ba7cbb2a
permissions -rw-r--r--
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
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@48814
     7
text {* Isabelle provides several ways to present the outcome of
wenzelm@48814
     8
  formal developments, including WWW-based browsable libraries or
wenzelm@48814
     9
  actual printable documents.  Presentation is centered around the
wenzelm@48814
    10
  concept of \emph{sessions} (\chref{ch:session}).  The global session
wenzelm@48814
    11
  structure is that of a tree, with Isabelle Pure at its root, further
wenzelm@48814
    12
  object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and
wenzelm@48814
    13
  application sessions further on in the hierarchy.
wenzelm@28221
    14
wenzelm@48814
    15
  The tools @{tool_ref mkroot} and @{tool_ref build} provide the
wenzelm@48814
    16
  primary means for managing Isabelle sessions, including proper setup
wenzelm@48814
    17
  for presentation; @{tool build} takes care to have @{executable_ref
wenzelm@48814
    18
  "isabelle-process"} run any additional stages required for document
wenzelm@48814
    19
  preparation, notably the @{tool_ref document} and @{tool_ref latex}.
wenzelm@48814
    20
  The complete tool chain for managing batch-mode Isabelle sessions is
wenzelm@48814
    21
  illustrated in \figref{fig:session-tools}.
wenzelm@28221
    22
wenzelm@28221
    23
  \begin{figure}[htbp]
wenzelm@28221
    24
  \begin{center}
wenzelm@28221
    25
  \begin{tabular}{lp{0.6\textwidth}}
wenzelm@28221
    26
wenzelm@48814
    27
      @{tool_ref mkroot} & invoked once by the user to initialize the
wenzelm@48814
    28
      session @{verbatim ROOT} with optional @{verbatim document}
wenzelm@48814
    29
      directory; \\
wenzelm@28221
    30
wenzelm@48814
    31
      @{tool_ref build} & invoked repeatedly by the user to keep
wenzelm@48814
    32
      session output up-to-date (HTML, documents etc.); \\
wenzelm@28221
    33
wenzelm@48602
    34
      @{executable "isabelle-process"} & run through @{tool_ref
wenzelm@48814
    35
      build}; \\
wenzelm@28221
    36
wenzelm@48602
    37
      @{tool_ref document} & run by the Isabelle process if document
wenzelm@48602
    38
      preparation is enabled; \\
wenzelm@28221
    39
wenzelm@48602
    40
      @{tool_ref latex} & universal {\LaTeX} tool wrapper invoked
wenzelm@48602
    41
      multiple times by @{tool_ref document}; also useful for manual
wenzelm@48602
    42
      experiments; \\
wenzelm@28221
    43
wenzelm@28221
    44
  \end{tabular}
wenzelm@28221
    45
  \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
wenzelm@28221
    46
  \end{center}
wenzelm@28221
    47
  \end{figure}
wenzelm@28221
    48
*}
wenzelm@28221
    49
wenzelm@28221
    50
wenzelm@28221
    51
section {* Generating theory browser information \label{sec:info} *}
wenzelm@28221
    52
wenzelm@28221
    53
text {*
wenzelm@28221
    54
  \index{theory browsing information|bold}
wenzelm@28221
    55
wenzelm@48814
    56
  As a side-effect of building sessions, Isabelle is able to generate
wenzelm@48814
    57
  theory browsing information, including HTML documents that show the
wenzelm@48814
    58
  theory sources and the relationship with its ancestors and
wenzelm@48814
    59
  descendants.  Besides the HTML file that is generated for every
wenzelm@48814
    60
  theory, Isabelle stores links to all theories in an index
wenzelm@48814
    61
  file. These indexes are linked with other indexes to represent the
wenzelm@48814
    62
  overall tree structure of the sessions.
wenzelm@28221
    63
wenzelm@28221
    64
  Isabelle also generates graph files that represent the theory
wenzelm@48814
    65
  dependencies within a session.  There is a graph browser Java applet
wenzelm@48814
    66
  embedded in the generated HTML pages, and also a stand-alone
wenzelm@48814
    67
  application that allows browsing theory graphs without having to
wenzelm@48814
    68
  start a WWW client first.  The latter version also includes features
wenzelm@48814
    69
  such as generating Postscript files, which are not available in the
wenzelm@48814
    70
  applet version.  See \secref{sec:browse} for further information.
wenzelm@28221
    71
wenzelm@28221
    72
  \medskip
wenzelm@28221
    73
wenzelm@28221
    74
  The easiest way to let Isabelle generate theory browsing information
wenzelm@48814
    75
  for existing sessions is to invoke @{tool build} with suitable
wenzelm@48814
    76
  options:
wenzelm@28221
    77
wenzelm@28221
    78
\begin{ttbox}
wenzelm@48814
    79
isabelle build -o browser_info -v -c FOL
wenzelm@28221
    80
\end{ttbox}
wenzelm@28221
    81
wenzelm@48814
    82
  The presentation output will appear in @{verbatim
wenzelm@48814
    83
  "$ISABELLE_BROWSER_INFO/FOL"} as reported by the above verbose
wenzelm@48814
    84
  invocation of the build process.
wenzelm@28221
    85
wenzelm@48814
    86
  Many Isabelle sessions (such as @{verbatim "HOL-Library"} in @{file
wenzelm@48814
    87
  "~~/src/HOL/Library"}) also provide actual printable documents.
wenzelm@48814
    88
  These are prepared automatically as well if enabled like this:
wenzelm@28221
    89
\begin{ttbox}
wenzelm@48814
    90
isabelle build -o browser_info -o document=pdf -v -c HOL-Library
wenzelm@28221
    91
\end{ttbox}
wenzelm@48814
    92
wenzelm@48814
    93
  Enabling both browser info and document preparation simultaneously
wenzelm@48814
    94
  causes an appropriate ``document'' link to be included in the HTML
wenzelm@48814
    95
  index.  Documents may be generated independently of browser
wenzelm@48814
    96
  information as well, see \secref{sec:tool-document} for further
wenzelm@48814
    97
  details.
wenzelm@28221
    98
wenzelm@28221
    99
  \bigskip The theory browsing information is stored in a
wenzelm@28221
   100
  sub-directory directory determined by the @{setting_ref
wenzelm@28221
   101
  ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the
wenzelm@28221
   102
  session identifier (according to the tree structure of sub-sessions
wenzelm@48814
   103
  by default).  In order to present Isabelle applications on the web,
wenzelm@48814
   104
  the corresponding subdirectory from @{setting ISABELLE_BROWSER_INFO}
wenzelm@48814
   105
  can be put on a WWW server.
wenzelm@28221
   106
*}
wenzelm@28221
   107
wenzelm@48814
   108
section {* Preparing session root directories \label{sec:tool-mkroot} *}
wenzelm@28221
   109
wenzelm@48814
   110
text {* The @{tool_def mkroot} tool configures a given directory as
wenzelm@48814
   111
  session root, with some @{verbatim ROOT} file and optional document
wenzelm@48814
   112
  source directory.  Its usage is:
wenzelm@28221
   113
\begin{ttbox}
wenzelm@48814
   114
Usage: isabelle mkroot [OPTIONS] [DIR]
wenzelm@28221
   115
wenzelm@28221
   116
  Options are:
wenzelm@48814
   117
    -d           enable document preparation
wenzelm@48814
   118
    -n NAME      alternative session name (default: DIR base name)
wenzelm@28221
   119
wenzelm@48814
   120
  Prepare session root DIR (default: current directory).
wenzelm@28221
   121
\end{ttbox}
wenzelm@28221
   122
wenzelm@48814
   123
  The results are placed in the given directory @{text dir}, which
wenzelm@48814
   124
  refers to the current directory by default.  The @{tool mkroot} tool
wenzelm@48814
   125
  is conservative in the sense that it does not overwrite existing
wenzelm@48814
   126
  files or directories.  Earlier attempts to generate a session root
wenzelm@48814
   127
  need to be deleted manually.
wenzelm@28221
   128
wenzelm@48814
   129
  \medskip Option @{verbatim "-d"} indicates that the session shall be
wenzelm@48814
   130
  accompanied by a formal document, with @{text dir}@{verbatim
wenzelm@48814
   131
  "/document/root.tex"} as its {\LaTeX} entry point (see also
wenzelm@48814
   132
  \chref{ch:present}).
wenzelm@28221
   133
wenzelm@48814
   134
  Option @{verbatim "-n"} allows to specify an alternative session
wenzelm@48814
   135
  name; otherwise the base name of the given directory is used.
wenzelm@28221
   136
wenzelm@48814
   137
  \medskip The implicit Isabelle settings variable @{setting
wenzelm@48814
   138
  ISABELLE_LOGIC} specifies the parent session, and @{setting
wenzelm@48814
   139
  ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled
wenzelm@48814
   140
  into the generated @{verbatim ROOT} file.  *}
wenzelm@28221
   141
wenzelm@28221
   142
wenzelm@28221
   143
subsubsection {* Examples *}
wenzelm@28221
   144
wenzelm@48814
   145
text {* Produce session @{verbatim Test} (with document preparation)
wenzelm@48814
   146
  within a separate directory of the same name:
wenzelm@28221
   147
\begin{ttbox}
wenzelm@48814
   148
isabelle mkroot -d Test && isabelle build -D Test
wenzelm@28221
   149
\end{ttbox}
wenzelm@28221
   150
wenzelm@48814
   151
  \medskip Upgrade the current directory into a session ROOT with
wenzelm@48814
   152
  document preparation, and build it:
wenzelm@48814
   153
\begin{ttbox}
wenzelm@48814
   154
isabelle mkroot -d && isabelle build -D .
wenzelm@48814
   155
\end{ttbox}
wenzelm@28221
   156
*}
wenzelm@28221
   157
wenzelm@28221
   158
wenzelm@28221
   159
section {* Preparing Isabelle session documents
wenzelm@28221
   160
  \label{sec:tool-document} *}
wenzelm@28221
   161
wenzelm@48602
   162
text {* The @{tool_def document} tool prepares logic session
wenzelm@48602
   163
  documents, processing the sources both as provided by the user and
wenzelm@48602
   164
  generated by Isabelle.  Its usage is:
wenzelm@28221
   165
\begin{ttbox}
wenzelm@48602
   166
Usage: isabelle document [OPTIONS] [DIR]
wenzelm@28221
   167
wenzelm@28221
   168
  Options are:
wenzelm@28221
   169
    -c           cleanup -- be aggressive in removing old stuff
wenzelm@28221
   170
    -n NAME      specify document name (default 'document')
wenzelm@28221
   171
    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
wenzelm@28221
   172
                 ps.gz, pdf
wenzelm@28221
   173
    -t TAGS      specify tagged region markup
wenzelm@28221
   174
wenzelm@28221
   175
  Prepare the theory session document in DIR (default 'document')
wenzelm@28221
   176
  producing the specified output format.
wenzelm@28221
   177
\end{ttbox}
wenzelm@48814
   178
  This tool is usually run automatically as part of the Isabelle build
wenzelm@48814
   179
  process, provided document preparation has been enabled via suitable
wenzelm@48814
   180
  options.  It may be manually invoked on the generated browser
wenzelm@48814
   181
  information document output as well, e.g.\ in case of errors
wenzelm@48814
   182
  encountered in the batch run.
wenzelm@28221
   183
wenzelm@48602
   184
  \medskip The @{verbatim "-c"} option tells @{tool document} to
wenzelm@48814
   185
  dispose the document sources after successful operation!  This is
wenzelm@28221
   186
  the right thing to do for sources generated by an Isabelle process,
wenzelm@28221
   187
  but take care of your files in manual document preparation!
wenzelm@28221
   188
wenzelm@28221
   189
  \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify
wenzelm@28221
   190
  the final output file name and format, the default is ``@{verbatim
wenzelm@28221
   191
  document.dvi}''.  Note that the result will appear in the parent of
wenzelm@28221
   192
  the target @{verbatim DIR}.
wenzelm@28221
   193
wenzelm@28221
   194
  \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret
wenzelm@28221
   195
  tagged Isabelle command regions.  Tags are specified as a comma
wenzelm@28221
   196
  separated list of modifier/name pairs: ``@{verbatim "+"}@{text
wenzelm@28221
   197
  foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim
wenzelm@28221
   198
  "-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to
wenzelm@28221
   199
  fold text tagged as @{text foo}.  The builtin default is equivalent
wenzelm@28221
   200
  to the tag specification ``@{verbatim
wenzelm@30113
   201
  "+theory,+proof,+ML,+visible,-invisible"}''; see also the {\LaTeX}
wenzelm@28221
   202
  macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
wenzelm@40800
   203
  @{verbatim "\\isafoldtag"}, in @{file
wenzelm@28238
   204
  "~~/lib/texinputs/isabelle.sty"}.
wenzelm@28221
   205
wenzelm@48814
   206
  \medskip Document preparation requires a @{verbatim document}
wenzelm@48814
   207
  directory within the session sources.  This directory is supposed to
wenzelm@48814
   208
  contain all the files needed to produce the final document --- apart
wenzelm@48814
   209
  from the actual theories which are generated by Isabelle.
wenzelm@28221
   210
wenzelm@48602
   211
  \medskip For most practical purposes, @{tool document} is smart
wenzelm@48602
   212
  enough to create any of the specified output formats, taking
wenzelm@28221
   213
  @{verbatim root.tex} supplied by the user as a starting point.  This
wenzelm@28221
   214
  even includes multiple runs of {\LaTeX} to accommodate references
wenzelm@28221
   215
  and bibliographies (the latter assumes @{verbatim root.bib} within
wenzelm@28221
   216
  the same directory).
wenzelm@28221
   217
wenzelm@48657
   218
  In more complex situations, a separate @{verbatim build} script for
wenzelm@48657
   219
  the document sources may be given.  It is invoked with command-line
wenzelm@48657
   220
  arguments for the document format and the document variant name.
wenzelm@48657
   221
  The script needs to produce corresponding output files, e.g.\
wenzelm@48657
   222
  @{verbatim root.pdf} for target format @{verbatim pdf} (and default
wenzelm@48657
   223
  default variants).  The main work can be again delegated to @{tool
wenzelm@48814
   224
  latex}, but it is also possible to harvest generated {\LaTeX}
wenzelm@48814
   225
  sources and copy them elsewhere, for example.
wenzelm@28221
   226
wenzelm@42009
   227
  \medskip When running the session, Isabelle copies the content of
wenzelm@42009
   228
  the original @{verbatim document} directory into its proper place
wenzelm@42009
   229
  within @{setting ISABELLE_BROWSER_INFO}, according to the session
wenzelm@42009
   230
  path and document variant.  Then, for any processed theory @{text A}
wenzelm@42009
   231
  some {\LaTeX} source is generated and put there as @{text
wenzelm@42009
   232
  A}@{verbatim ".tex"}.  Furthermore, a list of all generated theory
wenzelm@42009
   233
  files is put into @{verbatim session.tex}.  Typically, the root
wenzelm@42009
   234
  {\LaTeX} file provided by the user would include @{verbatim
wenzelm@42009
   235
  session.tex} to get a document containing all the theories.
wenzelm@28221
   236
wenzelm@28221
   237
  The {\LaTeX} versions of the theories require some macros defined in
wenzelm@40800
   238
  @{file "~~/lib/texinputs/isabelle.sty"}.  Doing @{verbatim
wenzelm@28238
   239
  "\\usepackage{isabelle}"} in @{verbatim root.tex} should be fine;
wenzelm@48602
   240
  the underlying @{tool latex} already includes an appropriate path
wenzelm@48602
   241
  specification for {\TeX} inputs.
wenzelm@28221
   242
wenzelm@28221
   243
  If the text contains any references to Isabelle symbols (such as
wenzelm@28221
   244
  @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim
wenzelm@28238
   245
  "isabellesym.sty"} should be included as well.  This package
wenzelm@28238
   246
  contains a standard set of {\LaTeX} macro definitions @{verbatim
wenzelm@28221
   247
  "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
wenzelm@28838
   248
  "<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a
wenzelm@28838
   249
  complete list of predefined Isabelle symbols.  Users may invent
wenzelm@28221
   250
  further symbols as well, just by providing {\LaTeX} macros in a
wenzelm@40800
   251
  similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of
wenzelm@28238
   252
  the distribution.
wenzelm@28221
   253
wenzelm@28221
   254
  For proper setup of DVI and PDF documents (with hyperlinks and
wenzelm@40800
   255
  bookmarks), we recommend to include @{file
wenzelm@28238
   256
  "~~/lib/texinputs/pdfsetup.sty"} as well.
wenzelm@28221
   257
wenzelm@48814
   258
  \medskip As a final step of Isabelle document preparation, @{tool
wenzelm@48814
   259
  document}~@{verbatim "-c"} is run on the resulting copy of the
wenzelm@48814
   260
  @{verbatim document} directory.  Thus the actual output document is
wenzelm@48814
   261
  built and installed in its proper place.  The generated sources are
wenzelm@48814
   262
  deleted after successful run of {\LaTeX} and friends.
wenzelm@48814
   263
wenzelm@48814
   264
  Some care is needed if the document output location is configured
wenzelm@48814
   265
  differently, say within a directory whose content is still required
wenzelm@48814
   266
  afterwards!
wenzelm@48814
   267
*}
wenzelm@28221
   268
wenzelm@28221
   269
wenzelm@28221
   270
section {* Running {\LaTeX} within the Isabelle environment
wenzelm@28221
   271
  \label{sec:tool-latex} *}
wenzelm@28221
   272
wenzelm@48602
   273
text {* The @{tool_def latex} tool provides the basic interface for
wenzelm@28221
   274
  Isabelle document preparation.  Its usage is:
wenzelm@28221
   275
\begin{ttbox}
wenzelm@48602
   276
Usage: isabelle latex [OPTIONS] [FILE]
wenzelm@28221
   277
wenzelm@28221
   278
  Options are:
wenzelm@28221
   279
    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
wenzelm@28221
   280
                 ps.gz, pdf, bbl, idx, sty, syms
wenzelm@28221
   281
wenzelm@28221
   282
  Run LaTeX (and related tools) on FILE (default root.tex),
wenzelm@28221
   283
  producing the specified output format.
wenzelm@28221
   284
\end{ttbox}
wenzelm@28221
   285
wenzelm@28221
   286
  Appropriate {\LaTeX}-related programs are run on the input file,
wenzelm@28221
   287
  according to the given output format: @{executable latex},
wenzelm@28221
   288
  @{executable pdflatex}, @{executable dvips}, @{executable bibtex}
wenzelm@28221
   289
  (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim
wenzelm@28221
   290
  idx}).  The actual commands are determined from the settings
wenzelm@28221
   291
  environment (@{setting ISABELLE_LATEX} etc.).
wenzelm@28221
   292
wenzelm@28221
   293
  The @{verbatim sty} output format causes the Isabelle style files to
wenzelm@28221
   294
  be updated from the distribution.  This is useful in special
wenzelm@28221
   295
  situations where the document sources are to be processed another
wenzelm@48814
   296
  time by separate tools.
wenzelm@28221
   297
wenzelm@28221
   298
  The @{verbatim syms} output is for internal use; it generates lists
wenzelm@28221
   299
  of symbols that are available without loading additional {\LaTeX}
wenzelm@28221
   300
  packages.
wenzelm@28221
   301
*}
wenzelm@28221
   302
wenzelm@28221
   303
wenzelm@28221
   304
subsubsection {* Examples *}
wenzelm@28221
   305
wenzelm@48602
   306
text {* Invoking @{tool latex} by hand may be occasionally useful when
wenzelm@48602
   307
  debugging failed attempts of the automatic document preparation
wenzelm@48602
   308
  stage of batch-mode Isabelle.  The abortive process leaves the
wenzelm@48602
   309
  sources at a certain place within @{setting ISABELLE_BROWSER_INFO},
wenzelm@48602
   310
  see the runtime error message for details.  This enables users to
wenzelm@48602
   311
  inspect {\LaTeX} runs in further detail, e.g.\ like this:
wenzelm@48602
   312
wenzelm@28221
   313
\begin{ttbox}
wenzelm@40387
   314
  cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
wenzelm@28504
   315
  isabelle latex -o pdf
wenzelm@28221
   316
\end{ttbox}
wenzelm@28221
   317
*}
wenzelm@28221
   318
wenzelm@28221
   319
end