doc-src/System/Thy/document/Presentation.tex

clarified "isabelle logo";

%
\begin{isabellebody}%
\def\isabellecontext{Presentation}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Presentation\isanewline
\isakeyword{imports}\ Base\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Presenting theories \label{ch:present}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle provides several ways to present the outcome of
  formal developments, including WWW-based browsable libraries or
  actual printable documents.  Presentation is centered around the
  concept of \emph{sessions} (\chref{ch:session}).  The global session
  structure is that of a tree, with Isabelle Pure at its root, further
  object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and
  application sessions further on in the hierarchy.

  The tools \indexref{}{tool}{mkroot}\hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} and \indexref{}{tool}{build}\hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}} provide the
  primary means for managing Isabelle sessions, including proper setup
  for presentation; \hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}} takes care to have \indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} run any additional stages required for document
  preparation, notably the \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}} and \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}}.
  The complete tool chain for managing batch-mode Isabelle sessions is
  illustrated in \figref{fig:session-tools}.

  \begin{figure}[htbp]
  \begin{center}
  \begin{tabular}{lp{0.6\textwidth}}

      \indexref{}{tool}{mkroot}\hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} & invoked once by the user to initialize the
      session \verb|ROOT| with optional \verb|document|
      directory; \\

      \indexref{}{tool}{build}\hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}} & invoked repeatedly by the user to keep
      session output up-to-date (HTML, documents etc.); \\

      \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} & run through \indexref{}{tool}{build}\hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}}; \\

      \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}} & run by the Isabelle process if document
      preparation is enabled; \\

      \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}} & universal {\LaTeX} tool wrapper invoked
      multiple times by \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}; also useful for manual
      experiments; \\

  \end{tabular}
  \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
  \end{center}
  \end{figure}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Generating theory browser information \label{sec:info}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\index{theory browsing information|bold}

  As a side-effect of building sessions, Isabelle is able to generate
  theory browsing information, including HTML documents that show the
  theory sources and the relationship with its ancestors and
  descendants.  Besides the HTML file that is generated for every
  theory, Isabelle stores links to all theories in an index
  file. These indexes are linked with other indexes to represent the
  overall tree structure of the sessions.

  Isabelle also generates graph files that represent the theory
  dependencies within a session.  There is a graph browser Java applet
  embedded in the generated HTML pages, and also a stand-alone
  application that allows browsing theory graphs without having to
  start a WWW client first.  The latter version also includes features
  such as generating Postscript files, which are not available in the
  applet version.  See \secref{sec:browse} for further information.

  \medskip

  The easiest way to let Isabelle generate theory browsing information
  for existing sessions is to invoke \hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}} with suitable
  options:

\begin{ttbox}
isabelle build -o browser_info -v -c FOL
\end{ttbox}

  The presentation output will appear in \verb|$ISABELLE_BROWSER_INFO/FOL| as reported by the above verbose
  invocation of the build process.

  Many Isabelle sessions (such as \verb|HOL-Library| in \verb|~~/src/HOL/Library|) also provide actual printable documents.
  These are prepared automatically as well if enabled like this:
\begin{ttbox}
isabelle build -o browser_info -o document=pdf -v -c HOL-Library
\end{ttbox}

  Enabling both browser info and document preparation simultaneously
  causes an appropriate ``document'' link to be included in the HTML
  index.  Documents may be generated independently of browser
  information as well, see \secref{sec:tool-document} for further
  details.

  \bigskip The theory browsing information is stored in a
  sub-directory directory determined by the \indexref{}{setting}{ISABELLE\_BROWSER\_INFO}\hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}} setting plus a prefix corresponding to the
  session identifier (according to the tree structure of sub-sessions
  by default).  In order to present Isabelle applications on the web,
  the corresponding subdirectory from \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}
  can be put on a WWW server.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Preparing session root directories \label{sec:tool-mkroot}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{mkroot}\hypertarget{tool.mkroot}{\hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}}} tool configures a given directory as
  session root, with some \verb|ROOT| file and optional document
  source directory.  Its usage is:
