src/Doc/System/Presentation.thy

reconcile object-logic constraint vs. mixfix constraint;

(*:maxLineLen=78:*)

theory Presentation
imports Base
begin

chapter \<open>Presenting theories \label{ch:present}\<close>

text \<open>
  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>\<open>sessions\<close>
  (\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 @{tool_ref mkroot} and @{tool_ref build} provide the primary means
  for managing Isabelle sessions, including proper setup for presentation;
  @{tool build} tells the Isabelle process to run any additional stages
  required for document preparation, notably the @{tool_ref document} and
  @{tool_ref 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}}

      @{tool_ref mkroot} & invoked once by the user to initialize the
      session \<^verbatim>\<open>ROOT\<close> with optional \<^verbatim>\<open>document\<close>
      directory; \\

      @{tool_ref build} & invoked repeatedly by the user to keep
      session output up-to-date (HTML, documents etc.); \\

      @{tool_ref process} & run through @{tool_ref build}; \\

      @{tool_ref document} & run by the Isabelle process if document
      preparation is enabled; \\

      @{tool_ref latex} & universal {\LaTeX} tool wrapper invoked
      multiple times by @{tool_ref document}; also useful for manual
      experiments; \\

  \end{tabular}
  \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
  \end{center}
  \end{figure}
\<close>


section \<open>Generating HTML browser information \label{sec:info}\<close>

text \<open>
  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 of a session in an index file. As a second hierarchy, groups of
  sessions are organized as \<^emph>\<open>chapters\<close>, with a separate index. Note that the
  implicit tree structure of the session build hierarchy is \<^emph>\<open>not\<close> relevant
  for the presentation.

  \<^medskip>
  To generate theory browsing information for an existing session, just invoke
  @{tool build} with suitable options:
  @{verbatim [display] \<open>isabelle build -o browser_info -v -c FOL\<close>}

  The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
  reported by the above verbose invocation of the build process.

  Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in @{file
  "~~/src/HOL/Library"}) also provide printable documents in PDF. These are
  prepared automatically as well if enabled like this:
  @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}

  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 @{setting_ref ISABELLE_BROWSER_INFO} setting plus a prefix
  corresponding to the session chapter and identifier. In order to present
  Isabelle applications on the web, the corresponding subdirectory from
  @{setting ISABELLE_BROWSER_INFO} can be put on a WWW server.
\<close>


section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close>

text \<open>
  The @{tool_def mkroot} tool configures a given directory as session root,
  with some \<^verbatim>\<open>ROOT\<close> file and optional document source directory. Its usage is:
  @{verbatim [display]
\<open>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).\<close>}

  The results are placed in the given directory \<open>dir\<close>, which refers to the
  current directory by default. The @{tool 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 \<^verbatim>\<open>-d\<close> indicates that the session shall be accompanied by a formal
  document, with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see
  also \chref{ch:present}).

  Option \<^verbatim>\<open>-n\<close> allows to specify an alternative session name; otherwise the
  base name of the given directory is used.

  \<^medskip>
  The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies
  the parent session, and @{setting ISABELLE_DOCUMENT_FORMAT} the document
  format to be filled filled into the generated \<^verbatim>\<open>ROOT\<close> file.
\<close>


subsubsection \<open>Examples\<close>

text \<open>
  Produce session \<^verbatim>\<open>Test\<close> (with document preparation) within a separate
  directory of the same name:
  @{verbatim [display] \<open>isabelle mkroot -d Test && isabelle build -D Test\<close>}

  \<^medskip>
  Upgrade the current directory into a session ROOT with document preparation,
  and build it:
  @{verbatim [display] \<open>isabelle mkroot -d && isabelle build -D .\<close>}
\<close>


section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close>

