author wenzelm
Wed Dec 06 21:30:26 2017 +0100 (6 weeks ago)
changeset 67151 d1ace598c026
parent 67139 8fe0aba577af
child 67176 13b5c3ff1954
permissions -rw-r--r--
more default tags;
     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 \<^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>}
    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] [DIR]
   153   Options are:
   154     -c           cleanup -- be aggressive in removing old stuff
   155     -n NAME      specify document name (default 'document')
   156     -o FORMAT    specify output format: pdf (default), dvi
   157     -t TAGS      specify tagged region markup
   159   Prepare the theory session document in DIR (default 'document')
   160   producing the specified output format.\<close>}
   162   This tool is usually run automatically as part of the Isabelle build
   163   process, provided document preparation has been enabled via suitable
   164   options. It may be manually invoked on the generated browser information
   165   document output as well, e.g.\ in case of errors encountered in the batch
   166   run.
   168   \<^medskip>
   169   The \<^verbatim>\<open>-c\<close> option tells @{tool document} to dispose the document sources
   170   after successful operation! This is the right thing to do for sources
   171   generated by an Isabelle process, but take care of your files in manual
   172   document preparation!
   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.dvi\<close>''. Note that the result will appear in the
   177   parent of the target \<^verbatim>\<open>DIR\<close>.
   179   \<^medskip>
   180   The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
   181   regions. Tags are specified as a comma separated list of modifier/name
   182   pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
   183   drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
   184   equivalent to the tag specification
   185   ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible,+important,+unimportant\<close>'';
   186   see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and
   187   \<^verbatim>\<open>\isafoldtag\<close>, in \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
   189   \<^medskip>
   190   Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session
   191   sources. This directory is supposed to contain all the files needed to
   192   produce the final document --- apart from the actual theories which are
   193   generated by Isabelle.
   195   \<^medskip>
   196   For most practical purposes, @{tool document} is smart enough to create any
   197   of the specified output formats, taking \<^verbatim>\<open>root.tex\<close> supplied by the user as
   198   a starting point. This even includes multiple runs of {\LaTeX} to
   199   accommodate references and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close>
   200   within the same directory).
   202   In more complex situations, a separate \<^verbatim>\<open>build\<close> script for the document
   203   sources may be given. It is invoked with command-line arguments for the
   204   document format and the document variant name. The script needs to produce
   205   corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and
   206   default variants). The main work can be again delegated to @{tool latex},
   207   but it is also possible to harvest generated {\LaTeX} sources and copy them
   208   elsewhere.
   210   \<^medskip>
   211   When running the session, Isabelle copies the content of the original
   212   \<^verbatim>\<open>document\<close> directory into its proper place within @{setting
   213   ISABELLE_BROWSER_INFO}, according to the session path and document variant.
   214   Then, for any processed theory \<open>A\<close> some {\LaTeX} source is generated and put
   215   there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>. Furthermore, a list of all generated theory files is
   216   put into \<^verbatim>\<open>session.tex\<close>. Typically, the root {\LaTeX} file provided by the
   217   user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the
   218   theories.
   220   The {\LaTeX} versions of the theories require some macros defined in
   221   \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
   222   \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an
   223   appropriate path specification for {\TeX} inputs.
   225   If the text contains any references to Isabelle symbols (such as \<^verbatim>\<open>\<forall>\<close>) then
   226   \<^verbatim>\<open>isabellesym.sty\<close> should be included as well. This package contains a
   227   standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to
   228   \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list
   229   of predefined Isabelle symbols. Users may invent further symbols as well,
   230   just by providing {\LaTeX} macros in a similar fashion as in
   231   \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution.
   233   For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),
   234   we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
   236   \<^medskip>
   237   As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
   238   run on the resulting copy of the \<^verbatim>\<open>document\<close> directory. Thus the actual
   239   output document is built and installed in its proper place. The generated
   240   sources are deleted after successful run of {\LaTeX} and friends.
   242   Some care is needed if the document output location is configured
   243   differently, say within a directory whose content is still required
   244   afterwards!
   245 \<close>
   248 section \<open>Running {\LaTeX} within the Isabelle environment
   249   \label{sec:tool-latex}\<close>
   251 text \<open>
   252   The @{tool_def latex} tool provides the basic interface for Isabelle
   253   document preparation. Its usage is:
   254   @{verbatim [display]
   255 \<open>Usage: isabelle latex [OPTIONS] [FILE]
   257   Options are:
   258     -o FORMAT    specify output format: pdf (default), dvi,
   259                  bbl, idx, sty, syms
   261   Run LaTeX (and related tools) on FILE (default root.tex),
   262   producing the specified output format.\<close>}
   264   Appropriate {\LaTeX}-related programs are run on the input file, according
   265   to the given output format: @{executable latex}, @{executable pdflatex},
   266   @{executable dvips}, @{executable bibtex} (for \<^verbatim>\<open>bbl\<close>), and @{executable
   267   makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands are determined from the
   268   settings environment (@{setting ISABELLE_PDFLATEX} etc.).
   270   The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from
   271   the distribution. This is useful in special situations where the document
   272   sources are to be processed another time by separate tools.
   274   The \<^verbatim>\<open>syms\<close> output is for internal use; it generates lists of symbols that
   275   are available without loading additional {\LaTeX} packages.
   276 \<close>
   279 subsubsection \<open>Examples\<close>
   281 text \<open>
   282   Invoking @{tool latex} by hand may be occasionally useful when debugging
   283   failed attempts of the automatic document preparation stage of batch-mode
   284   Isabelle. The abortive process leaves the sources at a certain place within
   285   @{setting ISABELLE_BROWSER_INFO}, see the runtime error message for details.
   286   This enables users to inspect {\LaTeX} runs in further detail, e.g.\ like
   287   this:
   289   @{verbatim [display]
   290 \<open>cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
   291 isabelle latex -o pdf\<close>}
   292 \<close>
   294 end