doc-src/System/Thy/Presentation.thy
 author wenzelm Sat Oct 04 17:40:56 2008 +0200 (2008-10-04 ago) changeset 28504 7ad7d7d6df47 parent 28238 398bf960d3d4 child 28838 d5db6dfcb34a permissions -rw-r--r--
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
     1 (* $Id$ *)

     2

     3 theory Presentation

     4 imports Pure

     5 begin

     6

     7 chapter {* Presenting theories \label{ch:present} *}

     8

     9 text {*

    10   Isabelle provides several ways to present the outcome of formal

    11   developments, including WWW-based browsable libraries or actual

    12   printable documents.  Presentation is centered around the concept of

    13   \emph{logic sessions}.  The global session structure is that of a

    14   tree, with Isabelle Pure at its root, further object-logics derived

    15   (e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions

    16   in leaf positions (usually without a separate image).

    17

    18   The Isabelle tools @{tool_ref mkdir} and @{tool_ref make} provide

    19   the primary means for managing Isabelle sessions, including proper

    20   setup for presentation.  Here the @{tool_ref usedir} tool takes care

    21   to let @{executable_ref "isabelle-process"} process run any

    22   additional stages required for document preparation, notably the

    23   tools @{tool_ref document} and @{tool_ref latex}.  The complete tool

    24   chain for managing batch-mode Isabelle sessions is illustrated in

    25   \figref{fig:session-tools}.

    26

    27   \begin{figure}[htbp]

    28   \begin{center}

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

    30

    31       @{verbatim isabelle} @{tool_ref mkdir} & invoked once by the user

    32       to create the initial source setup (common @{verbatim

    33       IsaMakefile} plus a single session directory); \\

    34

    35       @{verbatim isabelle} @{tool make} & invoked repeatedly by the

    36       user to keep session output up-to-date (HTML, documents etc.); \\

    37

    38       @{verbatim isabelle} @{tool usedir} & part of the standard

    39       @{verbatim IsaMakefile} entry of a session; \\

    40

    41       @{executable "isabelle-process"} & run through @{verbatim

    42       isabelle} @{tool_ref usedir}; \\

    43

    44       @{verbatim isabelle} @{tool_ref document} & run by the Isabelle

    45       process if document preparation is enabled; \\

    46

    47       @{verbatim isabelle} @{tool_ref latex} & universal {\LaTeX} tool

    48       wrapper invoked multiple times by @{verbatim isabelle} @{tool_ref

    49       document}; also useful for manual experiments; \\

    50

    51   \end{tabular}

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

    53   \end{center}

    54   \end{figure}

    55 *}

    56

    57

    58 section {* Generating theory browser information \label{sec:info} *}

    59

    60 text {*

    61   \index{theory browsing information|bold}

    62

    63   As a side-effect of running a logic sessions, Isabelle is able to

    64   generate theory browsing information, including HTML documents that

    65   show a theory's definition, the theorems proved in its ML file and

    66   the relationship with its ancestors and descendants.  Besides the

    67   HTML file that is generated for every theory, Isabelle stores links

    68   to all theories in an index file. These indexes are linked with

    69   other indexes to represent the overall tree structure of logic

    70   sessions.

    71

    72   Isabelle also generates graph files that represent the theory

    73   hierarchy of a logic.  There is a graph browser Java applet embedded

    74   in the generated HTML pages, and also a stand-alone application that

    75   allows browsing theory graphs without having to start a WWW client

    76   first.  The latter version also includes features such as generating

    77   Postscript files, which are not available in the applet version.

    78   See \secref{sec:browse} for further information.

    79

    80   \medskip

    81

    82   The easiest way to let Isabelle generate theory browsing information

    83   for existing sessions is to append @{verbatim "-i true"}'' to the

    84   @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim

    85   isabelle} @{tool make} (or @{"file" "$ISABELLE_HOME/build"}). For   86 example, add something like this to your Isabelle settings file   87   88 \begin{ttbox}   89 ISABELLE_USEDIR_OPTIONS="-i true"   90 \end{ttbox}   91   92 and then change into the @{"file" "~~/src/FOL"} directory and run   93 @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle} @{tool   94 make}~@{verbatim all}. The presentation output will appear in   95 @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to   96 @{verbatim "~/isabelle/browser_info/FOL"}. Note that option   97 @{verbatim "-v true"} will make the internal runs of @{tool usedir}   98 more explicit about such details.   99   100 Many standard Isabelle sessions (such as @{"file" "~~/src/HOL/ex"})   101 also provide actual printable documents. These are prepared   102 automatically as well if enabled like this, using the @{verbatim   103 "-d"} option   104 \begin{ttbox}   105 ISABELLE_USEDIR_OPTIONS="-i true -d dvi"   106 \end{ttbox}   107 Enabling options @{verbatim "-i"} and @{verbatim "-d"}   108 simultaneously as shown above causes an appropriate document''   109 link to be included in the HTML index. Documents (or raw document   110 sources) may be generated independently of browser information as   111 well, see \secref{sec:tool-document} for further details.   112   113 \bigskip The theory browsing information is stored in a   114 sub-directory directory determined by the @{setting_ref   115 ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the   116 session identifier (according to the tree structure of sub-sessions   117 by default). A complete WWW view of all standard object-logics and   118 examples of the Isabelle distribution is available at the usual   119 Isabelle sites:   120 \begin{center}\small   121 \begin{tabular}{l}   122 \url{http://isabelle.in.tum.de/dist/library/} \\   123 \url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/} \\   124 \url{http://mirror.cse.unsw.edu.au/pub/isabelle/dist/library/} \\   125 \end{tabular}   126 \end{center}   127   128 \medskip In order to present your own theories on the web, simply   129 copy the corresponding subdirectory from @{setting   130 ISABELLE_BROWSER_INFO} to your WWW server, having generated browser   131 info like this:   132 \begin{ttbox}   133 isabelle usedir -i true HOL Foo   134 \end{ttbox}   135   136 This assumes that directory @{verbatim Foo} contains some @{verbatim   137 ROOT.ML} file to load all your theories, and HOL is your parent   138 logic image (@{verbatim isabelle} @{tool_ref mkdir} assists in   139 setting up Isabelle session directories. Theory browser information   140 for HOL should have been generated already beforehand.   141 Alternatively, one may specify an external link to an existing body   142 of HTML data by giving @{tool usedir} a @{verbatim "-P"} option like   143 this:   144 \begin{ttbox}   145 isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo   146 \end{ttbox}   147   148 \medskip For production use, the @{tool usedir} tool is usually   149 invoked in an appropriate @{verbatim IsaMakefile}, via the Isabelle   150 @{tool make} tool. There is a separate @{tool mkdir} tool to   151 provide easy setup of all this, with only minimal manual editing   152 required.   153 \begin{ttbox}   154 isabelle mkdir HOL Foo && isabelle make   155 \end{ttbox}   156 See \secref{sec:tool-mkdir} for more information on preparing   157 Isabelle session directories, including the setup for documents.   158 *}   159   160   161 section {* Browsing theory graphs \label{sec:browse} *}   162   163 text {*   164 \index{theory graph browser|bold}   165   166 The Isabelle graph browser is a general tool for visualizing   167 dependency graphs. Certain nodes of the graph (i.e.~theories) can   168 be grouped together in directories'', whose contents may be   169 hidden, thus enabling the user to collapse irrelevant portions of   170 information. The browser is written in Java, it can be used both as   171 a stand-alone application and as an applet. Note that the option   172 @{verbatim "-g"} of @{verbatim isabelle} @{tool_ref usedir} creates   173 graph presentations in batch mode for inclusion in session   174 documents.   175 *}   176   177   178 subsection {* Invoking the graph browser *}   179   180 text {*   181 The stand-alone version of the graph browser is wrapped up as an   182 Isabelle tool called @{tool_def browser}:   183   184 \begin{ttbox}   185 Usage: browser [OPTIONS] [GRAPHFILE]   186   187 Options are:   188 -c cleanup -- remove GRAPHFILE after use   189 -o FILE output to FILE (ps, eps, pdf)   190 \end{ttbox}   191 When no filename is specified, the browser automatically changes to   192 the directory @{setting ISABELLE_BROWSER_INFO}.   193   194 \medskip The @{verbatim "-c"} option causes the input file to be   195 removed after use.   196   197 The @{verbatim "-o"} option indicates batch-mode operation, with the   198 output written to the indicated file; note that @{verbatim pdf}   199 produces an @{verbatim eps} copy as well.   200   201 \medskip The applet version of the browser is part of the standard   202 WWW theory presentation, see the link theory dependencies'' within   203 each session index.   204 *}   205   206   207 subsection {* Using the graph browser *}   208   209 text {*   210 The browser's main window, which is shown in   211 \figref{fig:browserwindow}, consists of two sub-windows. In the   212 left sub-window, the directory tree is displayed. The graph itself   213 is displayed in the right sub-window.   214   215 \begin{figure}[ht]   216 \includegraphics[width=\textwidth]{browser_screenshot}   217 \caption{\label{fig:browserwindow} Browser main window}   218 \end{figure}   219 *}   220   221   222 subsubsection {* The directory tree window *}   223   224 text {*   225 We describe the usage of the directory browser and the meaning of   226 the different items in the browser window.   227   228 \begin{itemize}   229   230 \item A red arrow before a directory name indicates that the   231 directory is currently folded'', i.e.~the nodes in this directory   232 are collapsed to one single node. In the right sub-window, the names   233 of nodes corresponding to folded directories are enclosed in square   234 brackets and displayed in red color.   235   236 \item A green downward arrow before a directory name indicates that   237 the directory is currently unfolded''. It can be folded by   238 clicking on the directory name. Clicking on the name for a second   239 time unfolds the directory again. Alternatively, a directory can   240 also be unfolded by clicking on the corresponding node in the right   241 sub-window.   242   243 \item Blue arrows stand before ordinary node names. When clicking on   244 such a name (i.e.\ that of a theory), the graph display window   245 focuses to the corresponding node. Double clicking invokes a text   246 viewer window in which the contents of the theory file are   247 displayed.   248   249 \end{itemize}   250 *}   251   252   253 subsubsection {* The graph display window *}   254   255 text {*   256 When pointing on an ordinary node, an upward and a downward arrow is   257 shown. Initially, both of these arrows are green. Clicking on the   258 upward or downward arrow collapses all predecessor or successor   259 nodes, respectively. The arrow's color then changes to red,   260 indicating that the predecessor or successor nodes are currently   261 collapsed. The node corresponding to the collapsed nodes has the   262 name @{verbatim "[....]"}''. To uncollapse the nodes again, simply   263 click on the red arrow or on the node with the name @{verbatim   264 "[....]"}''. Similar to the directory browser, the contents of   265 theory files can be displayed by double clicking on the   266 corresponding node.   267 *}   268   269   270 subsubsection {* The File'' menu *}   271   272 text {*   273 Due to Java Applet security restrictions this menu is only available   274 in the full application version. The meaning of the menu items is as   275 follows:   276   277 \begin{description}   278   279 \item[Open \dots] Open a new graph file.   280   281 \item[Export to PostScript] Outputs the current graph in Postscript   282 format, appropriately scaled to fit on one single sheet of A4 paper.   283 The resulting file can be printed directly.   284   285 \item[Export to EPS] Outputs the current graph in Encapsulated   286 Postscript format. The resulting file can be included in other   287 documents.   288   289 \item[Quit] Quit the graph browser.   290   291 \end{description}   292 *}   293   294   295 subsection {* Syntax of graph definition files *}   296   297 text {*   298 A graph definition file has the following syntax:   299   300 \begin{center}\small   301 \begin{tabular}{rcl}   302 @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\   303 @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"}   304 \end{tabular}   305 \end{center}   306   307 The meaning of the items in a vertex description is as follows:   308   309 \begin{description}   310   311 \item[@{text vertex_name}] The name of the vertex.   312   313 \item[@{text vertex_ID}] The vertex identifier. Note that there may   314 be several vertices with equal names, whereas identifiers must be   315 unique.   316   317 \item[@{text dir_name}] The name of the directory'' the vertex   318 should be placed in. A @{verbatim "+"}'' sign after @{text   319 dir_name} indicates that the nodes in the directory are initially   320 visible. Directories are initially invisible by default.   321   322 \item[@{text path}] The path of the corresponding theory file. This   323 is specified relatively to the path of the graph definition file.   324   325 \item[List of successor/predecessor nodes] A @{verbatim "<"}''   326 sign before the list means that successor nodes are listed, a   327 @{verbatim ">"}'' sign means that predecessor nodes are listed. If   328 neither @{verbatim "<"}'' nor @{verbatim ">"}'' is found, the   329 browser assumes that successor nodes are listed.   330   331 \end{description}   332 *}   333   334   335 section {* Creating Isabelle session directories   336 \label{sec:tool-mkdir} *}   337   338 text {*   339 The @{tool_def mkdir} utility prepares Isabelle session source   340 directories, including a sensible default setup of @{verbatim   341 IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document}   342 directory with a minimal @{verbatim root.tex} that is sufficient to   343 print all theories of the session (in the order of appearance); see   344 \secref{sec:tool-document} for further information on Isabelle   345 document preparation. The usage of @{verbatim isabelle} @{tool   346 mkdir} is:   347   348 \begin{ttbox}   349 Usage: mkdir [OPTIONS] [LOGIC] NAME   350   351 Options are:   352 -I FILE alternative IsaMakefile output   353 -P include parent logic target   354 -b setup build mode (session outputs heap image)   355 -q quiet mode   356   357 Prepare session directory, including IsaMakefile and document source,   358 with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)

   359 \end{ttbox}

   360

   361   The @{tool mkdir} tool is conservative in the sense that any

   362   existing @{verbatim IsaMakefile} etc.\ is left unchanged.  Thus it

   363   is safe to invoke it multiple times, although later runs may not

   364   have the desired effect.

   365

   366   Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile}

   367   incrementally --- manual changes are required for multiple

   368   sub-sessions.  On order to get an initial working session, the only

   369   editing needed is to add appropriate @{ML use_thy} calls to the

   370   generated @{verbatim ROOT.ML} file.

   371 *}

   372

   373

   374 subsubsection {* Options *}

   375

   376 text {*

   377   The @{verbatim "-I"} option specifies an alternative to @{verbatim

   378   IsaMakefile} for dependencies.  Note that @{verbatim "-"}'' refers

   379   to \emph{stdout}, i.e.\ @{verbatim "-I-"}'' provides an easy way

   380   to peek at @{tool mkdir}'s idea of @{tool make} setup required for

   381   some particular of Isabelle session.

   382

   383   \medskip The @{verbatim "-P"} option includes a target for the

   384   parent @{verbatim LOGIC} session in the generated @{verbatim

   385   IsaMakefile}.  The corresponding sources are assumed to be located

   386   within the Isabelle distribution.

   387

   388   \medskip The @{verbatim "-b"} option sets up the current directory

   389   as the base for a new session that provides an actual logic image,

   390   as opposed to one that only runs several theories based on an

   391   existing image.  Note that in the latter case, everything except

   392   @{verbatim IsaMakefile} would be placed into a separate directory

   393   @{verbatim NAME}, rather than the current one.  See

   394   \secref{sec:tool-usedir} for further information on \emph{build

   395   mode} vs.\ \emph{example mode} of the @{tool usedir} utility.

   396

   397   \medskip The @{verbatim "-q"} option enables quiet mode, suppressing

   398   further notes on how to proceed.

   399 *}

   400

   401

   402 subsubsection {* Examples *}

   403

   404 text {*

   405   The standard setup of a single example session'' based on the

   406   default logic, with proper document generation is generated like

   407   this:

   408 \begin{ttbox}

   409 isabelle mkdir Foo && isabelle make

   410 \end{ttbox}

   411

   412   \noindent The theory sources should be put into the @{verbatim Foo}

   413   directory, and its @{verbatim ROOT.ML} should be edited to load all

   414   required theories.  Invoking @{verbatim isabelle} @{tool make} again

   415   would run the whole session, generating browser information and the

   416   document automatically.  The @{verbatim IsaMakefile} is typically

   417   tuned manually later, e.g.\ adding source dependencies, or changing

   418   the options passed to @{tool usedir}.

   419

   420   \medskip Large projects may demand further sessions, potentially

   421   with separate logic images being created.  This usually requires

   422   manual editing of the generated @{verbatim IsaMakefile}, which is

   423   meant to cover all of the sub-session directories at the same time

   424   (this is the deeper reasong why @{verbatim IsaMakefile} is not made

   425   part of the initial session directory created by @{verbatim

   426   isabelle} @{tool mkdir}).  See @{"file" "~~/src/HOL/IsaMakefile"} for

   427   a full-blown example.

   428 *}

   429

   430

   431 section {* Running Isabelle sessions \label{sec:tool-usedir} *}

   432

   433 text {*

   434   The @{tool_def usedir} utility builds object-logic images, or runs

   435   example sessions based on existing logics. Its usage is:

   436 \begin{ttbox}

   437

   438 Usage: usedir [OPTIONS] LOGIC NAME

   439

   440   Options are:

   441     -C BOOL      copy existing document directory to -D PATH (default true)

   442     -D PATH      dump generated document sources into PATH

   443     -M MAX       multithreading: maximum number of worker threads (default 1)

   444     -P PATH      set path for remote theory browsing information

   445     -T LEVEL     multithreading: trace level (default 0)

   446     -V VERSION   declare alternative document VERSION

   447     -b           build mode (output heap image, using current dir)

   448     -c BOOL      tell ML system to compress output image (default true)

   449     -d FORMAT    build document as FORMAT (default false)

   450     -f NAME      use ML file NAME (default ROOT.ML)

   451     -g BOOL      generate session graph image for document (default false)

   452     -i BOOL      generate theory browser information (default false)

   453     -m MODE      add print mode for output

   454     -p LEVEL     set level of detail for proof objects

   455     -r           reset session path

   456     -s NAME      override session NAME

   457     -v BOOL      be verbose (default false)

   458

   459   Build object-logic or run examples. Also creates browsing

   460   information (HTML etc.) according to settings.

   461

   462   ISABELLE_USEDIR_OPTIONS=

   463   HOL_USEDIR_OPTIONS=

   464 \end{ttbox}

   465

   466   Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}

   467   setting is implicitly prefixed to \emph{any} @{tool usedir}

   468   call. Since the @{verbatim IsaMakefile}s of all object-logics

   469   distributed with Isabelle just invoke @{tool usedir} for the real

   470   work, one may control compilation options globally via above

   471   variable. In particular, generation of \rmindex{HTML} browsing

   472   information and document preparation is controlled here.

   473

   474   The @{setting_ref HOL_USEDIR_OPTIONS} setting is specific to the

   475   plain and main Isabelle/HOL images; its value is appended to

   476   @{setting ISABELLE_USEDIR_OPTIONS} for these particular sessions

   477   only.

   478 *}

   479

   480

   481 subsubsection {* Options *}

   482

   483 text {*

   484   Basically, there are two different modes of operation: \emph{build

   485   mode} (enabled through the @{verbatim "-b"} option) and

   486   \emph{example mode} (default).

   487

   488   Calling @{tool usedir} with @{verbatim "-b"} runs @{executable

   489   "isabelle-process"} with input image @{verbatim LOGIC} and output to

   490   @{verbatim NAME}, as provided on the command line. This will be a

   491   batch session, running @{verbatim ROOT.ML} from the current

   492   directory and then quitting.  It is assumed that @{verbatim ROOT.ML}

   493   contains all ML commands required to build the logic.

   494

   495   In example mode, @{tool usedir} runs a read-only session of

   496   @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from

   497   within directory @{verbatim NAME}.  It assumes that this file

   498   contains appropriate ML commands to run the desired examples.

   499

   500   \medskip The @{verbatim "-i"} option controls theory browser data

   501   generation. It may be explicitly turned on or off --- as usual, the

   502   last occurrence of @{verbatim "-i"} on the command line wins.

   503

   504   The @{verbatim "-P"} option specifies a path (or actual URL) to be

   505   prefixed to any \emph{non-local} reference of existing theories.

   506   Thus user sessions may easily link to existing Isabelle libraries

   507   already present on the WWW.

   508

   509   The @{verbatim "-m"} options specifies additional print modes to be

   510   activated temporarily while the session is processed.

   511

   512   \medskip The @{verbatim "-d"} option controls document preparation.

   513   Valid arguments are @{verbatim false} (do not prepare any document;

   514   this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz},

   515   @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}.  The logic

   516   session has to provide a properly setup @{verbatim document}

   517   directory.  See \secref{sec:tool-document} and

   518   \secref{sec:tool-latex} for more details.

   519

   520   \medskip The @{verbatim "-V"} option declares alternative document

   521   versions, consisting of name/tags pairs (cf.\ options @{verbatim

   522   "-n"} and @{verbatim "-t"} of the @{tool_ref document} tool).  The

   523   standard document is equivalent to @{verbatim

   524   "document=theory,proof,ML"}'', which means that all theory begin/end

   525   commands, proof body texts, and ML code will be presented

   526   faithfully.  An alternative version @{verbatim

   527   "outline=/proof/ML"}'' would fold proof and ML parts, replacing the

   528   original text by a short place-holder.  The form @{text

   529   name}@{verbatim "=-"},'' means to remove document @{text name} from

   530   the list of versions to be processed.  Any number of @{verbatim

   531   "-V"} options may be given; later declarations have precedence over

   532   earlier ones.

   533

   534   \medskip The @{verbatim "-g"} option produces images of the theory

   535   dependency graph (cf.\ \secref{sec:browse}) for inclusion in the

   536   generated document, both as @{verbatim session_graph.eps} and

   537   @{verbatim session_graph.pdf} at the same time.  To include this in

   538   the final {\LaTeX} document one could say @{verbatim

   539   "\\includegraphics{session_graph}"} in @{verbatim

   540   "document/root.tex"} (omitting the file-name extension enables

   541   {\LaTeX} to select to correct version, either for the DVI or PDF

   542   output path).

   543

   544   \medskip The @{verbatim "-D"} option causes the generated document

   545   sources to be dumped at location @{verbatim PATH}; this path is

   546   relative to the session's main directory.  If the @{verbatim "-C"}

   547   option is true, this will include a copy of an existing @{verbatim

   548   document} directory as provided by the user.  For example,

   549   @{verbatim isabelle} @{tool usedir}~@{verbatim "-D generated HOL

   550   Foo"} produces a complete set of document sources at @{verbatim

   551   "Foo/generated"}.  Subsequent invocation of @{verbatim

   552   isabelle} @{tool document}~@{verbatim "Foo/generated"} (see also

   553   \secref{sec:tool-document}) will process the final result

   554   independently of an Isabelle job.  This decoupled mode of operation

   555   facilitates debugging of serious {\LaTeX} errors, for example.

   556

   557   \medskip The @{verbatim "-p"} option determines the level of detail

   558   for internal proof objects, see also the \emph{Isabelle Reference

   559   Manual}~\cite{isabelle-ref}.

   560

   561   \medskip The @{verbatim "-v"} option causes additional information

   562   to be printed while running the session, notably the location of

   563   prepared documents.

   564

   565   \medskip The @{verbatim "-M"} option specifies the maximum number of

   566   parallel threads used for processing independent tasks when checking

   567   theory sources (multithreading only works on suitable ML platforms).

   568   The special value of @{verbatim 0} or @{verbatim max} refers to the

   569   number of actual CPU cores of the underlying machine, which is a

   570   good starting point for optimal performance tuning.  The @{verbatim

   571   "-T"} option determines the level of detail in tracing output

   572   concerning the internal locking and scheduling in multithreaded

   573   operation.  This may be helpful in isolating performance

   574   bottle-necks, e.g.\ due to excessive wait states when locking

   575   critical code sections.

   576

   577   \medskip Any @{tool usedir} session is named by some \emph{session

   578   identifier}. These accumulate, documenting the way sessions depend

   579   on others. For example, consider @{verbatim "Pure/FOL/ex"}, which

   580   refers to the examples of FOL, which in turn is built upon Pure.

   581

   582   The current session's identifier is by default just the base name of

   583   the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim

   584   NAME} argument (in example mode). This may be overridden explicitly

   585   via the @{verbatim "-s"} option.

   586 *}

   587

   588

   589 subsubsection {* Examples *}

   590

   591 text {*

   592   Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's

   593   object-logics as a model for your own developments.  For example,

   594   see @{"file" "~~/src/FOL/IsaMakefile"}.  The Isabelle @{tool_ref

   595   mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation

   596   of @{tool usedir} as well.

   597 *}

   598

   599

   600 section {* Preparing Isabelle session documents

   601   \label{sec:tool-document} *}

   602

   603 text {*

   604   The @{tool_def document} utility prepares logic session documents,

   605   processing the sources both as provided by the user and generated by

   606   Isabelle.  Its usage is:

   607 \begin{ttbox}

   608 Usage: document [OPTIONS] [DIR]

   609

   610   Options are:

   611     -c           cleanup -- be aggressive in removing old stuff

   612     -n NAME      specify document name (default 'document')

   613     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,

   614                  ps.gz, pdf

   615     -t TAGS      specify tagged region markup

   616

   617   Prepare the theory session document in DIR (default 'document')

   618   producing the specified output format.

   619 \end{ttbox}

   620   This tool is usually run automatically as part of the corresponding

   621   Isabelle batch process, provided document preparation has been

   622   enabled (cf.\ the @{verbatim "-d"} option of the @{tool_ref usedir}

   623   tool).  It may be manually invoked on the generated browser

   624   information document output as well, e.g.\ in case of errors

   625   encountered in the batch run.

   626

   627   \medskip The @{verbatim "-c"} option tells the @{tool document} tool

   628   to dispose the document sources after successful operation.  This is

   629   the right thing to do for sources generated by an Isabelle process,

   630   but take care of your files in manual document preparation!

   631

   632   \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify

   633   the final output file name and format, the default is @{verbatim

   634   document.dvi}''.  Note that the result will appear in the parent of

   635   the target @{verbatim DIR}.

   636

   637   \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret

   638   tagged Isabelle command regions.  Tags are specified as a comma

   639   separated list of modifier/name pairs: @{verbatim "+"}@{text

   640   foo}'' (or just @{text foo}'') means to keep, @{verbatim

   641   "-"}@{text foo}'' to drop, and @{verbatim "/"}@{text foo}'' to

   642   fold text tagged as @{text foo}.  The builtin default is equivalent

   643   to the tag specification @{verbatim

   644   "/theory,/proof,/ML,+visible,-invisible"}''; see also the {\LaTeX}

   645   macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and

   646   @{verbatim "\\isafoldtag"}, in @{"file"

   647   "~~/lib/texinputs/isabelle.sty"}.

   648

   649   \medskip Document preparation requires a properly setup @{verbatim

   650   document}'' directory within the logic session sources.  This

   651   directory is supposed to contain all the files needed to produce the

   652   final document --- apart from the actual theories which are

   653   generated by Isabelle.

   654

   655   \medskip For most practical purposes, the @{tool document} tool is

   656   smart enough to create any of the specified output formats, taking

   657   @{verbatim root.tex} supplied by the user as a starting point.  This

   658   even includes multiple runs of {\LaTeX} to accommodate references

   659   and bibliographies (the latter assumes @{verbatim root.bib} within

   660   the same directory).

   661

   662   In more complex situations, a separate @{verbatim IsaMakefile} for

   663   the document sources may be given instead.  This should provide

   664   targets for any admissible document format; these have to produce

   665   corresponding output files named after @{verbatim root} as well,

   666   e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}.

   667

   668   \medskip When running the session, Isabelle copies the original

   669   @{verbatim document} directory into its proper place within

   670   @{setting ISABELLE_BROWSER_INFO} according to the session path.

   671   Then, for any processed theory @{text A} some {\LaTeX} source is

   672   generated and put there as @{text A}@{verbatim ".tex"}.

   673   Furthermore, a list of all generated theory files is put into

   674   @{verbatim session.tex}.  Typically, the root {\LaTeX} file provided

   675   by the user would include @{verbatim session.tex} to get a document

   676   containing all the theories.

   677

   678   The {\LaTeX} versions of the theories require some macros defined in

   679   @{"file" "~~/lib/texinputs/isabelle.sty"}.  Doing @{verbatim

   680   "\\usepackage{isabelle}"} in @{verbatim root.tex} should be fine;

   681   the underlying Isabelle @{tool latex} tool already includes an

   682   appropriate path specification for {\TeX} inputs.

   683

   684   If the text contains any references to Isabelle symbols (such as

   685   @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim

   686   "isabellesym.sty"} should be included as well.  This package

   687   contains a standard set of {\LaTeX} macro definitions @{verbatim

   688   "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim

   689   "<"}@{text foo}@{verbatim ">"}, (see \appref{app:symbols} for a

   690   complete list of predefined Isabelle symbols).  Users may invent

   691   further symbols as well, just by providing {\LaTeX} macros in a

   692   similar fashion as in @{"file" "~~/lib/texinputs/isabellesym.sty"} of

   693   the distribution.

   694

   695   For proper setup of DVI and PDF documents (with hyperlinks and

   696   bookmarks), we recommend to include @{"file"

   697   "~~/lib/texinputs/pdfsetup.sty"} as well.

   698

   699   \medskip As a final step of document preparation within Isabelle,

   700   @{verbatim isabelle} @{tool document}~@{verbatim "-c"} is run on the

   701   resulting @{verbatim document} directory.  Thus the actual output

   702   document is built and installed in its proper place (as linked by

   703   the session's @{verbatim index.html} if option @{verbatim "-i"} of

   704   @{tool_ref usedir} has been enabled, cf.\ \secref{sec:info}).  The

   705   generated sources are deleted after successful run of {\LaTeX} and

   706   friends.  Note that a separate copy of the sources may be retained

   707   by passing an option @{verbatim "-D"} to the @{tool usedir} utility

   708   when running the session.

   709 *}

   710

   711

   712 section {* Running {\LaTeX} within the Isabelle environment

   713   \label{sec:tool-latex} *}

   714

   715 text {*

   716   The @{tool_def latex} utility provides the basic interface for

   717   Isabelle document preparation.  Its usage is:

   718 \begin{ttbox}

   719 Usage: latex [OPTIONS] [FILE]

   720

   721   Options are:

   722     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,

   723                  ps.gz, pdf, bbl, idx, sty, syms

   724

   725   Run LaTeX (and related tools) on FILE (default root.tex),

   726   producing the specified output format.

   727 \end{ttbox}

   728

   729   Appropriate {\LaTeX}-related programs are run on the input file,

   730   according to the given output format: @{executable latex},

   731   @{executable pdflatex}, @{executable dvips}, @{executable bibtex}

   732   (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim

   733   idx}).  The actual commands are determined from the settings

   734   environment (@{setting ISABELLE_LATEX} etc.).

   735

   736   The @{verbatim sty} output format causes the Isabelle style files to

   737   be updated from the distribution.  This is useful in special

   738   situations where the document sources are to be processed another

   739   time by separate tools (cf.\ option @{verbatim "-D"} of the @{tool

   740   usedir} utility).

   741

   742   The @{verbatim syms} output is for internal use; it generates lists

   743   of symbols that are available without loading additional {\LaTeX}

   744   packages.

   745 *}

   746

   747

   748 subsubsection {* Examples *}

   749

   750 text {*

   751   Invoking @{verbatim isabelle} @{tool latex} by hand may be

   752   occasionally useful when debugging failed attempts of the automatic

   753   document preparation stage of batch-mode Isabelle.  The abortive

   754   process leaves the sources at a certain place within @{setting

   755   ISABELLE_BROWSER_INFO}, see the runtime error message for details.

   756   This enables users to inspect {\LaTeX} runs in further detail, e.g.\

   757   like this:

   758 \begin{ttbox}

   759   cd ~/isabelle/browser_info/HOL/Test/document

   760   isabelle latex -o pdf

   761 \end{ttbox}

   762 *}

   763

   764 end