text \<open>
  The @{tool_def document} tool prepares logic session documents, processing
  the sources as provided by the user and generated by Isabelle. Its usage is:
  @{verbatim [display]
\<open>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: pdf (default), dvi
    -t TAGS      specify tagged region markup

  Prepare the theory session document in DIR (default 'document')
  producing the specified output format.\<close>}

  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 \<^verbatim>\<open>-c\<close> option tells @{tool 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 \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format,
  the default is ``\<^verbatim>\<open>document.dvi\<close>''. Note that the result will appear in the
  parent of the target \<^verbatim>\<open>DIR\<close>.

  \<^medskip>
  The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
  regions. Tags are specified as a comma separated list of modifier/name
  pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
  drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
  equivalent to the tag specification
  ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
  \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in @{file
  "~~/lib/texinputs/isabelle.sty"}.

  \<^medskip>
  Document preparation requires a \<^verbatim>\<open>document\<close> 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, @{tool document} is smart enough to create any
  of the specified output formats, taking \<^verbatim>\<open>root.tex\<close> supplied by the user as
  a starting point. This even includes multiple runs of {\LaTeX} to
  accommodate references and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close>
  within the same directory).

  In more complex situations, a separate \<^verbatim>\<open>build\<close> 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.\ \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and
  default variants). The main work can be again delegated to @{tool latex},
  but it is also possible to harvest generated {\LaTeX} sources and copy them
  elsewhere.

  \<^medskip>
  When running the session, Isabelle copies the content of the original
  \<^verbatim>\<open>document\<close> directory into its proper place within @{setting
  ISABELLE_BROWSER_INFO}, according to the session path and document variant.
  Then, for any processed theory \<open>A\<close> some {\LaTeX} source is generated and put
  there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>. Furthermore, a list of all generated theory files is
  put into \<^verbatim>\<open>session.tex\<close>. Typically, the root {\LaTeX} file provided by the
  user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the
  theories.

  The {\LaTeX} versions of the theories require some macros defined in @{file
  "~~/lib/texinputs/isabelle.sty"}. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
  \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an
  appropriate path specification for {\TeX} inputs.

  If the text contains any references to Isabelle symbols (such as \<^verbatim>\<open>\<forall>\<close>) then
  \<^verbatim>\<open>isabellesym.sty\<close> should be included as well. This package contains a
  standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to
  \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, 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 @{file
  "~~/lib/texinputs/isabellesym.sty"} of the Isabelle distribution.

  For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),
  we recommend to include @{file "~~/lib/texinputs/pdfsetup.sty"} as well.

  \<^medskip>
  As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
  run on the resulting copy of the \<^verbatim>\<open>document\<close> 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!
\<close>


section \<open>Running {\LaTeX} within the Isabelle environment
  \label{sec:tool-latex}\<close>

text \<open>
  The @{tool_def latex} tool provides the basic interface for Isabelle
  document preparation. Its usage is:
  @{verbatim [display]
\<open>Usage: isabelle latex [OPTIONS] [FILE]

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

  Run LaTeX (and related tools) on FILE (default root.tex),
  producing the specified output format.\<close>}

  Appropriate {\LaTeX}-related programs are run on the input file, according
  to the given output format: @{executable latex}, @{executable pdflatex},
  @{executable dvips}, @{executable bibtex} (for \<^verbatim>\<open>bbl\<close>), and @{executable
  makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands are determined from the
  settings environment (@{setting ISABELLE_PDFLATEX} etc.).

  The \<^verbatim>\<open>sty\<close> 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 \<^verbatim>\<open>syms\<close> output is for internal use; it generates lists of symbols that
  are available without loading additional {\LaTeX} packages.
\<close>


subsubsection \<open>Examples\<close>

text \<open>
  Invoking @{tool 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
  @{setting ISABELLE_BROWSER_INFO}, see the runtime error message for details.
  This enables users to inspect {\LaTeX} runs in further detail, e.g.\ like
  this:

  @{verbatim [display]
\<open>cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
isabelle latex -o pdf\<close>}
\<close>

end