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@51055:   theories that may be associated with formal documents
wenzelm@51055:   (\chref{ch:present}).  There is also a notion of \emph{persistent
wenzelm@48604:   heap} image to capture the state of a session, similar to
wenzelm@48604:   object-code in compiled programming languages.  Thus the concept of
wenzelm@48604:   session resembles that of a ``project'' in common IDE environments,
wenzelm@48604:   but the specific name emphasizes the connection to interactive
wenzelm@48604:   theorem proving: the session wraps-up the results of
wenzelm@48604:   user-interaction with the prover in a persistent form.
wenzelm@48584: 
wenzelm@48604:   Application sessions are built on a given parent session, which may
wenzelm@48604:   be built recursively on other parents.  Following this path in the
wenzelm@48604:   hierarchy eventually leads to some major object-logic session like
wenzelm@48604:   @{text "HOL"}, which itself is based on @{text "Pure"} as the common
wenzelm@48604:   root of all sessions.
wenzelm@48584: 
wenzelm@48604:   Processing sessions may take considerable time.  Isabelle build
wenzelm@48604:   management helps to organize this efficiently.  This includes
wenzelm@48604:   support for parallel build jobs, in addition to the multithreaded
wenzelm@48604:   theory and proof checking that is already provided by the prover
wenzelm@48604:   process itself.  *}
wenzelm@48604: 
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@51417:   etc.  The grammar for @{syntax session_chapter} and @{syntax
wenzelm@51417:   session_entry} is given as syntax diagram below; each ROOT file may
wenzelm@51417:   contain multiple specifications like this.  Chapters help to
wenzelm@51417:   organize browser info (\secref{sec:info}), but have no formal
wenzelm@51417:   meaning.  The default chapter is ``@{text "Unsorted"}''.
wenzelm@48579: 
wenzelm@48582:   Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
wenzelm@51055:   mode @{verbatim "isabelle-root"} for session ROOT files, which is
wenzelm@51055:   enabled by default for any file of that name.
wenzelm@48579: 
wenzelm@48579:   @{rail "
wenzelm@51417:     @{syntax_def session_chapter}: @'chapter' @{syntax name}
wenzelm@51417:     ;
wenzelm@51417: 
wenzelm@48579:     @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
wenzelm@48579:     ;
wenzelm@48916:     body: description? options? ( theories + ) files?
wenzelm@48579:     ;
wenzelm@48738:     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@48605:     opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
wenzelm@48605:     ;
wenzelm@48605:     value: @{syntax name} | @{syntax real}
wenzelm@48579:     ;
wenzelm@48739:     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@48738:   of sessions, with globally unique names.  The new session name
wenzelm@51055:   @{text "A"} should be sufficiently long and descriptive to stand on
wenzelm@51055:   its own in a potentially large 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@48604:   the group name called ``@{text "main"}''.  Other projects may invent
wenzelm@48604:   their own conventions, but this requires some care to avoid clashes
wenzelm@48604:   within this unchecked name space.
wenzelm@48579: 
wenzelm@48579:   \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
wenzelm@48738:   specifies an explicit directory for this session; by default this is
wenzelm@48738:   the current directory of the @{verbatim 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@48604:   separate options (\secref{sec:system-options}) that are used when
wenzelm@48604:   processing this session, but \emph{without} propagation to child
wenzelm@48604:   sessions.  Note that @{text "z"} abbreviates @{text "z = true"} for
wenzelm@48604:   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@48604:   augmented by the given options, in addition to the global session
wenzelm@48604:   options given before.  Any number of blocks of \isakeyword{theories}
wenzelm@48604:   may be given.  Options are only active for each
wenzelm@48604:   \isakeyword{theories} block separately.
wenzelm@48579: 
wenzelm@48579:   \item \isakeyword{files}~@{text "files"} lists additional source
wenzelm@48604:   files that are involved in the processing of this session.  This
wenzelm@48604:   should cover anything outside the formal content of the theory
wenzelm@48579:   sources, say some auxiliary {\TeX} files that are required for
wenzelm@51055:   document processing.  In contrast, files that are loaded formally
wenzelm@51055:   within a theory, e.g.\ via @{keyword "ML_file"}, need not be
wenzelm@51055:   declared again.
wenzelm@48579: 
wenzelm@48579:   \end{description}
wenzelm@48580: *}
wenzelm@48579: 
wenzelm@51055: 
wenzelm@48580: subsubsection {* Examples *}
wenzelm@48580: 
wenzelm@48580: text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
wenzelm@51055:   relevant situations, although it uses relatively complex
wenzelm@51055:   quasi-hierarchic naming conventions like @{text "HOL\<dash>SPARK"},
wenzelm@51055:   @{text "HOL\<dash>SPARK\<dash>Examples"}.  An alternative is to use
wenzelm@48738:   unqualified names that are relatively long and descriptive, as in
wenzelm@48738:   the Archive of Formal Proofs (\url{http://afp.sf.net}), for
wenzelm@48738:   example. *}
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@48693: 
wenzelm@51055:   The following options are particulary relevant to build Isabelle
wenzelm@51055:   sessions, in particular with document preparation
wenzelm@51055:   (\chref{ch:present}).
wenzelm@51055: 
wenzelm@51055:   \begin{itemize}
wenzelm@51055: 
wenzelm@51055:   \item @{system_option_def "browser_info"} controls output of HTML
wenzelm@51055:   browser info, see also \secref{sec:info}.
wenzelm@51055: 
wenzelm@51055:   \item @{system_option_def "document"} specifies the document output
wenzelm@51055:   format, see @{tool document} option @{verbatim "-o"} in
wenzelm@51055:   \secref{sec:tool-document}.  In practice, the most relevant values
wenzelm@51055:   are @{verbatim "document=false"} or @{verbatim "document=pdf"}.
wenzelm@51055: 
wenzelm@51055:   \item @{system_option_def "document_output"} specifies an
wenzelm@51055:   alternative directory for generated output of the document
wenzelm@51055:   preparation system; the default is within the @{setting
wenzelm@51055:   "ISABELLE_BROWSER_INFO"} hierarchy as explained in
wenzelm@51055:   \secref{sec:info}.  See also @{tool mkroot}, which generates a
wenzelm@51055:   default configuration with output readily available to the author of
wenzelm@51055:   the document.
wenzelm@51055: 
wenzelm@51055:   \item @{system_option_def "document_variants"} specifies document
wenzelm@51055:   variants as a colon-separated list of @{text "name=tags"} entries,
wenzelm@51055:   corresponding to @{tool document} options @{verbatim "-n"} and
wenzelm@51055:   @{verbatim "-t"}.
wenzelm@51055: 
wenzelm@51055:   For example, @{verbatim
wenzelm@51055:   "document_variants=document:outline=/proof,/ML"} indicates two
wenzelm@51055:   documents: the one called @{verbatim document} with default tags,
wenzelm@51055:   and the other called @{verbatim outline} where proofs and ML
wenzelm@51055:   sections are folded.
wenzelm@51055: 
wenzelm@51055:   Document variant names are just a matter of conventions.  It is also
wenzelm@51055:   possible to use different document variant names (without tags) for
wenzelm@51055:   different document root entries, see also
wenzelm@51055:   \secref{sec:tool-document}.
wenzelm@51055: 
wenzelm@51055:   \item @{system_option_def "document_graph"} tells whether the
wenzelm@51055:   generated document files should include a theory graph (cf.\
wenzelm@51055:   \secref{sec:browse} and \secref{sec:info}).  The resulting EPS or
wenzelm@51055:   PDF file can be included as graphics in {\LaTeX}.
wenzelm@51055: 
wenzelm@51055:   Note that this option is usually determined as static parameter of
wenzelm@51055:   some session (e.g.\ within its @{verbatim ROOT} file) and \emph{not}
wenzelm@51055:   given globally or on the command line of @{tool build}.
wenzelm@51055: 
wenzelm@51055:   \item @{system_option_def "threads"} determines the number of worker
wenzelm@51055:   threads for parallel checking of theories and proofs.  The default
wenzelm@51055:   @{text "0"} means that a sensible maximum value is determined by the
wenzelm@51055:   underlying hardware.  For machines with many cores or with
wenzelm@51055:   hyperthreading, this is often requires manual adjustment (on the
wenzelm@51055:   command-line or within personal settings or preferences, not within
wenzelm@51055:   a session @{verbatim ROOT}).
wenzelm@51055: 
wenzelm@51055:   \item @{system_option_def "condition"} specifies a comma-separated
wenzelm@51055:   list of process environment variables (or Isabelle settings) that
wenzelm@51055:   are required for the subsequent theories to be processed.
wenzelm@51055:   Conditions are considered ``true'' if the corresponding environment
wenzelm@51055:   value is defined and non-empty.
wenzelm@51055: 
wenzelm@51055:   For example, the @{verbatim "condition=ISABELLE_FULL_TEST"} may be
wenzelm@51055:   used to guard extraordinary theories, which are meant to be enabled
wenzelm@51055:   explicitly via some shell prefix @{verbatim "env ISABELLE_FULL_TEST=true"}
wenzelm@51055:   before invoking @{tool build}.
wenzelm@51055: 
wenzelm@51055:   \item @{system_option_def "timeout"} specifies a real wall-clock
wenzelm@51055:   timeout (in seconds) for the session as a whole.  The timer is
wenzelm@51055:   controlled outside the ML process by the JVM that runs
wenzelm@51055:   Isabelle/Scala.  Thus it is relatively reliable in canceling
wenzelm@51055:   processes that get out of control, even if there is a deadlock
wenzelm@51055:   without CPU time usage.
wenzelm@51055: 
wenzelm@51055:   \end{itemize}
wenzelm@51055: 
wenzelm@48693:   The @{tool_def options} tool prints Isabelle system options.  Its
wenzelm@48693:   command-line usage is:
wenzelm@48693: \begin{ttbox}
wenzelm@48693: Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
wenzelm@48693: 
wenzelm@48693:   Options are:
wenzelm@48693:     -b           include $ISABELLE_BUILD_OPTIONS
wenzelm@50531:     -l           list options
wenzelm@48693:     -x FILE      export to FILE in YXML format
wenzelm@48693: 
wenzelm@50531:   Report Isabelle system options, augmented by MORE_OPTIONS given as
wenzelm@48693:   arguments NAME=VAL or NAME.
wenzelm@48693: \end{ttbox}
wenzelm@48693: 
wenzelm@48693:   The command line arguments provide additional system options of the
wenzelm@48693:   form @{text "name"}@{verbatim "="}@{text "value"} or @{text name}
wenzelm@48693:   for Boolean options.
wenzelm@48693: 
wenzelm@48693:   Option @{verbatim "-b"} augments the implicit environment of system
wenzelm@48693:   options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\
wenzelm@48693:   \secref{sec:tool-build}.
wenzelm@48693: 
wenzelm@48693:   Option @{verbatim "-x"} specifies a file to export the result in
wenzelm@48693:   YXML format, instead of printing it in human-readable form.
wenzelm@48580: *}
wenzelm@48578: 
wenzelm@48578: 
wenzelm@48578: section {* Invoking the build process \label{sec:tool-build} *}
wenzelm@48578: 
wenzelm@48602: text {* The @{tool_def build} tool 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@48602: \begin{ttbox}
wenzelm@48602: Usage: isabelle build [OPTIONS] [SESSIONS ...]
wenzelm@48578: 
wenzelm@48578:   Options are:
wenzelm@48737:     -D DIR       include session directory and select its sessions
wenzelm@49131:     -R           operate on requirements of selected sessions
wenzelm@48578:     -a           select all sessions
wenzelm@48578:     -b           build heap images
wenzelm@48595:     -c           clean build
wenzelm@48737:     -d DIR       include session directory
wenzelm@48578:     -g NAME      select session group NAME
wenzelm@48578:     -j INT       maximum number of parallel jobs (default 1)
wenzelm@48903:     -l           list session source files
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@48650:   \texttt{ROOT} file with several session specifications.
wenzelm@48578: 
wenzelm@48684:   Any session root directory may refer recursively to further
wenzelm@48684:   directories of the same kind, by listing them in a catalog file
wenzelm@48684:   @{verbatim "ROOTS"} line-by-line.  This helps to organize large
wenzelm@48684:   collections of session specifications, or to make @{verbatim "-d"}
wenzelm@48684:   command line options persistent (say within @{verbatim
wenzelm@48684:   "$ISABELLE_HOME_USER/ROOTS"}).
wenzelm@48684: 
wenzelm@48604:   \medskip The subset of sessions to be managed is determined via
wenzelm@48578:   individual @{text "SESSIONS"} given as command-line arguments, or
wenzelm@48604:   session groups that are given via one or more options @{verbatim
wenzelm@48578:   "-g"}~@{text "NAME"}.  Option @{verbatim "-a"} selects all sessions.
wenzelm@48604:   The build tool takes session dependencies into account: the set of
wenzelm@48604:   selected sessions is completed by including all ancestors.
wenzelm@48578: 
wenzelm@49131:   \medskip Option @{verbatim "-R"} reverses the selection in the sense
wenzelm@49131:   that it refers to its requirements: all ancestor sessions excluding
wenzelm@49131:   the original selection.  This allows to prepare the stage for some
wenzelm@49131:   build process with different options, before running the main build
wenzelm@49131:   itself (without option @{verbatim "-R"}).
wenzelm@49131: 
wenzelm@48737:   \medskip Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but
wenzelm@48737:   selects all sessions that are defined in the given directories.
wenzelm@48737: 
wenzelm@48604:   \medskip The build process depends on additional options
wenzelm@48604:   (\secref{sec:system-options}) that are passed to the prover
wenzelm@48604:   eventually.  The settings variable @{setting_ref
wenzelm@48604:   ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\
wenzelm@48604:   \texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,
wenzelm@48604:   the environment of system build options may be augmented on the
wenzelm@48604:   command line via @{verbatim "-o"}~@{text "name"}@{verbatim
wenzelm@48604:   "="}@{text "value"} or @{verbatim "-o"}~@{text "name"}, which
wenzelm@48604:   abbreviates @{verbatim "-o"}~@{text "name"}@{verbatim"=true"} for
wenzelm@48604:   Boolean options.  Multiple occurrences of @{verbatim "-o"} on the
wenzelm@48604:   command-line are applied in the given 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@48604:   parallel build jobs (prover processes).  Each prover process is
wenzelm@48604:   subject to a separate limit of parallel worker threads, cf.\ system
wenzelm@48604:   option @{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@48903:   \medskip Option @{verbatim "-v"} increases the general level of
wenzelm@48903:   verbosity.  Option @{verbatim "-l"} lists the source files that
wenzelm@48903:   contribute to a session.
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@48604:   \smallskip Build the main group of logic images:
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@48604:   \smallskip Build all sessions with a maximum of 8 parallel prover
wenzelm@48604:   processes and 4 worker 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@48737: 
wenzelm@48737:   \smallskip Build all sessions from some other directory hierarchy,
wenzelm@48737:   according to the settings variable @{verbatim "AFP"} that happens to
wenzelm@48737:   be defined inside the Isabelle environment:
wenzelm@48737: \begin{ttbox}
wenzelm@48737: isabelle build -D '$AFP'
wenzelm@48737: \end{ttbox}
wenzelm@49131: 
wenzelm@49131:   \smallskip Inform about the status of all sessions required for AFP,
wenzelm@49131:   without building anything yet:
wenzelm@49131: \begin{ttbox}
wenzelm@49131: isabelle build -D '$AFP' -R -v -n
wenzelm@49131: \end{ttbox}
wenzelm@48578: *}
wenzelm@48578: 
wenzelm@50406: 
wenzelm@50406: section {* Build dialog *}
wenzelm@50406: 
wenzelm@50406: text {* The @{tool_def build_dialog} provides a simple GUI wrapper to
wenzelm@50406:   the tool Isabelle @{tool build} tool.  This enables user interfaces
wenzelm@50406:   like Isabelle/jEdit \secref{sec:tool-jedit} to provide read-made
wenzelm@50406:   logic image on startup.  Its command-line usage is:
wenzelm@50406: \begin{ttbox}
wenzelm@50406: Usage: isabelle build_dialog [OPTIONS] LOGIC
wenzelm@50406: 
wenzelm@50406:   Options are:
wenzelm@50406:     -L OPTION    default logic via system option
wenzelm@50406:     -d DIR       include session directory
wenzelm@50546:     -l NAME      logic session name
wenzelm@50406:     -s           system build mode: produce output in ISABELLE_HOME
wenzelm@50406: 
wenzelm@50546:   Build Isabelle logic session image via GUI dialog (default: \$ISABELLE_LOGIC).
wenzelm@50406: \end{ttbox}
wenzelm@50406: 
wenzelm@50546:   \medskip Option @{verbatim "-l"} specifies an explicit logic session
wenzelm@50546:   name.  Option @{verbatim "-L"} specifies a system option name as
wenzelm@50546:   fall-back to determine the logic session name.  If both are omitted
wenzelm@50546:   or have empty value, @{setting ISABELLE_LOGIC} is used as default.
wenzelm@50406: 
wenzelm@50406:   \medskip Options @{verbatim "-d"} and @{verbatim "-s"} have the same
wenzelm@50546:   meaning as for the command-line @{tool build} tool itself.  *}
wenzelm@50406: 
wenzelm@48578: end