wenzelm@48578: theory Sessions
wenzelm@48578: imports Base
wenzelm@48578: begin
wenzelm@48578: 
wenzelm@48584: chapter {* Isabelle sessions and build management \label{ch:session} *}
wenzelm@48584: 
wenzelm@48584: text {* An Isabelle \emph{session} consists of a collection of related
wenzelm@48584:   theories that are associated with an optional formal document (see
wenzelm@48584:   also \chref{ch:present}).  There is also a notion of persistent
wenzelm@48584:   \emph{heap image} to capture the state of a session, similar to
wenzelm@48584:   object-code in compiled programming languages.
wenzelm@48578: 
wenzelm@48584:   Thus the concept of session resembles that of a ``project'' in
wenzelm@48584:   common IDE environments, but our specific name emphasizes the
wenzelm@48584:   connection to interactive theorem proving: the session wraps-up the
wenzelm@48584:   results of user-interaction with the prover in a persistent form.
wenzelm@48584: 
wenzelm@48584:   \medskip Application sessions are built on a given parent session.
wenzelm@48584:   The resulting hierarchy eventually leads to some major object-logic
wenzelm@48584:   session, notably @{text "HOL"}, which itself is based on @{text
wenzelm@48584:   "Pure"} as the common root.
wenzelm@48584: 
wenzelm@48584:   Processing sessions may take considerable time.  The tools for
wenzelm@48584:   Isabelle build management help to organize this efficiently,
wenzelm@48584:   including support for parallel build jobs --- in addition to the
wenzelm@48584:   multithreaded theory and proof checking that is already provided by
wenzelm@48584:   the prover process.
wenzelm@48584: *}
wenzelm@48578: 
wenzelm@48578: section {* Session ROOT specifications \label{sec:session-root} *}
wenzelm@48578: 
wenzelm@48579: text {* Session specifications reside in files called @{verbatim ROOT}
wenzelm@48579:   within certain directories, such as the home locations of registered
wenzelm@48579:   Isabelle components or additional project directories given by the
wenzelm@48579:   user.
wenzelm@48579: 
wenzelm@48579:   The ROOT file format follows the lexical conventions of the
wenzelm@48579:   \emph{outer syntax} of Isabelle/Isar, see also
wenzelm@48579:   \cite{isabelle-isar-ref}.  This defines common forms like
wenzelm@48579:   identifiers, names, quoted strings, verbatim text, nested comments
wenzelm@48579:   etc.  The grammar for a single @{syntax session_entry} is given as
wenzelm@48579:   syntax diagram below; each ROOT file may contain multiple session
wenzelm@48579:   specifications like this.
wenzelm@48579: 
wenzelm@48582:   Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
wenzelm@48582:   mode @{verbatim "isabelle-root"} for session ROOT files.
wenzelm@48579: 
wenzelm@48579:   @{rail "
wenzelm@48579:     @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
wenzelm@48579:     ;
wenzelm@48579:     body: description? options? ( theories * ) files?
wenzelm@48579:     ;
wenzelm@48579:     spec: @{syntax name} '!'? groups? dir?
wenzelm@48579:     ;
wenzelm@48579:     groups: '(' (@{syntax name} +) ')'
wenzelm@48579:     ;
wenzelm@48579:     dir: @'in' @{syntax name}
wenzelm@48579:     ;
wenzelm@48579:     description: @'description' @{syntax text}
wenzelm@48579:     ;
wenzelm@48579:     options: @'options' opts
wenzelm@48579:     ;
wenzelm@48579:     opts: '[' ( (@{syntax name} '=' @{syntax name} | @{syntax name}) + ',' ) ']'
wenzelm@48579:     ;
wenzelm@48579:     theories: @'theories' opts? ( @{syntax name} + )
wenzelm@48579:     ;
wenzelm@48579:     files: @'files' ( @{syntax name} + )
wenzelm@48579:     "}
wenzelm@48579: 
wenzelm@48579:   \begin{description}
wenzelm@48579: 
wenzelm@48579:   \item \isakeyword{session}~@{text "A = B + body"} defines a new
wenzelm@48579:   session @{text "A"} based on parent session @{text "B"}, with its
wenzelm@48579:   content given in @{text body} (theories and auxiliary source files).
wenzelm@48579:   Note that a parent (like @{text "HOL"}) is mandatory in practical
wenzelm@48579:   applications: only Isabelle/Pure can bootstrap itself from nothing.
wenzelm@48579: 
wenzelm@48579:   All such session specifications together describe a hierarchy (tree)
wenzelm@48579:   of sessions, with globally unique names.  By default, names are
wenzelm@48579:   derived from parent ones by concatenation, i.e.\ @{text "B\<dash>A"}
wenzelm@48579:   above.  Cumulatively, this leads to session paths of the form @{text
wenzelm@48579:   "X\<dash>Y\<dash>Z\<dash>W"}.  Note that in the specification,
wenzelm@48579:   @{text B} is already such a fully-qualified name, while @{text "A"}
wenzelm@48579:   is the new base name.
wenzelm@48579: 
wenzelm@48579:   \item \isakeyword{session}~@{text "A! = B"} indicates a fresh start
wenzelm@48579:   in the naming scheme: the session is called just @{text "A"} instead
wenzelm@48579:   of @{text "B\<dash>A"}.  Here the name @{text "A"} should be
wenzelm@48579:   sufficiently long to stand on its own in a potentially large
wenzelm@48579:   library.
wenzelm@48579: 
wenzelm@48579:   \item \isakeyword{session}~@{text "A (groups)"} indicates a
wenzelm@48579:   collection of groups where the new session is a member.  Group names
wenzelm@48579:   are uninterpreted and merely follow certain conventions.  For
wenzelm@48579:   example, the Isabelle distribution tags some important sessions by
wenzelm@48579:   the group name @{text "main"}.  Other projects may invent their own
wenzelm@48579:   conventions, which requires some care to avoid clashes within this
wenzelm@48579:   unchecked name space.
wenzelm@48579: 
wenzelm@48579:   \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
wenzelm@48579:   specifies an explicit directory for this session.  By default,
wenzelm@48579:   \isakeyword{session}~@{text "A"} abbreviates
wenzelm@48579:   \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "A"}.  This
wenzelm@48579:   accommodates the common scheme where some base directory contains
wenzelm@48579:   several sessions in sub-directories of corresponding names.  Another
wenzelm@48579:   common scheme is \isakeyword{session}~@{text
wenzelm@48579:   "A"}~\isakeyword{in}~@{verbatim "\".\""} to refer to the current
wenzelm@48579:   directory of the ROOT file.
wenzelm@48579: 
wenzelm@48579:   All theories and auxiliary source files are located relatively to
wenzelm@48579:   the session directory.  The prover process is run within the same as
wenzelm@48579:   its current working directory.
wenzelm@48579: 
wenzelm@48579:   \item \isakeyword{description}~@{text "text"} is a free-form
wenzelm@48579:   annotation for this session.
wenzelm@48579: 
wenzelm@48579:   \item \isakeyword{options}~@{text "[x = a, y = b, z]"} defines
wenzelm@48579:   separate options that are used when processing this session, but
wenzelm@48579:   \emph{without} propagation to child sessions; see also
wenzelm@48579:   \secref{sec:system-options}.  Note that @{text "z"} abbreviates
wenzelm@48579:   @{text "z = true"} for Boolean options.
wenzelm@48579: 
wenzelm@48579:   \item \isakeyword{theories}~@{text "options names"} specifies a
wenzelm@48579:   block of theories that are processed within an environment that is
wenzelm@48579:   augmented further by the given options, in addition to the global
wenzelm@48579:   session options given before.  Any number of blocks of
wenzelm@48579:   \isakeyword{theories} may be given.  Options are only active for
wenzelm@48579:   each \isakeyword{theories} block separately.
wenzelm@48579: 
wenzelm@48579:   \item \isakeyword{files}~@{text "files"} lists additional source
wenzelm@48579:   files that are somehow involved in the processing of this session.
wenzelm@48579:   This should cover anything outside the formal content of the theory
wenzelm@48579:   sources, say some auxiliary {\TeX} files that are required for
wenzelm@48579:   document processing.  In contrast, files that are specified in
wenzelm@48579:   formal theory headers as @{keyword "uses"} need not be declared
wenzelm@48579:   again.
wenzelm@48579: 
wenzelm@48579:   \end{description}
wenzelm@48580: *}
wenzelm@48579: 
wenzelm@48580: subsubsection {* Examples *}
wenzelm@48580: 
wenzelm@48580: text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
wenzelm@48580:   relevant situations. *}
wenzelm@48578: 
wenzelm@48578: 
wenzelm@48578: section {* System build options \label{sec:system-options} *}
wenzelm@48578: 
wenzelm@48580: text {* See @{file "~~/etc/options"} for the main defaults provided by
wenzelm@48582:   the Isabelle distribution.  Isabelle/jEdit (\secref{sec:tool-jedit})
wenzelm@48582:   includes a simple editing mode @{verbatim "isabelle-options"} for
wenzelm@48582:   this file-format.
wenzelm@48580: *}
wenzelm@48578: 
wenzelm@48578: 
wenzelm@48578: section {* Invoking the build process \label{sec:tool-build} *}
wenzelm@48578: 
wenzelm@48578: text {* The @{tool_def build} utility invokes the build process for
wenzelm@48578:   Isabelle sessions.  It manages dependencies between sessions,
wenzelm@48578:   related sources of theories and auxiliary files, and target heap
wenzelm@48578:   images.  Accordingly, it runs instances of the prover process with
wenzelm@48578:   optional document preparation.  Its command-line usage
wenzelm@48578:   is:\footnote{Isabelle/Scala provides the same functionality via
wenzelm@48578:   \texttt{isabelle.Build.build}.}
wenzelm@48578: \begin{ttbox} Usage: isabelle build [OPTIONS] [SESSIONS ...]
wenzelm@48578: 
wenzelm@48578:   Options are:
wenzelm@48578:     -a           select all sessions
wenzelm@48578:     -b           build heap images
wenzelm@48595:     -c           clean build
wenzelm@48578:     -d DIR       include session directory with ROOT file
wenzelm@48578:     -g NAME      select session group NAME
wenzelm@48578:     -j INT       maximum number of parallel jobs (default 1)
wenzelm@48578:     -n           no build -- test dependencies only
wenzelm@48578:     -o OPTION    override session configuration OPTION
wenzelm@48578:                  (via NAME=VAL or NAME)
wenzelm@48578:     -s           system build mode: produce output in ISABELLE_HOME
wenzelm@48578:     -v           verbose
wenzelm@48578: 
wenzelm@48578:   Build and manage Isabelle sessions, depending on implicit
wenzelm@48578:   ISABELLE_BUILD_OPTIONS="..."
wenzelm@48578: 
wenzelm@48578:   ML_PLATFORM="..."
wenzelm@48578:   ML_HOME="..."
wenzelm@48578:   ML_SYSTEM="..."
wenzelm@48578:   ML_OPTIONS="..."
wenzelm@48578: \end{ttbox}
wenzelm@48578: 
wenzelm@48578:   \medskip Isabelle sessions are defined via session ROOT files as
wenzelm@48578:   described in (\secref{sec:session-root}).  The totality of sessions
wenzelm@48578:   is determined by collecting such specifications from all Isabelle
wenzelm@48578:   component directories (\secref{sec:components}), augmented by more
wenzelm@48578:   directories given via options @{verbatim "-d"}~@{text "DIR"} on the
wenzelm@48578:   command line.  Each such directory may contain a session
wenzelm@48578:   \texttt{ROOT} file and an additional catalog file @{verbatim
wenzelm@48578:   "etc/sessions"} with further sub-directories (list of lines).  Note
wenzelm@48578:   that a single \texttt{ROOT} file usually defines many sessions;
haftmann@48591:   catalogs are only required for extra scalability and modularity
wenzelm@48578:   of large libraries.
wenzelm@48578: 
wenzelm@48578:   \medskip The subset of sessions to be managed is selected via
wenzelm@48578:   individual @{text "SESSIONS"} given as command-line arguments, or
wenzelm@48578:   session groups that are specified via one or more options @{verbatim
wenzelm@48578:   "-g"}~@{text "NAME"}.  Option @{verbatim "-a"} selects all sessions.
wenzelm@48578:   The build tool takes the hierarchy of sessions into account: the
wenzelm@48578:   selected set of sessions is completed by including all ancestors
wenzelm@48578:   according to the dependency structure.
wenzelm@48578: 
wenzelm@48578:   \medskip The build process depends on additional options that are
wenzelm@48578:   passed to the prover session eventually, see also
wenzelm@48578:   (\secref{sec:system-options}).  The settings variable @{setting_ref
wenzelm@48578:   ISABELLE_BUILD_OPTIONS} allows to provide additional defaults.
wenzelm@48578:   Moreover, the environment of system build options may be augmented
wenzelm@48578:   on the command line via @{verbatim "-o"}~@{text "NAME=VALUE"} or
wenzelm@48578:   @{verbatim "-o"}~@{text "NAME"}, which abbreviates @{verbatim
wenzelm@48578:   "-o"}~@{text "NAME=true"} for Boolean options.  Multiple occurrences
wenzelm@48578:   of @{verbatim "-o"} on the command-line are applied in the given
wenzelm@48578:   order.
wenzelm@48578: 
wenzelm@48578:   \medskip Option @{verbatim "-b"} ensures that heap images are
wenzelm@48578:   produced for all selected sessions.  By default, images are only
wenzelm@48578:   saved for inner nodes of the hierarchy of sessions, as required for
wenzelm@48578:   other sessions to continue later on.
wenzelm@48578: 
wenzelm@48595:   \medskip Option @{verbatim "-c"} cleans all descendants of the
wenzelm@48595:   selected sessions before performing the specified build operation.
wenzelm@48595: 
wenzelm@48595:   \medskip Option @{verbatim "-n"} omits the actual build process
wenzelm@48595:   after the preparatory stage (including optional cleanup).  Note that
wenzelm@48595:   the return code always indicates the status of the set of selected
wenzelm@48595:   sessions.
wenzelm@48595: 
wenzelm@48578:   \medskip Option @{verbatim "-j"} specifies the maximum number of
wenzelm@48578:   parallel build jobs (prover processes).  Note that each process is
wenzelm@48578:   subject to a separate limit of parallel threads, cf.\ system option
wenzelm@48578:   @{system_option_ref threads}.
wenzelm@48578: 
wenzelm@48578:   \medskip Option @{verbatim "-s"} enables \emph{system mode}, which
wenzelm@48578:   means that resulting heap images and log files are stored in
wenzelm@48578:   @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location
wenzelm@48578:   @{setting ISABELLE_OUTPUT} (which is normally in @{setting
wenzelm@48578:   ISABELLE_HOME_USER}, i.e.\ the user's home directory).
wenzelm@48578: 
wenzelm@48578:   \medskip Option @{verbatim "-v"} enables verbose mode.
wenzelm@48578: *}
wenzelm@48578: 
wenzelm@48578: subsubsection {* Examples *}
wenzelm@48578: 
wenzelm@48578: text {*
wenzelm@48578:   Build a specific logic image:
wenzelm@48578: \begin{ttbox}
wenzelm@48578: isabelle build -b HOLCF
wenzelm@48578: \end{ttbox}
wenzelm@48578: 
wenzelm@48595:   \smallskip Build the main group of logic images (as determined by
wenzelm@48595:   the session ROOT specifications of the Isabelle distribution):
wenzelm@48578: \begin{ttbox}
wenzelm@48578: isabelle build -b -g main
wenzelm@48578: \end{ttbox}
wenzelm@48578: 
wenzelm@48595:   \smallskip Provide a general overview of the status of all Isabelle
wenzelm@48595:   sessions, without building anything:
wenzelm@48578: \begin{ttbox}
wenzelm@48578: isabelle build -a -n -v
wenzelm@48578: \end{ttbox}
wenzelm@48578: 
wenzelm@48595:   \smallskip Build all sessions with HTML browser info and PDF
wenzelm@48595:   document preparation:
wenzelm@48578: \begin{ttbox}
wenzelm@48578: isabelle build -a -o browser_info -o document=pdf
wenzelm@48578: \end{ttbox}
wenzelm@48578: 
wenzelm@48595:   \smallskip Build all sessions with a maximum of 8 prover processes
wenzelm@48595:   and 4 threads each (on a machine with many cores):
wenzelm@48578: \begin{ttbox}
wenzelm@48578: isabelle build -a -j8 -o threads=4
wenzelm@48578: \end{ttbox}
wenzelm@48595: 
wenzelm@48595:   \smallskip Build some session images with cleanup of their
wenzelm@48595:   descendants, while retaining their ancestry:
wenzelm@48595: \begin{ttbox}
wenzelm@48595: isabelle build -b -c HOL-Boogie HOL-SPARK
wenzelm@48595: \end{ttbox}
wenzelm@48595: 
wenzelm@48595:   \smallskip Clean all sessions without building anything:
wenzelm@48595: \begin{ttbox}
wenzelm@48595: isabelle build -a -n -c
wenzelm@48595: \end{ttbox}
wenzelm@48578: *}
wenzelm@48578: 
wenzelm@48578: end