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