src/Doc/System/Sessions.thy

added isabelle-process option -o;

theory Sessions
imports Base
begin

chapter {* Isabelle sessions and build management \label{ch:session} *}

text {* An Isabelle \emph{session} consists of a collection of related
  theories that may be associated with formal documents
  (\chref{ch:present}).  There is also a notion of \emph{persistent
  heap} image to capture the state of a session, similar to
  object-code in compiled programming languages.  Thus the concept of
  session resembles that of a ``project'' in common IDE environments,
  but the specific name emphasizes the connection to interactive
  theorem proving: the session wraps-up the results of
  user-interaction with the prover in a persistent form.

  Application sessions are built on a given parent session, which may
  be built recursively on other parents.  Following this path in the
  hierarchy eventually leads to some major object-logic session like
  @{text "HOL"}, which itself is based on @{text "Pure"} as the common
  root of all sessions.

  Processing sessions may take considerable time.  Isabelle build
  management helps to organize this efficiently.  This includes
  support for parallel build jobs, in addition to the multithreaded
  theory and proof checking that is already provided by the prover
  process itself.  *}


section {* Session ROOT specifications \label{sec:session-root} *}

text {* Session specifications reside in files called @{verbatim ROOT}
  within certain directories, such as the home locations of registered
  Isabelle components or additional project directories given by the
  user.

  The ROOT file format follows the lexical conventions of the
  \emph{outer syntax} of Isabelle/Isar, see also
  \cite{isabelle-isar-ref}.  This defines common forms like
  identifiers, names, quoted strings, verbatim text, nested comments
  etc.  The grammar for @{syntax session_chapter} and @{syntax
  session_entry} is given as syntax diagram below; each ROOT file may
  contain multiple specifications like this.  Chapters help to
  organize browser info (\secref{sec:info}), but have no formal
  meaning.  The default chapter is ``@{text "Unsorted"}''.

  Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
  mode @{verbatim "isabelle-root"} for session ROOT files, which is
  enabled by default for any file of that name.

  @{rail "
    @{syntax_def session_chapter}: @'chapter' @{syntax name}
    ;

    @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
    ;
    body: description? options? ( theories + ) files?
    ;
    spec: @{syntax name} groups? dir?
    ;
    groups: '(' (@{syntax name} +) ')'
    ;
    dir: @'in' @{syntax name}
    ;
    description: @'description' @{syntax text}
    ;
    options: @'options' opts
    ;
    opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
    ;
    value: @{syntax name} | @{syntax real}
    ;
    theories: @'theories' opts? ( @{syntax name} * )
    ;
    files: @'files' ( @{syntax name} + )
    "}

  \begin{description}

  \item \isakeyword{session}~@{text "A = B + body"} defines a new
  session @{text "A"} based on parent session @{text "B"}, with its
  content given in @{text body} (theories and auxiliary source files).
  Note that a parent (like @{text "HOL"}) is mandatory in practical
  applications: only Isabelle/Pure can bootstrap itself from nothing.

  All such session specifications together describe a hierarchy (tree)
  of sessions, with globally unique names.  The new session name
  @{text "A"} should be sufficiently long and descriptive to stand on
  its own in a potentially large library.

  \item \isakeyword{session}~@{text "A (groups)"} indicates a
  collection of groups where the new session is a member.  Group names
  are uninterpreted and merely follow certain conventions.  For
  example, the Isabelle distribution tags some important sessions by
  the group name called ``@{text "main"}''.  Other projects may invent
  their own conventions, but this requires some care to avoid clashes
  within this unchecked name space.

  \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
  specifies an explicit directory for this session; by default this is
  the current directory of the @{verbatim ROOT} file.

  All theories and auxiliary source files are located relatively to
  the session directory.  The prover process is run within the same as
  its current working directory.

  \item \isakeyword{description}~@{text "text"} is a free-form
  annotation for this session.

  \item \isakeyword{options}~@{text "[x = a, y = b, z]"} defines
  separate options (\secref{sec:system-options}) that are used when
  processing this session, but \emph{without} propagation to child
  sessions.  Note that @{text "z"} abbreviates @{text "z = true"} for
  Boolean options.

  \item \isakeyword{theories}~@{text "options names"} specifies a
  block of theories that are processed within an environment that is
  augmented by the given options, in addition to the global session
  options given before.  Any number of blocks of \isakeyword{theories}
  may be given.  Options are only active for each
  \isakeyword{theories} block separately.

  \item \isakeyword{files}~@{text "files"} lists additional source
  files that are involved in the processing of this session.  This
  should cover anything outside the formal content of the theory
  sources, say some auxiliary {\TeX} files that are required for
  document processing.  In contrast, files that are loaded formally
  within a theory, e.g.\ via @{keyword "ML_file"}, need not be
  declared again.

  \end{description}
*}


subsubsection {* Examples *}

text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
  relevant situations, although it uses relatively complex
  quasi-hierarchic naming conventions like @{text "HOL\<dash>SPARK"},
  @{text "HOL\<dash>SPARK\<dash>Examples"}.  An alternative is to use
  unqualified names that are relatively long and descriptive, as in
  the Archive of Formal Proofs (\url{http://afp.sf.net}), for
  example. *}


section {* System build options \label{sec:system-options} *}

text {* See @{file "~~/etc/options"} for the main defaults provided by
  the Isabelle distribution.  Isabelle/jEdit (\secref{sec:tool-jedit})
  includes a simple editing mode @{verbatim "isabelle-options"} for
  this file-format.

  The following options are particulary relevant to build Isabelle
  sessions, in particular with document preparation
  (\chref{ch:present}).

  \begin{itemize}

  \item @{system_option_def "browser_info"} controls output of HTML
  browser info, see also \secref{sec:info}.

  \item @{system_option_def "document"} specifies the document output
  format, see @{tool document} option @{verbatim "-o"} in
  \secref{sec:tool-document}.  In practice, the most relevant values
  are @{verbatim "document=false"} or @{verbatim "document=pdf"}.

  \item @{system_option_def "document_output"} specifies an
  alternative directory for generated output of the document
  preparation system; the default is within the @{setting
  "ISABELLE_BROWSER_INFO"} hierarchy as explained in
  \secref{sec:info}.  See also @{tool mkroot}, which generates a
  default configuration with output readily available to the author of
  the document.

  \item @{system_option_def "document_variants"} specifies document
  variants as a colon-separated list of @{text "name=tags"} entries,
  corresponding to @{tool document} options @{verbatim "-n"} and
  @{verbatim "-t"}.

  For example, @{verbatim
  "document_variants=document:outline=/proof,/ML"} indicates two
  documents: the one called @{verbatim document} with default tags,
  and the other called @{verbatim outline} where proofs and ML
  sections are folded.

  Document variant names are just a matter of conventions.  It is also
  possible to use different document variant names (without tags) for
  different document root entries, see also
  \secref{sec:tool-document}.

  \item @{system_option_def "document_graph"} tells whether the
  generated document files should include a theory graph (cf.\
  \secref{sec:browse} and \secref{sec:info}).  The resulting EPS or
  PDF file can be included as graphics in {\LaTeX}.

  Note that this option is usually determined as static parameter of
  some session (e.g.\ within its @{verbatim ROOT} file) and \emph{not}
  given globally or on the command line of @{tool build}.

  \item @{system_option_def "threads"} determines the number of worker
  threads for parallel checking of theories and proofs.  The default
  @{text "0"} means that a sensible maximum value is determined by the
  underlying hardware.  For machines with many cores or with
  hyperthreading, this is often requires manual adjustment (on the
  command-line or within personal settings or preferences, not within
  a session @{verbatim ROOT}).

  \item @{system_option_def "condition"} specifies a comma-separated
  list of process environment variables (or Isabelle settings) that
  are required for the subsequent theories to be processed.
  Conditions are considered ``true'' if the corresponding environment
  value is defined and non-empty.

  For example, the @{verbatim "condition=ISABELLE_FULL_TEST"} may be
  used to guard extraordinary theories, which are meant to be enabled
  explicitly via some shell prefix @{verbatim "env ISABELLE_FULL_TEST=true"}
  before invoking @{tool build}.

  \item @{system_option_def "timeout"} specifies a real wall-clock
  timeout (in seconds) for the session as a whole.  The timer is
  controlled outside the ML process by the JVM that runs
  Isabelle/Scala.  Thus it is relatively reliable in canceling
  processes that get out of control, even if there is a deadlock
  without CPU time usage.

  \end{itemize}

  The @{tool_def options} tool prints Isabelle system options.  Its
  command-line usage is:
\begin{ttbox}
Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]

  Options are:
    -b           include $ISABELLE_BUILD_OPTIONS