wenzelm@48578: theory Sessions
wenzelm@48578: imports Base
wenzelm@48578: begin
wenzelm@48578: 
wenzelm@48578: chapter {* Isabelle sessions and build management *}
wenzelm@48578: 
wenzelm@48578: text {* FIXME *}
wenzelm@48578: 
wenzelm@48578: section {* Session ROOT specifications \label{sec:session-root} *}
wenzelm@48578: 
wenzelm@48578: text {* FIXME *}
wenzelm@48578: 
wenzelm@48578: 
wenzelm@48578: section {* System build options \label{sec:system-options} *}
wenzelm@48578: 
wenzelm@48578: text {* FIXME *}
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@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;
wenzelm@48578:   catalogs are 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@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 "-n"} omits the actual build process
wenzelm@48578:   after performing all dependency checks.  The return code indicates
wenzelm@48578:   the status of the set of selected sessions.
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@48578:   Build the main group of logic images (as determined by the session
wenzelm@48578:   ROOT specifications of the Isabelle distribution):
wenzelm@48578: \begin{ttbox}
wenzelm@48578: isabelle build -b -g main
wenzelm@48578: \end{ttbox}
wenzelm@48578: 
wenzelm@48578:   Provide a general overview of the status of all Isabelle sessions,
wenzelm@48578:   without building anything:
wenzelm@48578: \begin{ttbox}
wenzelm@48578: isabelle build -a -n -v
wenzelm@48578: \end{ttbox}
wenzelm@48578: 
wenzelm@48578:   Build all sessions with HTML browser info and PDF document
wenzelm@48578:   preparation:
wenzelm@48578: \begin{ttbox}
wenzelm@48578: isabelle build -a -o browser_info -o document=pdf
wenzelm@48578: \end{ttbox}
wenzelm@48578: 
wenzelm@48578:   Build all sessions with a maximum of 8 prover processes and 4
wenzelm@48578:   threads each (on a machine with many cores):
wenzelm@48578: 
wenzelm@48578: \begin{ttbox}
wenzelm@48578: isabelle build -a -j8 -o threads=4
wenzelm@48578: \end{ttbox}
wenzelm@48578: *}
wenzelm@48578: 
wenzelm@48578: end