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