author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 9237 161fb7f00414
child 10564 42f41f966db4
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
     2 %% $Id$
     4 \chapter{Presenting theories}
     6 Isabelle provides several ways to present the outcome of formal developments,
     7 including WWW-based browsable libraries or actual printable documents.
     8 Presentation is centered around the concept of \emph{logic sessions}.  The
     9 global session structure is that of a tree, with Isabelle \texttt{Pure} at its
    10 root, further object-logics derived (e.g.\ \texttt{HOLCF} from \texttt{HOL},
    11 and \texttt{HOL} from \texttt{Pure}), and application sessions in leaf
    12 positions.  The latter usually do not have a separate {\ML} image.
    14 The \texttt{usedir} and \texttt{mkdir} utilities provide the prime means for
    15 managing Isabelle sessions, including proper setup for presentation (see
    16 \S\ref{sec:tool-usedir} and \S\ref{sec:tool-mkdir}).
    19 \section{Generating theory browsing information} \label{sec:info}
    20 \index{theory browsing information|bold}
    22 As a side-effect of running a logic sessions, Isabelle is able to generate
    23 theory browsing information, including HTML documents that show a theory's
    24 definition, the theorems proved in its ML file and the relationship with its
    25 ancestors and descendants.  Besides the HTML file that is generated for every
    26 theory, Isabelle stores links to all theories in an index file. These indexes
    27 are linked with other indexes to represent the overall tree structure of logic
    28 sessions.
    30 Isabelle also generates graph files that represent the theory hierarchy of a
    31 logic.  There is a graph browser Java applet embedded in the generated HTML
    32 pages, and also a stand-alone application that allows browsing theory graphs
    33 without having to start a WWW browser first.  The latter version also includes
    34 features such as generating {\sc PostScript} files, which are not available in
    35 the applet version.  See \S\ref{sec:browse} for further information.
    37 \medskip
    39 In order to let Isabelle generate theory browsing information, simply append
    40 ``\texttt{-i true}'' to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before
    41 making a logic.  For example, in order to do this for FOL, add this to your
    42 Isabelle settings file
    43 \begin{ttbox}
    45 \end{ttbox}
    46 and then change into the \texttt{src/FOL} directory of the Isabelle
    47 distribution and run \texttt{isatool make}, or even \texttt{isatool make all}.
    49 Some sessions (such as \texttt{HOL/Isar_examples}) even provide actual
    50 printable documents.  These are prepared automatically as well if enabled like
    51 this, using the \texttt{-d} option
    52 \begin{ttbox}
    53 ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
    54 \end{ttbox}
    55 See \S\ref{sec:tool-document} for further information on Isabelle document
    56 preparation.
    58 \bigskip The theory browsing information is stored within the directory
    59 determined by the \settdx{ISABELLE_BROWSER_INFO} setting.  The
    60 \texttt{index.html} file located there provides an entry point to all standard
    61 Isabelle logics.  A complete HTML version of all object-logics and examples of
    62 the Isabelle distribution is available at
    63 \begin{center}\small
    64   \begin{tabular}{l}
    65     \url{} \\
    66     \url{} \\
    67   \end{tabular}
    68 \end{center}
    70 \medskip
    72 The generated HTML document of any theory includes all theorems proved in the
    73 corresponding {\ML} file, provided these have been stored properly via
    74 \ttindex{qed}, \ttindex{qed_goal}, \ttindex{qed_goalw}, \ttindex{bind_thm},
    75 \ttindex{bind_thms} or \ttindex{store_thm} (see also \cite{isabelle-ref}).
    76 Section headings may be included in the presentation via the {\ML} function
    77 \begin{ttbox}\index{*section}
    78 section: string -> unit
    79 \end{ttbox}
    81 \medskip
    83 In order to present your own theories on the web, simply copy the
    84 corresponding subdirectory from \texttt{ISABELLE_BROWSER_INFO} to your WWW
    85 server, after having generated browser info like this:
    86 \begin{ttbox}
    87 isatool usedir -i true HOL Foo
    88 \end{ttbox}
    89 This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file
    90 to load all your theories, and HOL is your parent logic image.  Ideally,
    91 theory browser information would have been generated for HOL already.
    93 Alternatively, one may specify an external link to an existing body of HTML
    94 data by giving \texttt{usedir} a \texttt{-P} option like this:
    95 \begin{ttbox}
    96 isatool usedir -i true -P HOL Foo
    97 \end{ttbox}
    99 \medskip For production use, the \texttt{usedir} tool is usually invoked in an
   100 appropriate \texttt{IsaMakefile}, via the Isabelle \texttt{make} utility.
   101 There is a separate \texttt{mkdir} tool to provide easy setup of all this,
   102 with only minimal manual editing required.
   103 \begin{ttbox}
   104 isatool mkdir -d Foo
   105 edit Foo/ROOT.ML
   106 isatool make
   107 \end{ttbox}
   108 See \S\ref{sec:tool-mkdir} for more information on preparing Isabelle session
   109 directories, including the setup for documents.
   112 \section{Browsing theory graphs} \label{sec:browse}
   113 \index{theory graph browser|bold} 
   115 The graph browser is a tool for visualizing dependency graphs. Certain nodes
   116 of the graph (i.e.~theories) can be grouped together in ``directories'', whose
   117 contents may be hidden, thus enabling the user to filter out irrelevant
   118 information.  The browser is written in Java, it can be used both as a
   119 stand-alone application and as an applet.
   122 \subsection{Invoking the graph browser}
   124 The stand-alone version of the graph browser is wrapped up as an
   125 Isabelle tool called \tooldx{browser}:
   126 \begin{ttbox}
   127 Usage: browser [OPTIONS] [GRAPHFILE]
   129   Options are:
   130     -d           delete file after use
   131 \end{ttbox}
   132 When no filename is specified, the browser automatically changes to the
   133 directory \texttt{ISABELLE_BROWSER_INFO}.
   135 \medskip The applet version of the browser can be invoked by opening the {\tt
   136   index.html} file in the directory \texttt{ISABELLE_BROWSER_INFO} from your
   137 Web browser and selecting the version ``including theory graph browser''.
   138 There is also a link to the corresponding theory graph in every logic's {\tt
   139   index.html} file.
   142 \subsection{Using the graph browser}
   144 The browser's main window, which is shown in figure
   145 \ref{browserwindow}, consists of two sub-windows: In the left
   146 sub-window, the directory tree is displayed. The graph itself is
   147 displayed in the right sub-window.
   148 \begin{figure}[ht]
   149   \includegraphics[width=\textwidth]{browser_screenshot}
   150   \caption{\label{browserwindow} Browser main window}
   151 \end{figure}
   154 \subsubsection*{The directory tree window}
   156 We describe the usage of the directory browser and the meaning of the
   157 different items in the browser window.
   158 \begin{itemize}
   160 \item A red arrow before a directory name indicates that the directory
   161   is currently ``folded'', i.e.~the nodes in this directory are
   162   collapsed to one single node. In the right sub-window, the names of
   163   nodes corresponding to folded directories are enclosed in square
   164   brackets and displayed in red color.
   166 \item A green downward arrow before a directory name indicates that
   167   the directory is currently ``unfolded''. It can be folded by
   168   clicking on the directory name.  Clicking on the name for a second
   169   time unfolds the directory again.  Alternatively, a directory can
   170   also be unfolded by clicking on the corresponding node in the right
   171   sub-window.
   173 \item Blue arrows stand before ordinary node names. When clicking on such a
   174   name (i.e.\ that of a theory), the graph display window focuses to the
   175   corresponding node. Double clicking invokes a text viewer window in which
   176   the contents of the theory file are displayed.
   178 \end{itemize}
   181 \subsubsection*{The graph display window}
   183 When pointing on an ordinary node, an upward and a downward arrow is
   184 shown.  Initially, both of these arrows are green. Clicking on the
   185 upward or downward arrow collapses all predecessor or successor nodes,
   186 respectively. The arrow's color then changes to red, indicating that
   187 the predecessor or successor nodes are currently collapsed. The node
   188 corresponding to the collapsed nodes has the name ``{\tt [....]}''. To
   189 uncollapse the nodes again, simply click on the red arrow or on the
   190 node with the name ``{\tt [....]}''. Similar to the directory browser,
   191 the contents of theory files can be displayed by double clicking on
   192 the corresponding node.
   195 \subsubsection*{The ``File'' menu}
   197 Please note that due to Java security restrictions this menu is not
   198 available in the applet version. The meaning of the menu items is as
   199 follows:
   200 \begin{description}
   202 \item[Open \dots] Open a new graph file.
   204 \item[Export to PostScript] Outputs the current graph in {\sc
   205     PostScript} format, appropriately scaled to fit on one single
   206   sheet of paper.  The resulting file can be printed directly.
   208 \item[Export to EPS] Outputs the current graph in Encapsulated {\sc
   209     PostScript} format. The resulting file can be included in other
   210   documents.
   212 \item[Quit] Quit the graph browser.
   214 \end{description}
   217 \subsection*{*Syntax of graph definition files}
   219 A graph definition file has the following syntax:
   220 \begin{eqnarray*}
   221   \mbox{\it graph} & = & \{ \: \mbox{\it vertex \tt ;} \: \} ^ + \\
   222   vertex & = & \mbox{\it vertexname} \: \mbox{\it vertexID} \: \mbox{\it dirname} \: [ \mbox{\tt +} ]
   223   \: \mbox{\it path} \: [ \mbox{\tt <} | \mbox{\tt >} ] \: \{ \: \mbox{\it vertexID} \: \} ^ *
   224 \end{eqnarray*}
   226 The meaning of the items in a vertex description is as follows:
   227 \begin{description}
   229 \item[vertexname] The name of the vertex.
   231 \item[vertexID] The vertex identifier. Note that there may be two
   232   vertices with equal names, whereas identifiers must be unique.
   234 \item[dirname] The name of the ``directory'' the vertex should be
   235   placed in.  A ``{\tt +}'' sign after {\it dirname} indicates that
   236   the nodes in the directory are initially visible. Directories are
   237   initially invisible by default.
   239 \item[path] The path of the corresponding theory file. This is
   240   specified relatively to the path of the graph definition file.
   242 \item[List of successor/predecessor nodes] A ``{\tt <}'' sign before
   243   the list means that successor nodes are listed, a ``{\tt >}'' sign
   244   means that predecessor nodes are listed. If neither ``{\tt <}'' nor
   245   ``{\tt >}'' is found, the browser assumes that successor nodes are
   246   listed.
   248 \end{description}
   251 \section{Preparing Isabelle session documents --- \texttt{isatool document}}
   252 \label{sec:tool-document}
   254 The \tooldx{document} utility prepares logic session documents, processing the
   255 sources both as provided by the user and generated by Isabelle.  Its usage is:
   256 \begin{ttbox}
   257 Usage: document [OPTIONS] [DIR]
   259   Options are:
   260     -c           cleanup -- be aggressive in removing old stuff
   261     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
   262                  ps.gz, pdf
   264   Prepare the theory session document in DIR (default 'document')
   265   producing the specified output format.
   266 \end{ttbox}
   267 This tool is usually run automatically as part of the corresponding session,
   268 provided document preparation has been enabled (cf.\ the \texttt{-d} option of
   269 the \texttt{usedir} utility, \S\ref{sec:tool-usedir}).  It may be manually
   270 invoked on the generated browser information document output as well.
   272 \medskip Document preparation requires a properly setup ``\texttt{document}''
   273 directory within the logic session sources.  This directory is supposed to
   274 contain all the files needed to produce the final document --- apart from the
   275 actual theories which are generated by Isabelle.
   277 \medskip For simple documents, the \texttt{document} tool is smart enough to
   278 create any of the output formats, taking \texttt{root.tex} supplied by the
   279 user as a starting point.  This even includes multiple runs of {\LaTeX} to
   280 accommodate references and bibliographies (the latter assumes
   281 \texttt{root.bib} within the same directory).
   283 For complex documents, a separate \texttt{IsaMakefile} may be given instead.
   284 It should provide targets for any admissible document format; these have to
   285 produce corresponding output files named after \texttt{root} as well, e.g.\ 
   286 \texttt{root.dvi} for target format \texttt{dvi}.
   288 \medskip When running the session, Isabelle copies the original
   289 \texttt{document} directory into its proper place within
   290 \texttt{ISABELLE_BROWSER_INFO} according to the session path.  Then, for any
   291 processed theory $A$ some {\LaTeX} source is generated and put there as
   292 $A$\texttt{.tex}.  Furthermore, a list of all generated theory files is put
   293 into \texttt{session.tex}.  Typically, the root {\LaTeX} file provided by the
   294 user would include \texttt{session.tex} to get a document containing all the
   295 theories.
   297 The {\LaTeX} versions of the theories require some macros defined in
   298 \texttt{isabelle.sty} as distributed with Isabelle.  Doing
   299 \verb,\usepackage{isabelle}, somewhere in \texttt{root.tex} should work fine;
   300 the underlying Isabelle \texttt{latex} utility already includes an appropriate
   301 {\TeX} inputs path.
   303 If the text contains any references to Isabelle symbols (such as
   304 \verb,\<forall>,) then \texttt{isabellesym.sty} should be included as well.
   305 This package contains a standard set of {\LaTeX} macro definitions
   306 \verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>,.  The user may
   307 refer to further symbols as well, simply by providing {\LaTeX} macros of the
   308 same sort.
   310 For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
   311 images), we recommend to include \verb,pdfsetup.sty, as well.  It is safe to
   312 do so even without using PDF~\LaTeX.
   314 \medskip As a final step, \texttt{isatool document -c} is run on the resulting
   315 \texttt{document} directory.  Thus the actual output document is built and
   316 installed in its proper place (as linked by the session's
   317 \texttt{index.html}).  The generated sources are deleted after successful run
   318 of {\LaTeX} and friends.  Note that a copy of the sources may be retained by
   319 passing an option \texttt{-D} to the \texttt{usedir} utility when running the
   320 session (see also \S\ref{sec:tool-usedir}).
   323 \section{Running {\LaTeX} within the Isabelle environment --- \texttt{isatool latex}}
   324 \label{sec:tool-latex}
   326 The \tooldx{latex} utility provides the basic interface for Isabelle document
   327 preparation.  Its usage is:
   328 \begin{ttbox}
   329 Usage: latex [OPTIONS] [FILE]
   331   Options are:
   332     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
   333                  ps.gz, pdf, bbl, png, sty
   335   Run LaTeX (and related tools) on FILE (default root.tex),
   336   producing the specified output format.
   337 \end{ttbox}
   338 Appropriate {\LaTeX}-related programs are run on the input file, according to
   339 the given output format: \texttt{latex}, \texttt{pdflatex}, \texttt{dvips},
   340 \texttt{bibtex} (for \texttt{bbl}), and \texttt{thumbpdf} (for \texttt{png}).
   341 The actual commands are determined from the settings environment
   342 (\texttt{ISABELLE_LATEX} etc., see \S\ref{sec:settings}).
   344 The \texttt{sty} output format causes the Isabelle style files to be updated
   345 from the distribution.  This is useful in special situations where the
   346 document sources are to be processed another time by separate tools (cf.\ 
   347 option \texttt{-D} of the \texttt{usedir} utility, see
   348 \S\ref{sec:tool-usedir}).
   350 It is important to note that the {\LaTeX} inputs file space has to be properly
   351 setup to include the Isabelle styles.  Usually, this may be done by modifying
   352 the \settdx{TEXINPUTS} variable in settings like this:
   353 \begin{ttbox}
   355 \end{ttbox}
   356 This is known to work with recent versions of the \textsl{teTeX} distribution.
   359 \section{Creating Isabelle session directories --- \texttt{isatool mkdir}}
   360 \label{sec:tool-mkdir}
   362 The \tooldx{mkdir} utility prepares Isabelle session source directories,
   363 including a sensible default setup of \texttt{IsaMakefile}, \texttt{ROOT.ML}
   364 and an optional \texttt{document} directory.  Its usage is:
   365 \begin{ttbox}
   366 Usage: mkdir [OPTIONS] [LOGIC] NAME
   368   Options are:
   369     -I FILE      alternative IsaMakefile output
   370     -P           include parent logic target
   371     -b           setup build mode (session outputs heap image)
   372     -d           setup document
   374   Prepare session directory, including IsaMakefile, document etc.
   375   with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
   376 \end{ttbox}
   378 The \texttt{mkdir} tool is conservative in the sense that any existing
   379 \texttt{IsaMakefile} etc.\ is left unchanged.  Thus it is safe to invoke it
   380 experimentally, with varying options.
   382 Note that \texttt{mkdir} is unable to change \texttt{IsaMakefile}
   383 incrementally --- manual changes are required for multiple sub-sessions.  On
   384 order to get an initial working session, the only editing needed is to add
   385 appropriate \texttt{use_thy} calls to the generated \texttt{ROOT.ML} file.
   388 \subsection*{Options}
   390 The \texttt{-I} option specifies an alternative to \texttt{IsaMakefile} for
   391 dependencies.  Note that ``\texttt{-}'' refers to \emph{stdout}, i.e.\ 
   392 ``\texttt{-I-}'' provides an easy way to peek at \texttt{mkdir}'s idea of
   393 \texttt{make} setup required for some particular of Isabelle session.
   395 \medskip The \texttt{-P} option includes a target for the parent
   396 \texttt{LOGIC} session in the generated \texttt{IsaMakefile}.  The
   397 corresponding sources are assumed to be located within the Isabelle
   398 distribution.
   400 \medskip The \texttt{-b} option sets up the current directory as the base for
   401 a new session that provides an actual logic image, as opposed to one that only
   402 runs several theories based on an existing image.  Note that in the latter
   403 case, everything except \texttt{IsaMakefile} would be placed into a separate
   404 directory \texttt{NAME}, rather than the current one.  See
   405 \S\ref{sec:tool-usedir} for further information on \emph{build mode} vs.\ 
   406 \emph{example mode} of the \texttt{usedir} utility.
   408 \medskip The \texttt{-d} option creates a \texttt{document} directory with a
   409 minimal \texttt{root.tex} file, which is sufficient to get all theories pretty
   410 printed in the order of appearance.  See \S\ref{sec:tool-document} for further
   411 information on Isabelle document preparation.
   414 \subsection*{Examples}
   416 The standard setup of a single ``example session'' based on the default logic,
   417 with proper document generation is generated like this:
   418 \begin{ttbox}
   419 isatool mkdir -d Foo
   420 \end{ttbox}
   421 \noindent The theory sources should be put into the \texttt{Foo} directory, and its
   422 \texttt{ROOT.ML} should be edited to load all required theories.  Invoking
   423 \texttt{isatool make} would now run the whole session, generating browser
   424 information and the document automatically.  The \texttt{IsaMakefile} is
   425 usually tuned manually later, e.g.\ adding actual source dependencies, or
   426 changing the options passed to \texttt{usedir}.
   429 \section{Running Isabelle sessions --- \texttt{isatool usedir}} \label{sec:tool-usedir}
   431 The \tooldx{usedir} utility builds object-logic images, or runs example
   432 sessions based on existing logics. Its usage is:
   433 \begin{ttbox}
   434 Usage: usedir [OPTIONS] LOGIC NAME
   436   Options are:
   437     -D PATH      dump generated document sources into PATH
   438     -P PATH      set path for remote theory browsing information
   439     -b           build mode (output heap image, using current dir)
   440     -c BOOL      tell ML system to compress output image (default true)
   441     -d FORMAT    build document as FORMAT (default false)
   442     -i BOOL      generate theory browsing information,
   443                  i.e. HTML / graph data (default false)
   444     -r           reset session path
   445     -s NAME      override session NAME
   447   Build object-logic or run examples. Also creates browsing
   448   information (HTML etc.) according to settings.
   451 \end{ttbox}
   453 Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
   454 implicitly prefixed to \emph{any} \texttt{usedir} call. Since the
   455 \ttindex{IsaMakefile}s of all object-logics distributed with Isabelle just
   456 invoke \texttt{usedir} for the real work, one may control compilation options
   457 globally via above variable. In particular, generation of \rmindex{HTML}
   458 browsing information and document preparation is controlled here.
   461 \subsection*{Options}
   463 Basically, there are two different modes of operation: \emph{build mode}
   464 (enabled through the \texttt{-b} option) and \emph{example mode} (default).
   466 Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with input
   467 image \texttt{LOGIC} and output to \texttt{NAME}, as provided on the command
   468 line. This will be a batch session, running \texttt{ROOT.ML} from the current
   469 directory and then quitting.  It is assumed that \texttt{ROOT.ML} contains all
   470 {\ML} commands required to build the logic.
   472 In example mode, \texttt{usedir} runs a read-only session of \texttt{LOGIC}
   473 and automatically runs \texttt{ROOT.ML} from within directory \texttt{NAME}.
   474 It assumes that this file contains appropriate {\ML} commands to run the
   475 desired examples.
   477 \medskip The \texttt{-i} option controls theory browser data generation. It
   478 may be explicitly turned on or off --- as usual, the last occurrence of
   479 \texttt{-i} on the command line wins.  The \texttt{-P} option specifies a path
   480 (or actual URL) to be prefixed to any \emph{non-local} reference of existing
   481 theories.  Thus user sessions may easily link to existing Isabelle libraries
   482 already present on the WWW.
   484 \medskip The \texttt{-d} option controls document preparation.  Valid
   485 arguments are \texttt{false} (do not prepare any document; this is default),
   486 or any of \texttt{dvi}, \texttt{dvi.gz}, \texttt{ps}, \texttt{ps.gz},
   487 \texttt{pdf}.  The logic session has to provide a properly setup
   488 \texttt{document} directory.  See \S\ref{sec:tool-document} and
   489 \S\ref{sec:tool-latex} for more details.
   491 \medskip The \texttt{-D} option causes the generated document sources to be
   492 dumped at location \texttt{PATH}, which is relative to the session's main
   493 directory.  For example, \texttt{-D document} would leave a copy of the
   494 {\LaTeX} sources in the actual document directory.  Thus the Isabelle
   495 \texttt{document} or \texttt{latex} tools may be run later, facilitating much
   496 easier debugging of {\LaTeX} errors, for example.  Note that a copy of the
   497 Isabelle style files will be placed in \texttt{PATH} as well.
   499 \medskip Any \texttt{usedir} session is named by some \emph{session
   500   identifier}. These accumulate, documenting the way sessions depend on
   501 others. For example, consider \texttt{Pure/FOL/ex}, which refers to the
   502 examples of FOL, which in turn is built upon Pure.
   504 The current session's identifier is by default just the base name of the
   505 \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME} argument (in
   506 example mode). This may be overridden explicitly via the \texttt{-s} option.
   509 \subsection*{Examples}
   511 Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's
   512 object-logics as a model for your own developments.  For example, see
   513 \texttt{src/FOL/IsaMakefile}.  The Isabelle \texttt{mkdir} tool (see
   514 \S\ref{sec:tool-mkdir}) creates \texttt{IsaMakefile}s with proper invocation
   515 of \texttt{usedir} as well.
   518 %%% Local Variables: 
   519 %%% mode: latex
   520 %%% TeX-master: "system"
   521 %%% End: