src/Doc/System/Presentation.thy
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 58618 782f0b662cae
child 61406 eb2463fc4d7b
permissions -rw-r--r--
tuned signature;
     1 theory Presentation
     2 imports Base
     3 begin
     4 
     5 chapter \<open>Presenting theories \label{ch:present}\<close>
     6 
     7 text \<open>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 \<close>
    49 
    50 
    51 section \<open>Generating theory browser information \label{sec:info}\<close>
    52 
    53 text \<open>
    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.\<close>
   107 
   108 section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close>
   109 
   110 text \<open>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.\<close>
   141 
   142 
   143 subsubsection \<open>Examples\<close>
   144 
   145 text \<open>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 \<close>
   157 
   158 
   159 section \<open>Preparing Isabelle session documents
   160   \label{sec:tool-document}\<close>
   161 
   162 text \<open>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: pdf (default), dvi
   172     -t TAGS      specify tagged region markup
   173 
   174   Prepare the theory session document in DIR (default 'document')
   175   producing the specified output format.
   176 \end{ttbox}
   177   This tool is usually run automatically as part of the Isabelle build
   178   process, provided document preparation has been enabled via suitable
   179   options.  It may be manually invoked on the generated browser
   180   information document output as well, e.g.\ in case of errors
   181   encountered in the batch run.
   182 
   183   \medskip The @{verbatim "-c"} option tells @{tool document} to
   184   dispose the document sources after successful operation!  This is
   185   the right thing to do for sources generated by an Isabelle process,
   186   but take care of your files in manual document preparation!
   187 
   188   \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify
   189   the final output file name and format, the default is ``@{verbatim
   190   document.dvi}''.  Note that the result will appear in the parent of
   191   the target @{verbatim DIR}.
   192 
   193   \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret
   194   tagged Isabelle command regions.  Tags are specified as a comma
   195   separated list of modifier/name pairs: ``@{verbatim "+"}@{text
   196   foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim
   197   "-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to
   198   fold text tagged as @{text foo}.  The builtin default is equivalent
   199   to the tag specification ``@{verbatim
   200   "+theory,+proof,+ML,+visible,-invisible"}''; see also the {\LaTeX}
   201   macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
   202   @{verbatim "\\isafoldtag"}, in @{file
   203   "~~/lib/texinputs/isabelle.sty"}.
   204 
   205   \medskip Document preparation requires a @{verbatim document}
   206   directory within the session sources.  This directory is supposed to
   207   contain all the files needed to produce the final document --- apart
   208   from the actual theories which are generated by Isabelle.
   209 
   210   \medskip For most practical purposes, @{tool document} is smart
   211   enough to create any of the specified output formats, taking
   212   @{verbatim root.tex} supplied by the user as a starting point.  This
   213   even includes multiple runs of {\LaTeX} to accommodate references
   214   and bibliographies (the latter assumes @{verbatim root.bib} within
   215   the same directory).
   216 
   217   In more complex situations, a separate @{verbatim build} script for
   218   the document sources may be given.  It is invoked with command-line
   219   arguments for the document format and the document variant name.
   220   The script needs to produce corresponding output files, e.g.\
   221   @{verbatim root.pdf} for target format @{verbatim pdf} (and default
   222   variants).  The main work can be again delegated to @{tool latex},
   223   but it is also possible to harvest generated {\LaTeX} sources and
   224   copy them elsewhere.
   225 
   226   \medskip When running the session, Isabelle copies the content of
   227   the original @{verbatim document} directory into its proper place
   228   within @{setting ISABELLE_BROWSER_INFO}, according to the session
   229   path and document variant.  Then, for any processed theory @{text A}
   230   some {\LaTeX} source is generated and put there as @{text
   231   A}@{verbatim ".tex"}.  Furthermore, a list of all generated theory
   232   files is put into @{verbatim session.tex}.  Typically, the root
   233   {\LaTeX} file provided by the user would include @{verbatim
   234   session.tex} to get a document containing all the theories.
   235 
   236   The {\LaTeX} versions of the theories require some macros defined in
   237   @{file "~~/lib/texinputs/isabelle.sty"}.  Doing @{verbatim
   238   "\\usepackage{isabelle}"} in @{verbatim root.tex} should be fine;
   239   the underlying @{tool latex} already includes an appropriate path
   240   specification for {\TeX} inputs.
   241 
   242   If the text contains any references to Isabelle symbols (such as
   243   @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim
   244   "isabellesym.sty"} should be included as well.  This package
   245   contains a standard set of {\LaTeX} macro definitions @{verbatim
   246   "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
   247   "<"}@{text foo}@{verbatim ">"}, see @{cite "isabelle-implementation"} for a
   248   complete list of predefined Isabelle symbols.  Users may invent
   249   further symbols as well, just by providing {\LaTeX} macros in a
   250   similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of
   251   the Isabelle distribution.
   252 
   253   For proper setup of DVI and PDF documents (with hyperlinks and
   254   bookmarks), we recommend to include @{file
   255   "~~/lib/texinputs/pdfsetup.sty"} as well.
   256 
   257   \medskip As a final step of Isabelle document preparation, @{tool
   258   document}~@{verbatim "-c"} is run on the resulting copy of the
   259   @{verbatim document} directory.  Thus the actual output document is
   260   built and installed in its proper place.  The generated sources are
   261   deleted after successful run of {\LaTeX} and friends.
   262 
   263   Some care is needed if the document output location is configured
   264   differently, say within a directory whose content is still required
   265   afterwards!
   266 \<close>
   267 
   268 
   269 section \<open>Running {\LaTeX} within the Isabelle environment
   270   \label{sec:tool-latex}\<close>
   271 
   272 text \<open>The @{tool_def latex} tool provides the basic interface for
   273   Isabelle document preparation.  Its usage is:
   274 \begin{ttbox}
   275 Usage: isabelle latex [OPTIONS] [FILE]
   276 
   277   Options are:
   278     -o FORMAT    specify output format: pdf (default), dvi,
   279                  bbl, idx, sty, syms
   280 
   281   Run LaTeX (and related tools) on FILE (default root.tex),
   282   producing the specified output format.
   283 \end{ttbox}
   284 
   285   Appropriate {\LaTeX}-related programs are run on the input file,
   286   according to the given output format: @{executable latex},
   287   @{executable pdflatex}, @{executable dvips}, @{executable bibtex}
   288   (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim
   289   idx}).  The actual commands are determined from the settings
   290   environment (@{setting ISABELLE_PDFLATEX} etc.).
   291 
   292   The @{verbatim sty} output format causes the Isabelle style files to
   293   be updated from the distribution.  This is useful in special
   294   situations where the document sources are to be processed another
   295   time by separate tools.
   296 
   297   The @{verbatim syms} output is for internal use; it generates lists
   298   of symbols that are available without loading additional {\LaTeX}
   299   packages.
   300 \<close>
   301 
   302 
   303 subsubsection \<open>Examples\<close>
   304 
   305 text \<open>Invoking @{tool latex} by hand may be occasionally useful when
   306   debugging failed attempts of the automatic document preparation
   307   stage of batch-mode Isabelle.  The abortive process leaves the
   308   sources at a certain place within @{setting ISABELLE_BROWSER_INFO},
   309   see the runtime error message for details.  This enables users to
   310   inspect {\LaTeX} runs in further detail, e.g.\ like this:
   311 
   312 \begin{ttbox}
   313   cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
   314   isabelle latex -o pdf
   315 \end{ttbox}
   316 \<close>
   317 
   318 end