doc-src/System/Thy/document/Presentation.tex
author wenzelm
Sat Oct 04 17:40:58 2008 +0200 (2008-10-04)
changeset 28505 f98751bd715f
parent 28238 398bf960d3d4
child 28838 d5db6dfcb34a
permissions -rw-r--r--
updated generated file;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Presentation}%
     4 %
     5 \isadelimtheory
     6 \isanewline
     7 \isanewline
     8 %
     9 \endisadelimtheory
    10 %
    11 \isatagtheory
    12 \isacommand{theory}\isamarkupfalse%
    13 \ Presentation\isanewline
    14 \isakeyword{imports}\ Pure\isanewline
    15 \isakeyword{begin}%
    16 \endisatagtheory
    17 {\isafoldtheory}%
    18 %
    19 \isadelimtheory
    20 %
    21 \endisadelimtheory
    22 %
    23 \isamarkupchapter{Presenting theories \label{ch:present}%
    24 }
    25 \isamarkuptrue%
    26 %
    27 \begin{isamarkuptext}%
    28 Isabelle provides several ways to present the outcome of formal
    29   developments, including WWW-based browsable libraries or actual
    30   printable documents.  Presentation is centered around the concept of
    31   \emph{logic sessions}.  The global session structure is that of a
    32   tree, with Isabelle Pure at its root, further object-logics derived
    33   (e.g.\ HOLCF from HOL, and HOL from Pure), and application sessions
    34   in leaf positions (usually without a separate image).
    35 
    36   The Isabelle tools \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} and \indexref{}{tool}{make}\hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} provide
    37   the primary means for managing Isabelle sessions, including proper
    38   setup for presentation.  Here the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} tool takes care
    39   to let \indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} process run any
    40   additional stages required for document preparation, notably the
    41   tools \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} and \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}}.  The complete tool
    42   chain for managing batch-mode Isabelle sessions is illustrated in
    43   \figref{fig:session-tools}.
    44 
    45   \begin{figure}[htbp]
    46   \begin{center}
    47   \begin{tabular}{lp{0.6\textwidth}}
    48 
    49       \verb|isabelle| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} & invoked once by the user
    50       to create the initial source setup (common \verb|IsaMakefile| plus a single session directory); \\
    51 
    52       \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} & invoked repeatedly by the
    53       user to keep session output up-to-date (HTML, documents etc.); \\
    54 
    55       \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} & part of the standard
    56       \verb|IsaMakefile| entry of a session; \\
    57 
    58       \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} & run through \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}; \\
    59 
    60       \verb|isabelle| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} & run by the Isabelle
    61       process if document preparation is enabled; \\
    62 
    63       \verb|isabelle| \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} & universal {\LaTeX} tool
    64       wrapper invoked multiple times by \verb|isabelle| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}; also useful for manual experiments; \\
    65 
    66   \end{tabular}
    67   \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
    68   \end{center}
    69   \end{figure}%
    70 \end{isamarkuptext}%
    71 \isamarkuptrue%
    72 %
    73 \isamarkupsection{Generating theory browser information \label{sec:info}%
    74 }
    75 \isamarkuptrue%
    76 %
    77 \begin{isamarkuptext}%
    78 \index{theory browsing information|bold}
    79 
    80   As a side-effect of running a logic sessions, Isabelle is able to
    81   generate theory browsing information, including HTML documents that
    82   show a theory's definition, the theorems proved in its ML file and
    83   the relationship with its ancestors and descendants.  Besides the
    84   HTML file that is generated for every theory, Isabelle stores links
    85   to all theories in an index file. These indexes are linked with
    86   other indexes to represent the overall tree structure of logic
    87   sessions.
    88 
    89   Isabelle also generates graph files that represent the theory
    90   hierarchy of a logic.  There is a graph browser Java applet embedded
    91   in the generated HTML pages, and also a stand-alone application that
    92   allows browsing theory graphs without having to start a WWW client
    93   first.  The latter version also includes features such as generating
    94   Postscript files, which are not available in the applet version.
    95   See \secref{sec:browse} for further information.
    96 
    97   \medskip
    98 
    99   The easiest way to let Isabelle generate theory browsing information
   100   for existing sessions is to append ``\verb|-i true|'' to the
   101   \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} before invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} (or \hyperlink{file.$ISABELLE-HOME/build}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}build}}}}).  For
   102   example, add something like this to your Isabelle settings file
   103 
   104 \begin{ttbox}
   105 ISABELLE_USEDIR_OPTIONS="-i true"
   106 \end{ttbox}
   107 
   108   and then change into the \hyperlink{file.~~/src/FOL}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL}}}} directory and run
   109   \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|.  The presentation output will appear in
   110   \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
   111   \verb|~/isabelle/browser_info/FOL|.  Note that option
   112   \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
   113   more explicit about such details.
   114 
   115   Many standard Isabelle sessions (such as \hyperlink{file.~~/src/HOL/ex}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}ex}}}})
   116   also provide actual printable documents.  These are prepared
   117   automatically as well if enabled like this, using the \verb|-d| option
   118 \begin{ttbox}
   119 ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
   120 \end{ttbox}
   121   Enabling options \verb|-i| and \verb|-d|
   122   simultaneously as shown above causes an appropriate ``document''
   123   link to be included in the HTML index.  Documents (or raw document
   124   sources) may be generated independently of browser information as
   125   well, see \secref{sec:tool-document} for further details.
   126 
   127   \bigskip The theory browsing information is stored in a
   128   sub-directory directory determined by the \indexref{}{setting}{ISABELLE\_BROWSER\_INFO}\hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} setting plus a prefix corresponding to the
   129   session identifier (according to the tree structure of sub-sessions
   130   by default).  A complete WWW view of all standard object-logics and
   131   examples of the Isabelle distribution is available at the usual
   132   Isabelle sites:
   133   \begin{center}\small
   134   \begin{tabular}{l}
   135     \url{http://isabelle.in.tum.de/dist/library/} \\
   136     \url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/} \\
   137     \url{http://mirror.cse.unsw.edu.au/pub/isabelle/dist/library/} \\
   138   \end{tabular}
   139   \end{center}
   140   
   141   \medskip In order to present your own theories on the web, simply
   142   copy the corresponding subdirectory from \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} to your WWW server, having generated browser
   143   info like this:
   144 \begin{ttbox}
   145 isabelle usedir -i true HOL Foo
   146 \end{ttbox}
   147 
   148   This assumes that directory \verb|Foo| contains some \verb|ROOT.ML| file to load all your theories, and HOL is your parent
   149   logic image (\verb|isabelle| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} assists in
   150   setting up Isabelle session directories.  Theory browser information
   151   for HOL should have been generated already beforehand.
   152   Alternatively, one may specify an external link to an existing body
   153   of HTML data by giving \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} a \verb|-P| option like
   154   this:
   155 \begin{ttbox}
   156 isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
   157 \end{ttbox}
   158 
   159   \medskip For production use, the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} tool is usually
   160   invoked in an appropriate \verb|IsaMakefile|, via the Isabelle
   161   \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} tool.  There is a separate \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool to
   162   provide easy setup of all this, with only minimal manual editing
   163   required.
   164 \begin{ttbox}
   165 isabelle mkdir HOL Foo && isabelle make
   166 \end{ttbox}
   167   See \secref{sec:tool-mkdir} for more information on preparing
   168   Isabelle session directories, including the setup for documents.%
   169 \end{isamarkuptext}%
   170 \isamarkuptrue%
   171 %
   172 \isamarkupsection{Browsing theory graphs \label{sec:browse}%
   173 }
   174 \isamarkuptrue%
   175 %
   176 \begin{isamarkuptext}%
   177 \index{theory graph browser|bold} 
   178 
   179   The Isabelle graph browser is a general tool for visualizing
   180   dependency graphs.  Certain nodes of the graph (i.e.~theories) can
   181   be grouped together in ``directories'', whose contents may be
   182   hidden, thus enabling the user to collapse irrelevant portions of
   183   information.  The browser is written in Java, it can be used both as
   184   a stand-alone application and as an applet.  Note that the option
   185   \verb|-g| of \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
   186   graph presentations in batch mode for inclusion in session
   187   documents.%
   188 \end{isamarkuptext}%
   189 \isamarkuptrue%
   190 %
   191 \isamarkupsubsection{Invoking the graph browser%
   192 }
   193 \isamarkuptrue%
   194 %
   195 \begin{isamarkuptext}%
   196 The stand-alone version of the graph browser is wrapped up as an
   197   Isabelle tool called \indexdef{}{tool}{browser}\hypertarget{tool.browser}{\hyperlink{tool.browser}{\mbox{\isa{\isatt{browser}}}}}:
   198 
   199 \begin{ttbox}
   200 Usage: browser [OPTIONS] [GRAPHFILE]
   201 
   202   Options are:
   203     -c           cleanup -- remove GRAPHFILE after use
   204     -o FILE      output to FILE (ps, eps, pdf)
   205 \end{ttbox}
   206   When no filename is specified, the browser automatically changes to
   207   the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}.
   208 
   209   \medskip The \verb|-c| option causes the input file to be
   210   removed after use.
   211 
   212   The \verb|-o| option indicates batch-mode operation, with the
   213   output written to the indicated file; note that \verb|pdf|
   214   produces an \verb|eps| copy as well.
   215 
   216   \medskip The applet version of the browser is part of the standard
   217   WWW theory presentation, see the link ``theory dependencies'' within
   218   each session index.%
   219 \end{isamarkuptext}%
   220 \isamarkuptrue%
   221 %
   222 \isamarkupsubsection{Using the graph browser%
   223 }
   224 \isamarkuptrue%
   225 %
   226 \begin{isamarkuptext}%
   227 The browser's main window, which is shown in
   228   \figref{fig:browserwindow}, consists of two sub-windows.  In the
   229   left sub-window, the directory tree is displayed. The graph itself
   230   is displayed in the right sub-window.
   231 
   232   \begin{figure}[ht]
   233   \includegraphics[width=\textwidth]{browser_screenshot}
   234   \caption{\label{fig:browserwindow} Browser main window}
   235   \end{figure}%
   236 \end{isamarkuptext}%
   237 \isamarkuptrue%
   238 %
   239 \isamarkupsubsubsection{The directory tree window%
   240 }
   241 \isamarkuptrue%
   242 %
   243 \begin{isamarkuptext}%
   244 We describe the usage of the directory browser and the meaning of
   245   the different items in the browser window.
   246 
   247   \begin{itemize}
   248   
   249   \item A red arrow before a directory name indicates that the
   250   directory is currently ``folded'', i.e.~the nodes in this directory
   251   are collapsed to one single node. In the right sub-window, the names
   252   of nodes corresponding to folded directories are enclosed in square
   253   brackets and displayed in red color.
   254   
   255   \item A green downward arrow before a directory name indicates that
   256   the directory is currently ``unfolded''. It can be folded by
   257   clicking on the directory name.  Clicking on the name for a second
   258   time unfolds the directory again.  Alternatively, a directory can
   259   also be unfolded by clicking on the corresponding node in the right
   260   sub-window.
   261   
   262   \item Blue arrows stand before ordinary node names. When clicking on
   263   such a name (i.e.\ that of a theory), the graph display window
   264   focuses to the corresponding node. Double clicking invokes a text
   265   viewer window in which the contents of the theory file are
   266   displayed.
   267 
   268   \end{itemize}%
   269 \end{isamarkuptext}%
   270 \isamarkuptrue%
   271 %
   272 \isamarkupsubsubsection{The graph display window%
   273 }
   274 \isamarkuptrue%
   275 %
   276 \begin{isamarkuptext}%
   277 When pointing on an ordinary node, an upward and a downward arrow is
   278   shown.  Initially, both of these arrows are green. Clicking on the
   279   upward or downward arrow collapses all predecessor or successor
   280   nodes, respectively. The arrow's color then changes to red,
   281   indicating that the predecessor or successor nodes are currently
   282   collapsed. The node corresponding to the collapsed nodes has the
   283   name ``\verb|[....]|''. To uncollapse the nodes again, simply
   284   click on the red arrow or on the node with the name ``\verb|[....]|''. Similar to the directory browser, the contents of
   285   theory files can be displayed by double clicking on the
   286   corresponding node.%
   287 \end{isamarkuptext}%
   288 \isamarkuptrue%
   289 %
   290 \isamarkupsubsubsection{The ``File'' menu%
   291 }
   292 \isamarkuptrue%
   293 %
   294 \begin{isamarkuptext}%
   295 Due to Java Applet security restrictions this menu is only available
   296   in the full application version. The meaning of the menu items is as
   297   follows:
   298 
   299   \begin{description}
   300   
   301   \item[Open \dots] Open a new graph file.
   302   
   303   \item[Export to PostScript] Outputs the current graph in Postscript
   304   format, appropriately scaled to fit on one single sheet of A4 paper.
   305   The resulting file can be printed directly.
   306   
   307   \item[Export to EPS] Outputs the current graph in Encapsulated
   308   Postscript format. The resulting file can be included in other
   309   documents.
   310 
   311   \item[Quit] Quit the graph browser.
   312 
   313   \end{description}%
   314 \end{isamarkuptext}%
   315 \isamarkuptrue%
   316 %
   317 \isamarkupsubsection{Syntax of graph definition files%
   318 }
   319 \isamarkuptrue%
   320 %
   321 \begin{isamarkuptext}%
   322 A graph definition file has the following syntax:
   323 
   324   \begin{center}\small
   325   \begin{tabular}{rcl}
   326     \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}\isactrlsup {\isacharplus}{\isachardoublequote}} \\
   327     \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}\isactrlsup {\isacharasterisk}{\isachardoublequote}}
   328   \end{tabular}
   329   \end{center}
   330 
   331   The meaning of the items in a vertex description is as follows:
   332 
   333   \begin{description}
   334   
   335   \item[\isa{vertex{\isacharunderscore}name}] The name of the vertex.
   336   
   337   \item[\isa{vertex{\isacharunderscore}ID}] The vertex identifier. Note that there may
   338   be several vertices with equal names, whereas identifiers must be
   339   unique.
   340   
   341   \item[\isa{dir{\isacharunderscore}name}] The name of the ``directory'' the vertex
   342   should be placed in.  A ``\verb|+|'' sign after \isa{dir{\isacharunderscore}name} indicates that the nodes in the directory are initially
   343   visible. Directories are initially invisible by default.
   344   
   345   \item[\isa{path}] The path of the corresponding theory file. This
   346   is specified relatively to the path of the graph definition file.
   347   
   348   \item[List of successor/predecessor nodes] A ``\verb|<|''
   349   sign before the list means that successor nodes are listed, a
   350   ``\verb|>|'' sign means that predecessor nodes are listed. If
   351   neither ``\verb|<|'' nor ``\verb|>|'' is found, the
   352   browser assumes that successor nodes are listed.
   353 
   354   \end{description}%
   355 \end{isamarkuptext}%
   356 \isamarkuptrue%
   357 %
   358 \isamarkupsection{Creating Isabelle session directories
   359   \label{sec:tool-mkdir}%
   360 }
   361 \isamarkuptrue%
   362 %
   363 \begin{isamarkuptext}%
   364 The \indexdef{}{tool}{mkdir}\hypertarget{tool.mkdir}{\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}} utility prepares Isabelle session source
   365   directories, including a sensible default setup of \verb|IsaMakefile|, \verb|ROOT.ML|, and a \verb|document|
   366   directory with a minimal \verb|root.tex| that is sufficient to
   367   print all theories of the session (in the order of appearance); see
   368   \secref{sec:tool-document} for further information on Isabelle
   369   document preparation.  The usage of \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is:
   370 
   371 \begin{ttbox}
   372 Usage: mkdir [OPTIONS] [LOGIC] NAME
   373 
   374   Options are:
   375     -I FILE      alternative IsaMakefile output
   376     -P           include parent logic target
   377     -b           setup build mode (session outputs heap image)
   378     -q           quiet mode
   379 
   380   Prepare session directory, including IsaMakefile and document source,
   381   with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
   382 \end{ttbox}
   383 
   384   The \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool is conservative in the sense that any
   385   existing \verb|IsaMakefile| etc.\ is left unchanged.  Thus it
   386   is safe to invoke it multiple times, although later runs may not
   387   have the desired effect.
   388 
   389   Note that \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is unable to change \verb|IsaMakefile|
   390   incrementally --- manual changes are required for multiple
   391   sub-sessions.  On order to get an initial working session, the only
   392   editing needed is to add appropriate \verb|use_thy| calls to the
   393   generated \verb|ROOT.ML| file.%
   394 \end{isamarkuptext}%
   395 \isamarkuptrue%
   396 %
   397 \isamarkupsubsubsection{Options%
   398 }
   399 \isamarkuptrue%
   400 %
   401 \begin{isamarkuptext}%
   402 The \verb|-I| option specifies an alternative to \verb|IsaMakefile| for dependencies.  Note that ``\verb|-|'' refers
   403   to \emph{stdout}, i.e.\ ``\verb|-I-|'' provides an easy way
   404   to peek at \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}'s idea of \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} setup required for
   405   some particular of Isabelle session.
   406 
   407   \medskip The \verb|-P| option includes a target for the
   408   parent \verb|LOGIC| session in the generated \verb|IsaMakefile|.  The corresponding sources are assumed to be located
   409   within the Isabelle distribution.
   410 
   411   \medskip The \verb|-b| option sets up the current directory
   412   as the base for a new session that provides an actual logic image,
   413   as opposed to one that only runs several theories based on an
   414   existing image.  Note that in the latter case, everything except
   415   \verb|IsaMakefile| would be placed into a separate directory
   416   \verb|NAME|, rather than the current one.  See
   417   \secref{sec:tool-usedir} for further information on \emph{build
   418   mode} vs.\ \emph{example mode} of the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility.
   419 
   420   \medskip The \verb|-q| option enables quiet mode, suppressing
   421   further notes on how to proceed.%
   422 \end{isamarkuptext}%
   423 \isamarkuptrue%
   424 %
   425 \isamarkupsubsubsection{Examples%
   426 }
   427 \isamarkuptrue%
   428 %
   429 \begin{isamarkuptext}%
   430 The standard setup of a single ``example session'' based on the
   431   default logic, with proper document generation is generated like
   432   this:
   433 \begin{ttbox}
   434 isabelle mkdir Foo && isabelle make
   435 \end{ttbox}
   436 
   437   \noindent The theory sources should be put into the \verb|Foo|
   438   directory, and its \verb|ROOT.ML| should be edited to load all
   439   required theories.  Invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} again
   440   would run the whole session, generating browser information and the
   441   document automatically.  The \verb|IsaMakefile| is typically
   442   tuned manually later, e.g.\ adding source dependencies, or changing
   443   the options passed to \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}.
   444 
   445   \medskip Large projects may demand further sessions, potentially
   446   with separate logic images being created.  This usually requires
   447   manual editing of the generated \verb|IsaMakefile|, which is
   448   meant to cover all of the sub-session directories at the same time
   449   (this is the deeper reasong why \verb|IsaMakefile| is not made
   450   part of the initial session directory created by \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}).  See \hyperlink{file.~~/src/HOL/IsaMakefile}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}IsaMakefile}}}} for
   451   a full-blown example.%
   452 \end{isamarkuptext}%
   453 \isamarkuptrue%
   454 %
   455 \isamarkupsection{Running Isabelle sessions \label{sec:tool-usedir}%
   456 }
   457 \isamarkuptrue%
   458 %
   459 \begin{isamarkuptext}%
   460 The \indexdef{}{tool}{usedir}\hypertarget{tool.usedir}{\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}} utility builds object-logic images, or runs
   461   example sessions based on existing logics. Its usage is:
   462 \begin{ttbox}
   463 
   464 Usage: usedir [OPTIONS] LOGIC NAME
   465 
   466   Options are:
   467     -C BOOL      copy existing document directory to -D PATH (default true)
   468     -D PATH      dump generated document sources into PATH
   469     -M MAX       multithreading: maximum number of worker threads (default 1)
   470     -P PATH      set path for remote theory browsing information
   471     -T LEVEL     multithreading: trace level (default 0)
   472     -V VERSION   declare alternative document VERSION
   473     -b           build mode (output heap image, using current dir)
   474     -c BOOL      tell ML system to compress output image (default true)
   475     -d FORMAT    build document as FORMAT (default false)
   476     -f NAME      use ML file NAME (default ROOT.ML)
   477     -g BOOL      generate session graph image for document (default false)
   478     -i BOOL      generate theory browser information (default false)
   479     -m MODE      add print mode for output
   480     -p LEVEL     set level of detail for proof objects
   481     -r           reset session path
   482     -s NAME      override session NAME
   483     -v BOOL      be verbose (default false)
   484 
   485   Build object-logic or run examples. Also creates browsing
   486   information (HTML etc.) according to settings.
   487 
   488   ISABELLE_USEDIR_OPTIONS=
   489   HOL_USEDIR_OPTIONS=
   490 \end{ttbox}
   491 
   492   Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}}
   493   setting is implicitly prefixed to \emph{any} \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
   494   call. Since the \verb|IsaMakefile|s of all object-logics
   495   distributed with Isabelle just invoke \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} for the real
   496   work, one may control compilation options globally via above
   497   variable. In particular, generation of \rmindex{HTML} browsing
   498   information and document preparation is controlled here.
   499 
   500   The \indexref{}{setting}{HOL\_USEDIR\_OPTIONS}\hyperlink{setting.HOL-USEDIR-OPTIONS}{\mbox{\isa{\isatt{HOL{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} setting is specific to the
   501   plain and main Isabelle/HOL images; its value is appended to
   502   \hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} for these particular sessions
   503   only.%
   504 \end{isamarkuptext}%
   505 \isamarkuptrue%
   506 %
   507 \isamarkupsubsubsection{Options%
   508 }
   509 \isamarkuptrue%
   510 %
   511 \begin{isamarkuptext}%
   512 Basically, there are two different modes of operation: \emph{build
   513   mode} (enabled through the \verb|-b| option) and
   514   \emph{example mode} (default).
   515 
   516   Calling \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} with \verb|-b| runs \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} with input image \verb|LOGIC| and output to
   517   \verb|NAME|, as provided on the command line. This will be a
   518   batch session, running \verb|ROOT.ML| from the current
   519   directory and then quitting.  It is assumed that \verb|ROOT.ML|
   520   contains all ML commands required to build the logic.
   521 
   522   In example mode, \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} runs a read-only session of
   523   \verb|LOGIC| and automatically runs \verb|ROOT.ML| from
   524   within directory \verb|NAME|.  It assumes that this file
   525   contains appropriate ML commands to run the desired examples.
   526 
   527   \medskip The \verb|-i| option controls theory browser data
   528   generation. It may be explicitly turned on or off --- as usual, the
   529   last occurrence of \verb|-i| on the command line wins.
   530 
   531   The \verb|-P| option specifies a path (or actual URL) to be
   532   prefixed to any \emph{non-local} reference of existing theories.
   533   Thus user sessions may easily link to existing Isabelle libraries
   534   already present on the WWW.
   535 
   536   The \verb|-m| options specifies additional print modes to be
   537   activated temporarily while the session is processed.
   538 
   539   \medskip The \verb|-d| option controls document preparation.
   540   Valid arguments are \verb|false| (do not prepare any document;
   541   this is default), or any of \verb|dvi|, \verb|dvi.gz|,
   542   \verb|ps|, \verb|ps.gz|, \verb|pdf|.  The logic
   543   session has to provide a properly setup \verb|document|
   544   directory.  See \secref{sec:tool-document} and
   545   \secref{sec:tool-latex} for more details.
   546 
   547   \medskip The \verb|-V| option declares alternative document
   548   versions, consisting of name/tags pairs (cf.\ options \verb|-n| and \verb|-t| of the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool).  The
   549   standard document is equivalent to ``\verb|document=theory,proof,ML|'', which means that all theory begin/end
   550   commands, proof body texts, and ML code will be presented
   551   faithfully.  An alternative version ``\verb|outline=/proof/ML|'' would fold proof and ML parts, replacing the
   552   original text by a short place-holder.  The form ``\isa{name}\verb|=-|,'' means to remove document \isa{name} from
   553   the list of versions to be processed.  Any number of \verb|-V| options may be given; later declarations have precedence over
   554   earlier ones.
   555 
   556   \medskip The \verb|-g| option produces images of the theory
   557   dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
   558   generated document, both as \verb|session_graph.eps| and
   559   \verb|session_graph.pdf| at the same time.  To include this in
   560   the final {\LaTeX} document one could say \verb|\includegraphics{session_graph}| in \verb|document/root.tex| (omitting the file-name extension enables
   561   {\LaTeX} to select to correct version, either for the DVI or PDF
   562   output path).
   563 
   564   \medskip The \verb|-D| option causes the generated document
   565   sources to be dumped at location \verb|PATH|; this path is
   566   relative to the session's main directory.  If the \verb|-C|
   567   option is true, this will include a copy of an existing \verb|document| directory as provided by the user.  For example,
   568   \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}~\verb|-D generated HOL|\isasep\isanewline%
   569 \verb|  Foo| produces a complete set of document sources at \verb|Foo/generated|.  Subsequent invocation of \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|Foo/generated| (see also
   570   \secref{sec:tool-document}) will process the final result
   571   independently of an Isabelle job.  This decoupled mode of operation
   572   facilitates debugging of serious {\LaTeX} errors, for example.
   573 
   574   \medskip The \verb|-p| option determines the level of detail
   575   for internal proof objects, see also the \emph{Isabelle Reference
   576   Manual}~\cite{isabelle-ref}.
   577 
   578   \medskip The \verb|-v| option causes additional information
   579   to be printed while running the session, notably the location of
   580   prepared documents.
   581 
   582   \medskip The \verb|-M| option specifies the maximum number of
   583   parallel threads used for processing independent tasks when checking
   584   theory sources (multithreading only works on suitable ML platforms).
   585   The special value of \verb|0| or \verb|max| refers to the
   586   number of actual CPU cores of the underlying machine, which is a
   587   good starting point for optimal performance tuning.  The \verb|-T| option determines the level of detail in tracing output
   588   concerning the internal locking and scheduling in multithreaded
   589   operation.  This may be helpful in isolating performance
   590   bottle-necks, e.g.\ due to excessive wait states when locking
   591   critical code sections.
   592 
   593   \medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
   594   identifier}. These accumulate, documenting the way sessions depend
   595   on others. For example, consider \verb|Pure/FOL/ex|, which
   596   refers to the examples of FOL, which in turn is built upon Pure.
   597 
   598   The current session's identifier is by default just the base name of
   599   the \verb|LOGIC| argument (in build mode), or of the \verb|NAME| argument (in example mode). This may be overridden explicitly
   600   via the \verb|-s| option.%
   601 \end{isamarkuptext}%
   602 \isamarkuptrue%
   603 %
   604 \isamarkupsubsubsection{Examples%
   605 }
   606 \isamarkuptrue%
   607 %
   608 \begin{isamarkuptext}%
   609 Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
   610   object-logics as a model for your own developments.  For example,
   611   see \hyperlink{file.~~/src/FOL/IsaMakefile}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}IsaMakefile}}}}.  The Isabelle \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool creates \verb|IsaMakefile|s with proper invocation
   612   of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} as well.%
   613 \end{isamarkuptext}%
   614 \isamarkuptrue%
   615 %
   616 \isamarkupsection{Preparing Isabelle session documents
   617   \label{sec:tool-document}%
   618 }
   619 \isamarkuptrue%
   620 %
   621 \begin{isamarkuptext}%
   622 The \indexdef{}{tool}{document}\hypertarget{tool.document}{\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}} utility prepares logic session documents,
   623   processing the sources both as provided by the user and generated by
   624   Isabelle.  Its usage is:
   625 \begin{ttbox}
   626 Usage: document [OPTIONS] [DIR]
   627 
   628   Options are:
   629     -c           cleanup -- be aggressive in removing old stuff
   630     -n NAME      specify document name (default 'document')
   631     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
   632                  ps.gz, pdf
   633     -t TAGS      specify tagged region markup
   634 
   635   Prepare the theory session document in DIR (default 'document')
   636   producing the specified output format.
   637 \end{ttbox}
   638   This tool is usually run automatically as part of the corresponding
   639   Isabelle batch process, provided document preparation has been
   640   enabled (cf.\ the \verb|-d| option of the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
   641   tool).  It may be manually invoked on the generated browser
   642   information document output as well, e.g.\ in case of errors
   643   encountered in the batch run.
   644 
   645   \medskip The \verb|-c| option tells the \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool
   646   to dispose the document sources after successful operation.  This is
   647   the right thing to do for sources generated by an Isabelle process,
   648   but take care of your files in manual document preparation!
   649 
   650   \medskip The \verb|-n| and \verb|-o| option specify
   651   the final output file name and format, the default is ``\verb|document.dvi|''.  Note that the result will appear in the parent of
   652   the target \verb|DIR|.
   653 
   654   \medskip The \verb|-t| option tells {\LaTeX} how to interpret
   655   tagged Isabelle command regions.  Tags are specified as a comma
   656   separated list of modifier/name pairs: ``\verb|+|\isa{foo}'' (or just ``\isa{foo}'') means to keep, ``\verb|-|\isa{foo}'' to drop, and ``\verb|/|\isa{foo}'' to
   657   fold text tagged as \isa{foo}.  The builtin default is equivalent
   658   to the tag specification ``\verb|/theory,/proof,/ML,+visible,-invisible|''; see also the {\LaTeX}
   659   macros \verb|\isakeeptag|, \verb|\isadroptag|, and
   660   \verb|\isafoldtag|, in \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}}.
   661 
   662   \medskip Document preparation requires a properly setup ``\verb|document|'' directory within the logic session sources.  This
   663   directory is supposed to contain all the files needed to produce the
   664   final document --- apart from the actual theories which are
   665   generated by Isabelle.
   666 
   667   \medskip For most practical purposes, the \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} tool is
   668   smart enough to create any of the specified output formats, taking
   669   \verb|root.tex| supplied by the user as a starting point.  This
   670   even includes multiple runs of {\LaTeX} to accommodate references
   671   and bibliographies (the latter assumes \verb|root.bib| within
   672   the same directory).
   673 
   674   In more complex situations, a separate \verb|IsaMakefile| for
   675   the document sources may be given instead.  This should provide
   676   targets for any admissible document format; these have to produce
   677   corresponding output files named after \verb|root| as well,
   678   e.g.\ \verb|root.dvi| for target format \verb|dvi|.
   679 
   680   \medskip When running the session, Isabelle copies the original
   681   \verb|document| directory into its proper place within
   682   \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} according to the session path.
   683   Then, for any processed theory \isa{A} some {\LaTeX} source is
   684   generated and put there as \isa{A}\verb|.tex|.
   685   Furthermore, a list of all generated theory files is put into
   686   \verb|session.tex|.  Typically, the root {\LaTeX} file provided
   687   by the user would include \verb|session.tex| to get a document
   688   containing all the theories.
   689 
   690   The {\LaTeX} versions of the theories require some macros defined in
   691   \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}}.  Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
   692   the underlying Isabelle \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} tool already includes an
   693   appropriate path specification for {\TeX} inputs.
   694 
   695   If the text contains any references to Isabelle symbols (such as
   696   \verb|\|\verb|<forall>|) then \verb|isabellesym.sty| should be included as well.  This package
   697   contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, (see \appref{app:symbols} for a
   698   complete list of predefined Isabelle symbols).  Users may invent
   699   further symbols as well, just by providing {\LaTeX} macros in a
   700   similar fashion as in \hyperlink{file.~~/lib/texinputs/isabellesym.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabellesym{\isachardot}sty}}}} of
   701   the distribution.
   702 
   703   For proper setup of DVI and PDF documents (with hyperlinks and
   704   bookmarks), we recommend to include \hyperlink{file.~~/lib/texinputs/pdfsetup.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}pdfsetup{\isachardot}sty}}}} as well.
   705 
   706   \medskip As a final step of document preparation within Isabelle,
   707   \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the
   708   resulting \verb|document| directory.  Thus the actual output
   709   document is built and installed in its proper place (as linked by
   710   the session's \verb|index.html| if option \verb|-i| of
   711   \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} has been enabled, cf.\ \secref{sec:info}).  The
   712   generated sources are deleted after successful run of {\LaTeX} and
   713   friends.  Note that a separate copy of the sources may be retained
   714   by passing an option \verb|-D| to the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility
   715   when running the session.%
   716 \end{isamarkuptext}%
   717 \isamarkuptrue%
   718 %
   719 \isamarkupsection{Running {\LaTeX} within the Isabelle environment
   720   \label{sec:tool-latex}%
   721 }
   722 \isamarkuptrue%
   723 %
   724 \begin{isamarkuptext}%
   725 The \indexdef{}{tool}{latex}\hypertarget{tool.latex}{\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}}} utility provides the basic interface for
   726   Isabelle document preparation.  Its usage is:
   727 \begin{ttbox}
   728 Usage: latex [OPTIONS] [FILE]
   729 
   730   Options are:
   731     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
   732                  ps.gz, pdf, bbl, idx, sty, syms
   733 
   734   Run LaTeX (and related tools) on FILE (default root.tex),
   735   producing the specified output format.
   736 \end{ttbox}
   737 
   738   Appropriate {\LaTeX}-related programs are run on the input file,
   739   according to the given output format: \hyperlink{executable.latex}{\mbox{\isa{\isatt{latex}}}},
   740   \hyperlink{executable.pdflatex}{\mbox{\isa{\isatt{pdflatex}}}}, \hyperlink{executable.dvips}{\mbox{\isa{\isatt{dvips}}}}, \hyperlink{executable.bibtex}{\mbox{\isa{\isatt{bibtex}}}}
   741   (for \verb|bbl|), and \hyperlink{executable.makeindex}{\mbox{\isa{\isatt{makeindex}}}} (for \verb|idx|).  The actual commands are determined from the settings
   742   environment (\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LATEX}}}} etc.).
   743 
   744   The \verb|sty| output format causes the Isabelle style files to
   745   be updated from the distribution.  This is useful in special
   746   situations where the document sources are to be processed another
   747   time by separate tools (cf.\ option \verb|-D| of the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility).
   748 
   749   The \verb|syms| output is for internal use; it generates lists
   750   of symbols that are available without loading additional {\LaTeX}
   751   packages.%
   752 \end{isamarkuptext}%
   753 \isamarkuptrue%
   754 %
   755 \isamarkupsubsubsection{Examples%
   756 }
   757 \isamarkuptrue%
   758 %
   759 \begin{isamarkuptext}%
   760 Invoking \verb|isabelle| \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} by hand may be
   761   occasionally useful when debugging failed attempts of the automatic
   762   document preparation stage of batch-mode Isabelle.  The abortive
   763   process leaves the sources at a certain place within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}, see the runtime error message for details.
   764   This enables users to inspect {\LaTeX} runs in further detail, e.g.\
   765   like this:
   766 \begin{ttbox}
   767   cd ~/isabelle/browser_info/HOL/Test/document
   768   isabelle latex -o pdf
   769 \end{ttbox}%
   770 \end{isamarkuptext}%
   771 \isamarkuptrue%
   772 %
   773 \isadelimtheory
   774 %
   775 \endisadelimtheory
   776 %
   777 \isatagtheory
   778 \isacommand{end}\isamarkupfalse%
   779 %
   780 \endisatagtheory
   781 {\isafoldtheory}%
   782 %
   783 \isadelimtheory
   784 %
   785 \endisadelimtheory
   786 \end{isabellebody}%
   787 %%% Local Variables:
   788 %%% mode: latex
   789 %%% TeX-master: "root"
   790 %%% End: