author wenzelm
Sat Dec 16 21:53:07 2017 +0100 (18 months ago)
changeset 67219 81e9804b2014
parent 67185 d5e51ba21561
child 67263 449a989f42cd
permissions -rw-r--r--
added document antiquotation @{session name};
renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;
     1 (*:maxLineLen=78:*)
     3 theory Presentation
     4 imports Base
     5 begin
     7 chapter \<open>Presenting theories \label{ch:present}\<close>
     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.
    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}.
    25   \begin{figure}[htbp]
    26   \begin{center}
    27   \begin{tabular}{lp{0.6\textwidth}}
    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; \\
    33       @{tool_ref build} & invoked repeatedly by the user to keep
    34       session output up-to-date (HTML, documents etc.); \\
    36       @{tool_ref process} & run through @{tool_ref build}; \\
    38       @{tool_ref document} & run by the Isabelle process if document
    39       preparation is enabled; \\
    41       @{tool_ref latex} & universal {\LaTeX} tool wrapper invoked
    42       multiple times by @{tool_ref document}; also useful for manual
    43       experiments; \\
    45   \end{tabular}
    46   \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
    47   \end{center}
    48   \end{figure}
    49 \<close>
    52 section \<open>Generating HTML browser information \label{sec:info}\<close>
    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.
    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>}
    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.
    72   Many Isabelle sessions (such as \<^session>\<open>HOL-Library\<close> in
    73   \<^dir>\<open>~~/src/HOL/Library\<close>) also provide printable documents in PDF. These are
    74   prepared automatically as well if enabled like this:
    75   @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
    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.
    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>
    91 section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close>
    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] [DIRECTORY]
    99   Options are:
   100     -A LATEX     provide author in LaTeX notation (default: user name)
   101     -I           init Mercurial repository and add generated files
   102     -T LATEX     provide title in LaTeX notation (default: session name)
   103     -n NAME      alternative session name (default: directory base name)
   105   Prepare session root directory (default: current directory).
   106 \<close>}
   108   The results are placed in the given directory \<open>dir\<close>, which refers to the
   109   current directory by default. The @{tool mkroot} tool is conservative in the
   110   sense that it does not overwrite existing files or directories. Earlier
   111   attempts to generate a session root need to be deleted manually.
   113   The generated session template will be accompanied by a formal document,
   114   with \<open>DIRECTORY\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see also
   115   \chref{ch:present}).
   117   Options \<^verbatim>\<open>-T\<close> and \<^verbatim>\<open>-A\<close> specify the document title and author explicitly,
   118   using {\LaTeX} source notation.
   120   Option \<^verbatim>\<open>-I\<close> initializes a Mercurial repository in the target directory, and
   121   adds all generated files (without commit).
   123   Option \<^verbatim>\<open>-n\<close> specifies an alternative session name; otherwise the base name
   124   of the given directory is used.
   126   \<^medskip>
   127   The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies
   128   the parent session.
   129 \<close>
   132 subsubsection \<open>Examples\<close>
   134 text \<open>
   135   Produce session \<^verbatim>\<open>Test\<close> within a separate directory of the same name:
   136   @{verbatim [display] \<open>isabelle mkroot Test && isabelle build -D Test\<close>}
   138   \<^medskip>
   139   Upgrade the current directory into a session ROOT with document preparation,
   140   and build it:
   141   @{verbatim [display] \<open>isabelle mkroot && isabelle build -D .\<close>}
   142 \<close>
   145 section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close>
   147 text \<open>
   148   The @{tool_def document} tool prepares logic session documents, processing
   149   the sources as provided by the user and generated by Isabelle. Its usage is:
   150   @{verbatim [display]
   151 \<open>Usage: isabelle document [OPTIONS]
   153   Options are:
   154     -d DIR       document output directory (default "output/document")
   155     -n NAME      document name (default "document")
   156     -o FORMAT    document format: pdf (default), dvi
   157     -t TAGS      markup for tagged regions
   159   Prepare the theory session document in document directory, producing the
   160   specified output format.
   161 \<close>}
   163   This tool is usually run automatically as part of the Isabelle build
   164   process, provided document preparation has been enabled via suitable
   165   options. It may be manually invoked on the generated browser information
   166   document output as well, e.g.\ in case of errors encountered in the batch
   167   run.
   169   \<^medskip>
   170   Option \<^verbatim>\<open>-d\<close> specifies an laternative document output directory. The default
   171   is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
   172   will appear in the parent of this directory.
   174   \<^medskip>
   175   The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format,
   176   the default is ``\<^verbatim>\<open>document.pdf\<close>''.
   178   \<^medskip>
   179   The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
   180   regions. Tags are specified as a comma separated list of modifier/name
   181   pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
   182   drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
   183   equivalent to the tag specification
   184   ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible,+important,+unimportant\<close>'';
   185   see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and
   186   \<^verbatim>\<open>\isafoldtag\<close>, in \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
   188   \<^medskip>
   189   Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session
   190   sources. This directory is supposed to contain all the files needed to
   191   produce the final document --- apart from the actual theories which are
   192   generated by Isabelle.
   194   \<^medskip>
   195   For most practical purposes, @{tool document} is smart enough to create any
   196   of the specified output formats, taking \<^verbatim>\<open>root.tex\<close> supplied by the user as
   197   a starting point. This even includes multiple runs of {\LaTeX} to
   198   accommodate references and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close>
   199   within the same directory).
   201   In more complex situations, a separate \<^verbatim>\<open>build\<close> script for the document
   202   sources may be given. It is invoked with command-line arguments for the
   203   document format and the document variant name. The script needs to produce
   204   corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and
   205   default variants). The main work can be again delegated to @{tool latex},
   206   but it is also possible to harvest generated {\LaTeX} sources and copy them
   207   elsewhere.
   209   \<^medskip>
   210   When running the session, Isabelle copies the content of the original
   211   \<^verbatim>\<open>document\<close> directory into its proper place within @{setting
   212   ISABELLE_BROWSER_INFO}, according to the session path and document variant.
   213   Then, for any processed theory \<open>A\<close> some {\LaTeX} source is generated and put
   214   there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>. Furthermore, a list of all generated theory files is
   215   put into \<^verbatim>\<open>session.tex\<close>. Typically, the root {\LaTeX} file provided by the
   216   user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the
   217   theories.
   219   The {\LaTeX} versions of the theories require some macros defined in
   220   \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
   221   \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an
   222   appropriate path specification for {\TeX} inputs.
   224   If the text contains any references to Isabelle symbols (such as \<^verbatim>\<open>\<forall>\<close>) then
   225   \<^verbatim>\<open>isabellesym.sty\<close> should be included as well. This package contains a
   226   standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to
   227   \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list
   228   of predefined Isabelle symbols. Users may invent further symbols as well,
   229   just by providing {\LaTeX} macros in a similar fashion as in
   230   \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution.
   232   For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),
   233   we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
   235   \<^medskip>
   236   As a final step of Isabelle document preparation, @{tool document} is run on
   237   the generated \<^verbatim>\<open>output/document\<close> directory. Thus the actual output document
   238   is built and installed in its proper place. The generated sources are
   239   deleted after successful run of {\LaTeX} and friends.
   241   Some care is needed if the document output location is configured
   242   differently, say within a directory whose content is still required
   243   afterwards!
   244 \<close>
   247 section \<open>Running {\LaTeX} within the Isabelle environment
   248   \label{sec:tool-latex}\<close>
   250 text \<open>
   251   The @{tool_def latex} tool provides the basic interface for Isabelle
   252   document preparation. Its usage is:
   253   @{verbatim [display]
   254 \<open>Usage: isabelle latex [OPTIONS] [FILE]
   256   Options are:
   257     -o FORMAT    specify output format: pdf (default), dvi,
   258                  bbl, idx, sty, syms
   260   Run LaTeX (and related tools) on FILE (default root.tex),
   261   producing the specified output format.\<close>}
   263   Appropriate {\LaTeX}-related programs are run on the input file, according
   264   to the given output format: @{executable latex}, @{executable pdflatex},
   265   @{executable dvips}, @{executable bibtex} (for \<^verbatim>\<open>bbl\<close>), and @{executable
   266   makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands are determined from the
   267   settings environment (@{setting ISABELLE_PDFLATEX} etc.).
   269   The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from
   270   the distribution. This is useful in special situations where the document
   271   sources are to be processed another time by separate tools.
   273   The \<^verbatim>\<open>syms\<close> output is for internal use; it generates lists of symbols that
   274   are available without loading additional {\LaTeX} packages.
   275 \<close>
   278 subsubsection \<open>Examples\<close>
   280 text \<open>
   281   Invoking @{tool latex} by hand may be occasionally useful when debugging
   282   failed attempts of the automatic document preparation stage of batch-mode
   283   Isabelle. The abortive process leaves the sources at a certain place within
   284   @{setting ISABELLE_BROWSER_INFO}, see the runtime error message for details.
   285   This enables users to inspect {\LaTeX} runs in further detail, e.g.\ like
   286   this:
   288   @{verbatim [display]
   289 \<open>cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
   290 isabelle latex -o pdf\<close>}
   291 \<close>
   293 end