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