src/Doc/System/Presentation.thy
author haftmann
Mon Feb 06 20:56:34 2017 +0100 (2017-02-06)
changeset 64990 c6a7de505796
parent 63680 6e1e8b5abbfa
child 67042 677cab7c2b85
permissions -rw-r--r--
more explicit errors in pathological cases
     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     -d           enable document preparation
   101     -n NAME      alternative session name (default: DIR base name)
   102 
   103   Prepare session root DIR (default: current directory).\<close>}
   104 
   105   The results are placed in the given directory \<open>dir\<close>, which refers to the
   106   current directory by default. The @{tool mkroot} tool is conservative in the
   107   sense that it does not overwrite existing files or directories. Earlier
   108   attempts to generate a session root need to be deleted manually.
   109 
   110   \<^medskip>
   111   Option \<^verbatim>\<open>-d\<close> indicates that the session shall be accompanied by a formal
   112   document, with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see
   113   also \chref{ch:present}).
   114 
   115   Option \<^verbatim>\<open>-n\<close> allows to specify an alternative session name; otherwise the
   116   base name of the given directory is used.
   117 
   118   \<^medskip>
   119   The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies
   120   the parent session, and @{setting ISABELLE_DOCUMENT_FORMAT} the document
   121   format to be filled filled into the generated \<^verbatim>\<open>ROOT\<close> file.
   122 \<close>
   123 
   124 
   125 subsubsection \<open>Examples\<close>
   126 
   127 text \<open>
   128   Produce session \<^verbatim>\<open>Test\<close> (with document preparation) within a separate
   129   directory of the same name:
   130   @{verbatim [display] \<open>isabelle mkroot -d Test && isabelle build -D Test\<close>}
   131 
   132   \<^medskip>
   133   Upgrade the current directory into a session ROOT with document preparation,
   134   and build it:
   135   @{verbatim [display] \<open>isabelle mkroot -d && isabelle build -D .\<close>}
   136 \<close>
   137 
   138 
   139 section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close>
   140 
   141 text \<open>
   142   The @{tool_def document} tool prepares logic session documents, processing
   143   the sources as provided by the user and generated by Isabelle. Its usage is:
   144   @{verbatim [display]
   145 \<open>Usage: isabelle document [OPTIONS] [DIR]
   146 
   147   Options are:
   148     -c           cleanup -- be aggressive in removing old stuff
   149     -n NAME      specify document name (default 'document')
   150     -o FORMAT    specify output format: pdf (default), dvi
   151     -t TAGS      specify tagged region markup
   152 
   153   Prepare the theory session document in DIR (default 'document')
   154   producing the specified output format.\<close>}
   155 
   156   This tool is usually run automatically as part of the Isabelle build
   157   process, provided document preparation has been enabled via suitable
   158   options. It may be manually invoked on the generated browser information
   159   document output as well, e.g.\ in case of errors encountered in the batch
   160   run.
   161 
   162   \<^medskip>
   163   The \<^verbatim>\<open>-c\<close> option tells @{tool document} to dispose the document sources
   164   after successful operation! This is the right thing to do for sources
   165   generated by an Isabelle process, but take care of your files in manual
   166   document preparation!
   167 
   168   \<^medskip>
   169   The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format,
   170   the default is ``\<^verbatim>\<open>document.dvi\<close>''. Note that the result will appear in the
   171   parent of the target \<^verbatim>\<open>DIR\<close>.
   172 
   173   \<^medskip>
   174   The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
   175   regions. Tags are specified as a comma separated list of modifier/name
   176   pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
   177   drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
   178   equivalent to the tag specification
   179   ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
   180   \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in
   181   \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
   182 
   183   \<^medskip>
   184   Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session
   185   sources. This directory is supposed to contain all the files needed to
   186   produce the final document --- apart from the actual theories which are
   187   generated by Isabelle.
   188 
   189   \<^medskip>
   190   For most practical purposes, @{tool document} is smart enough to create any
   191   of the specified output formats, taking \<^verbatim>\<open>root.tex\<close> supplied by the user as
   192   a starting point. This even includes multiple runs of {\LaTeX} to
   193   accommodate references and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close>
   194   within the same directory).
   195 
   196   In more complex situations, a separate \<^verbatim>\<open>build\<close> script for the document
   197   sources may be given. It is invoked with command-line arguments for the
   198   document format and the document variant name. The script needs to produce
   199   corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and
   200   default variants). The main work can be again delegated to @{tool latex},
   201   but it is also possible to harvest generated {\LaTeX} sources and copy them
   202   elsewhere.
   203 
   204   \<^medskip>
   205   When running the session, Isabelle copies the content of the original
   206   \<^verbatim>\<open>document\<close> directory into its proper place within @{setting
   207   ISABELLE_BROWSER_INFO}, according to the session path and document variant.
   208   Then, for any processed theory \<open>A\<close> some {\LaTeX} source is generated and put
   209   there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>. Furthermore, a list of all generated theory files is
   210   put into \<^verbatim>\<open>session.tex\<close>. Typically, the root {\LaTeX} file provided by the
   211   user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the
   212   theories.
   213 
   214   The {\LaTeX} versions of the theories require some macros defined in
   215   \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
   216   \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an
   217   appropriate path specification for {\TeX} inputs.
   218 
   219   If the text contains any references to Isabelle symbols (such as \<^verbatim>\<open>\<forall>\<close>) then
   220   \<^verbatim>\<open>isabellesym.sty\<close> should be included as well. This package contains a
   221   standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to
   222   \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list
   223   of predefined Isabelle symbols. Users may invent further symbols as well,
   224   just by providing {\LaTeX} macros in a similar fashion as in
   225   \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution.
   226 
   227   For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),
   228   we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
   229 
   230   \<^medskip>
   231   As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
   232   run on the resulting copy of the \<^verbatim>\<open>document\<close> directory. Thus the actual
   233   output document is built and installed in its proper place. The generated
   234   sources are deleted after successful run of {\LaTeX} and friends.
   235 
   236   Some care is needed if the document output location is configured
   237   differently, say within a directory whose content is still required
   238   afterwards!
   239 \<close>
   240 
   241 
   242 section \<open>Running {\LaTeX} within the Isabelle environment
   243   \label{sec:tool-latex}\<close>
   244 
   245 text \<open>
   246   The @{tool_def latex} tool provides the basic interface for Isabelle
   247   document preparation. Its usage is:
   248   @{verbatim [display]
   249 \<open>Usage: isabelle latex [OPTIONS] [FILE]
   250 
   251   Options are:
   252     -o FORMAT    specify output format: pdf (default), dvi,
   253                  bbl, idx, sty, syms
   254 
   255   Run LaTeX (and related tools) on FILE (default root.tex),
   256   producing the specified output format.\<close>}
   257 
   258   Appropriate {\LaTeX}-related programs are run on the input file, according
   259   to the given output format: @{executable latex}, @{executable pdflatex},
   260   @{executable dvips}, @{executable bibtex} (for \<^verbatim>\<open>bbl\<close>), and @{executable
   261   makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands are determined from the
   262   settings environment (@{setting ISABELLE_PDFLATEX} etc.).
   263 
   264   The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from
   265   the distribution. This is useful in special situations where the document
   266   sources are to be processed another time by separate tools.
   267 
   268   The \<^verbatim>\<open>syms\<close> output is for internal use; it generates lists of symbols that
   269   are available without loading additional {\LaTeX} packages.
   270 \<close>
   271 
   272 
   273 subsubsection \<open>Examples\<close>
   274 
   275 text \<open>
   276   Invoking @{tool latex} by hand may be occasionally useful when debugging
   277   failed attempts of the automatic document preparation stage of batch-mode
   278   Isabelle. The abortive process leaves the sources at a certain place within
   279   @{setting ISABELLE_BROWSER_INFO}, see the runtime error message for details.
   280   This enables users to inspect {\LaTeX} runs in further detail, e.g.\ like
   281   this:
   282 
   283   @{verbatim [display]
   284 \<open>cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
   285 isabelle latex -o pdf\<close>}
   286 \<close>
   287 
   288 end