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