\begin{ttbox}
Usage: isabelle mkroot [OPTIONS] [DIR]

  Options are:
    -d           enable document preparation
    -n NAME      alternative session name (default: DIR base name)

  Prepare session root DIR (default: current directory).
\end{ttbox}

  The results are placed in the given directory \isa{dir}, which
  refers to the current directory by default.  The \hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} tool
  is conservative in the sense that it does not overwrite existing
  files or directories.  Earlier attempts to generate a session root
  need to be deleted manually.

  \medskip Option \verb|-d| indicates that the session shall be
  accompanied by a formal document, with \isa{dir}\verb|/document/root.tex| as its {\LaTeX} entry point (see also
  \chref{ch:present}).

  Option \verb|-n| allows to specify an alternative session
  name; otherwise the base name of the given directory is used.

  \medskip The implicit Isabelle settings variable \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LOGIC}}}} specifies the parent session, and \hyperlink{setting.ISABELLE-DOCUMENT-FORMAT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DOCUMENT{\isaliteral{5F}{\isacharunderscore}}FORMAT}}}} the document format to be filled filled
  into the generated \verb|ROOT| file.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Examples%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Produce session \verb|Test| (with document preparation)
  within a separate directory of the same name:
\begin{ttbox}
isabelle mkroot -d Test && isabelle build -D Test
\end{ttbox}

  \medskip Upgrade the current directory into a session ROOT with
  document preparation, and build it:
\begin{ttbox}
isabelle mkroot -d && isabelle build -D .
\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Preparing Isabelle session documents
  \label{sec:tool-document}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{document}\hypertarget{tool.document}{\hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}} tool prepares logic session
  documents, processing the sources both as provided by the user and
  generated by Isabelle.  Its usage is:
\begin{ttbox}
Usage: isabelle document [OPTIONS] [DIR]

  Options are:
    -c           cleanup -- be aggressive in removing old stuff
    -n NAME      specify document name (default 'document')
    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
                 ps.gz, pdf
    -t TAGS      specify tagged region markup

  Prepare the theory session document in DIR (default 'document')
  producing the specified output format.
