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