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