\end{ttbox}
  This tool is usually run automatically as part of the Isabelle build
  process, provided document preparation has been enabled via suitable
  options.  It may be manually invoked on the generated browser
  information document output as well, e.g.\ in case of errors
  encountered in the batch run.

  \medskip The \verb|-c| option tells \hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}} to
  dispose the document sources after successful operation!  This is
  the right thing to do for sources generated by an Isabelle process,
  but take care of your files in manual document preparation!

  \medskip The \verb|-n| and \verb|-o| option specify
  the final output file name and format, the default is ``\verb|document.dvi|''.  Note that the result will appear in the parent of
  the target \verb|DIR|.

  \medskip The \verb|-t| option tells {\LaTeX} how to interpret
  tagged Isabelle command regions.  Tags are specified as a comma
  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
  fold text tagged as \isa{foo}.  The builtin default is equivalent
  to the tag specification ``\verb|+theory,+proof,+ML,+visible,-invisible|''; see also the {\LaTeX}
  macros \verb|\isakeeptag|, \verb|\isadroptag|, and
  \verb|\isafoldtag|, in \verb|~~/lib/texinputs/isabelle.sty|.

  \medskip Document preparation requires a \verb|document|
  directory within the session sources.  This directory is supposed to
  contain all the files needed to produce the final document --- apart
  from the actual theories which are generated by Isabelle.

  \medskip For most practical purposes, \hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}} is smart
  enough to create any of the specified output formats, taking
  \verb|root.tex| supplied by the user as a starting point.  This
  even includes multiple runs of {\LaTeX} to accommodate references
  and bibliographies (the latter assumes \verb|root.bib| within
  the same directory).

  In more complex situations, a separate \verb|build| script for
  the document sources may be given.  It is invoked with command-line
  arguments for the document format and the document variant name.
  The script needs to produce corresponding output files, e.g.\
  \verb|root.pdf| for target format \verb|pdf| (and default
  default variants).  The main work can be again delegated to \hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}}, but it is also possible to harvest generated {\LaTeX}
  sources and copy them elsewhere, for example.

  \medskip When running the session, Isabelle copies the content of
  the original \verb|document| directory into its proper place
  within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}, according to the session
  path and document variant.  Then, for any processed theory \isa{A}
  some {\LaTeX} source is generated and put there as \isa{A}\verb|.tex|.  Furthermore, a list of all generated theory
  files is put into \verb|session.tex|.  Typically, the root
  {\LaTeX} file provided by the user would include \verb|session.tex| to get a document containing all the theories.

  The {\LaTeX} versions of the theories require some macros defined in
  \verb|~~/lib/texinputs/isabelle.sty|.  Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
  the underlying \hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}} already includes an appropriate path
  specification for {\TeX} inputs.

  If the text contains any references to Isabelle symbols (such as
  \verb|\|\verb|<forall>|) then \verb|isabellesym.sty| should be included as well.  This package
  contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, see \cite{isabelle-implementation} for a
  complete list of predefined Isabelle symbols.  Users may invent
  further symbols as well, just by providing {\LaTeX} macros in a
  similar fashion as in \verb|~~/lib/texinputs/isabellesym.sty| of
  the distribution.

  For proper setup of DVI and PDF documents (with hyperlinks and
  bookmarks), we recommend to include \verb|~~/lib/texinputs/pdfsetup.sty| as well.

  \medskip As a final step of Isabelle document preparation, \hyperlink{tool.document}{\mbox{\isa{\isatool{document}}}}~\verb|-c| is run on the resulting copy of the
  \verb|document| directory.  Thus the actual output document is
  built and installed in its proper place.  The generated sources are
  deleted after successful run of {\LaTeX} and friends.

  Some care is needed if the document output location is configured
  differently, say within a directory whose content is still required
  afterwards!%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Running {\LaTeX} within the Isabelle environment
  \label{sec:tool-latex}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{latex}\hypertarget{tool.latex}{\hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}}} tool provides the basic interface for
  Isabelle document preparation.  Its usage is:
\begin{ttbox}
Usage: isabelle latex [OPTIONS] [FILE]

  Options are:
    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
                 ps.gz, pdf, bbl, idx, sty, syms

  Run LaTeX (and related tools) on FILE (default root.tex),
  producing the specified output format.
\end{ttbox}

  Appropriate {\LaTeX}-related programs are run on the input file,
  according to the given output format: \hyperlink{executable.latex}{\mbox{\isa{\isatt{latex}}}},
  \hyperlink{executable.pdflatex}{\mbox{\isa{\isatt{pdflatex}}}}, \hyperlink{executable.dvips}{\mbox{\isa{\isatt{dvips}}}}, \hyperlink{executable.bibtex}{\mbox{\isa{\isatt{bibtex}}}}
  (for \verb|bbl|), and \hyperlink{executable.makeindex}{\mbox{\isa{\isatt{makeindex}}}} (for \verb|idx|).  The actual commands are determined from the settings
  environment (\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LATEX}}}} etc.).

  The \verb|sty| output format causes the Isabelle style files to
  be updated from the distribution.  This is useful in special
  situations where the document sources are to be processed another
  time by separate tools.

  The \verb|syms| output is for internal use; it generates lists
  of symbols that are available without loading additional {\LaTeX}
  packages.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Examples%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Invoking \hyperlink{tool.latex}{\mbox{\isa{\isatool{latex}}}} by hand may be occasionally useful when
  debugging failed attempts of the automatic document preparation
  stage of batch-mode Isabelle.  The abortive process leaves the
  sources at a certain place within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}},
  see the runtime error message for details.  This enables users to
  inspect {\LaTeX} runs in further detail, e.g.\ like this:

\begin{ttbox}
  cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
  isabelle latex -o pdf
\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: