src/Doc/System/Presentation.thy
 author wenzelm Sat Nov 11 14:55:30 2017 +0100 (18 months ago) changeset 67042 677cab7c2b85 parent 63680 6e1e8b5abbfa child 67043 848672fcaee5 permissions -rw-r--r--
adapted to changed ROOT syntax (see 13857f49d215);
discontinued pointless option -d: always enabled;
     1 (*:maxLineLen=78:*)

     2

     3 theory Presentation

     4 imports Base

     5 begin

     6

     7 chapter \<open>Presenting theories \label{ch:present}\<close>

     8

     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.

    17

    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}.

    24

    25   \begin{figure}[htbp]

    26   \begin{center}

    27   \begin{tabular}{lp{0.6\textwidth}}

    28

    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; \\

    32

    33       @{tool_ref build} & invoked repeatedly by the user to keep

    34       session output up-to-date (HTML, documents etc.); \\

    35

    36       @{tool_ref process} & run through @{tool_ref build}; \\

    37

    38       @{tool_ref document} & run by the Isabelle process if document

    39       preparation is enabled; \\

    40

    41       @{tool_ref latex} & universal {\LaTeX} tool wrapper invoked

    42       multiple times by @{tool_ref document}; also useful for manual

    43       experiments; \\

    44

    45   \end{tabular}

    46   \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}

    47   \end{center}

    48   \end{figure}

    49 \<close>

    50

    51

    52 section \<open>Generating HTML browser information \label{sec:info}\<close>

    53

    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.

    63

    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>}

    68

    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.   71   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>}   76   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.   81   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>   89   90   91 section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close>   92   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] [DIR]   98   99 Options are:   100 -n NAME alternative session name (default: DIR base name)   101   102 Prepare session root DIR (default: current directory).\<close>}   103   104 The results are placed in the given directory \<open>dir\<close>, which refers to the   105 current directory by default. The @{tool mkroot} tool is conservative in the   106 sense that it does not overwrite existing files or directories. Earlier   107 attempts to generate a session root need to be deleted manually.   108   109 The generated session template will be accompanied by a formal document,   110 with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see also   111 \chref{ch:present}).   112   113 Option \<^verbatim>\<open>-n\<close> allows to specify an alternative session name; otherwise the   114 base name of the given directory is used.   115   116 \<^medskip>   117 The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies   118 the parent session, and @{setting ISABELLE_DOCUMENT_FORMAT} the document   119 format to be filled filled into the generated \<^verbatim>\<open>ROOT\<close> file.   120 \<close>   121   122   123 subsubsection \<open>Examples\<close>   124   125 text \<open>   126 Produce session \<^verbatim>\<open>Test\<close> within a separate directory of the same name:   127 @{verbatim [display] \<open>isabelle mkroot Test && isabelle build -D Test\<close>}   128   129 \<^medskip>   130 Upgrade the current directory into a session ROOT with document preparation,   131 and build it:   132 @{verbatim [display] \<open>isabelle mkroot && isabelle build -D .\<close>}   133 \<close>   134   135   136 section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close>   137   138 text \<open>   139 The @{tool_def document} tool prepares logic session documents, processing   140 the sources as provided by the user and generated by Isabelle. Its usage is:   141 @{verbatim [display]   142 \<open>Usage: isabelle document [OPTIONS] [DIR]   143   144 Options are:   145 -c cleanup -- be aggressive in removing old stuff   146 -n NAME specify document name (default 'document')   147 -o FORMAT specify output format: pdf (default), dvi   148 -t TAGS specify tagged region markup   149   150 Prepare the theory session document in DIR (default 'document')   151 producing the specified output format.\<close>}   152   153 This tool is usually run automatically as part of the Isabelle build   154 process, provided document preparation has been enabled via suitable   155 options. It may be manually invoked on the generated browser information   156 document output as well, e.g.\ in case of errors encountered in the batch   157 run.   158   159 \<^medskip>   160 The \<^verbatim>\<open>-c\<close> option tells @{tool document} to dispose the document sources   161 after successful operation! This is the right thing to do for sources   162 generated by an Isabelle process, but take care of your files in manual   163 document preparation!   164   165 \<^medskip>   166 The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format,   167 the default is \<^verbatim>\<open>document.dvi\<close>''. Note that the result will appear in the   168 parent of the target \<^verbatim>\<open>DIR\<close>.   169   170 \<^medskip>   171 The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command   172 regions. Tags are specified as a comma separated list of modifier/name   173 pairs: \<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just \<open>foo\<close>'') means to keep, \<^verbatim>\<open>-\<close>\<open>foo\<close>'' to   174 drop, and \<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is   175 equivalent to the tag specification   176 \<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros   177 \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in   178 \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.   179   180 \<^medskip>   181 Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session   182 sources. This directory is supposed to contain all the files needed to   183 produce the final document --- apart from the actual theories which are   184 generated by Isabelle.   185   186 \<^medskip>   187 For most practical purposes, @{tool document} is smart enough to create any   188 of the specified output formats, taking \<^verbatim>\<open>root.tex\<close> supplied by the user as   189 a starting point. This even includes multiple runs of {\LaTeX} to   190 accommodate references and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close>   191 within the same directory).   192   193 In more complex situations, a separate \<^verbatim>\<open>build\<close> script for the document   194 sources may be given. It is invoked with command-line arguments for the   195 document format and the document variant name. The script needs to produce   196 corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and   197 default variants). The main work can be again delegated to @{tool latex},   198 but it is also possible to harvest generated {\LaTeX} sources and copy them   199 elsewhere.   200   201 \<^medskip>   202 When running the session, Isabelle copies the content of the original   203 \<^verbatim>\<open>document\<close> directory into its proper place within @{setting   204 ISABELLE_BROWSER_INFO}, according to the session path and document variant.   205 Then, for any processed theory \<open>A\<close> some {\LaTeX} source is generated and put   206 there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>. Furthermore, a list of all generated theory files is   207 put into \<^verbatim>\<open>session.tex\<close>. Typically, the root {\LaTeX} file provided by the   208 user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the   209 theories.   210   211 The {\LaTeX} versions of the theories require some macros defined in   212 \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in   213 \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an   214 appropriate path specification for {\TeX} inputs.   215   216 If the text contains any references to Isabelle symbols (such as \<^verbatim>\<open>\<forall>\<close>) then   217 \<^verbatim>\<open>isabellesym.sty\<close> should be included as well. This package contains a   218 standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to   219 \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list   220 of predefined Isabelle symbols. Users may invent further symbols as well,   221 just by providing {\LaTeX} macros in a similar fashion as in   222 \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution.   223   224 For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),   225 we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.   226   227 \<^medskip>   228 As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is   229 run on the resulting copy of the \<^verbatim>\<open>document\<close> directory. Thus the actual   230 output document is built and installed in its proper place. The generated   231 sources are deleted after successful run of {\LaTeX} and friends.   232   233 Some care is needed if the document output location is configured   234 differently, say within a directory whose content is still required   235 afterwards!   236 \<close>   237   238   239 section \<open>Running {\LaTeX} within the Isabelle environment   240 \label{sec:tool-latex}\<close>   241   242 text \<open>   243 The @{tool_def latex} tool provides the basic interface for Isabelle   244 document preparation. Its usage is:   245 @{verbatim [display]   246 \<open>Usage: isabelle latex [OPTIONS] [FILE]   247   248 Options are:   249 -o FORMAT specify output format: pdf (default), dvi,   250 bbl, idx, sty, syms   251   252 Run LaTeX (and related tools) on FILE (default root.tex),   253 producing the specified output format.\<close>}   254   255 Appropriate {\LaTeX}-related programs are run on the input file, according   256 to the given output format: @{executable latex}, @{executable pdflatex},   257 @{executable dvips}, @{executable bibtex} (for \<^verbatim>\<open>bbl\<close>), and @{executable   258 makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands are determined from the   259 settings environment (@{setting ISABELLE_PDFLATEX} etc.).   260   261 The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from   262 the distribution. This is useful in special situations where the document   263 sources are to be processed another time by separate tools.   264   265 The \<^verbatim>\<open>syms\<close> output is for internal use; it generates lists of symbols that   266 are available without loading additional {\LaTeX} packages.   267 \<close>   268   269   270 subsubsection \<open>Examples\<close>   271   272 text \<open>   273 Invoking @{tool latex} by hand may be occasionally useful when debugging   274 failed attempts of the automatic document preparation stage of batch-mode   275 Isabelle. The abortive process leaves the sources at a certain place within   276 @{setting ISABELLE_BROWSER_INFO}, see the runtime error message for details.   277 This enables users to inspect {\LaTeX} runs in further detail, e.g.\ like   278 this:   279   280 @{verbatim [display]   281 \<open>cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"

   282 isabelle latex -o pdf\<close>}

   283 \<close>

   284

   285 end
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 1, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.8745826482772827, "perplexity": 15729.081464248233}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.3, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2019-22/segments/1558232256494.24/warc/CC-MAIN-20190521162634-20190521184634-00041.warc.gz"}