%
\begin{isabellebody}%
\def\isabellecontext{Sessions}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Sessions\isanewline
\isakeyword{imports}\ Base\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Isabelle sessions and build management%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Session ROOT specifications \label{sec:session-root}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Session specifications reside in files called \verb|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 a single \hyperlink{syntax.session-entry}{\mbox{\isa{session{\isaliteral{5F}{\isacharunderscore}}entry}}} is given as
syntax diagram below; each ROOT file may contain multiple session
specifications like this.
Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
mode \verb|isabelle-root| for session ROOT files.
\begin{railoutput}
\rail@begin{2}{\indexdef{}{syntax}{session\_entry}\hypertarget{syntax.session-entry}{\hyperlink{syntax.session-entry}{\mbox{\isa{session{\isaliteral{5F}{\isacharunderscore}}entry}}}}}
\rail@term{\isa{\isakeyword{session}}}[]
\rail@nont{\isa{spec}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
\rail@endbar
\rail@nont{\isa{body}}[]
\rail@end
\rail@begin{2}{\isa{body}}
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{description}}[]
\rail@endbar
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{options}}[]
\rail@endbar
\rail@plus
\rail@nextplus{1}
\rail@cnont{\isa{theories}}[]
\rail@endplus
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{files}}[]
\rail@endbar
\rail@end
\rail@begin{2}{\isa{spec}}
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
\rail@endbar
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{groups}}[]
\rail@endbar
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{dir}}[]
\rail@endbar
\rail@end
\rail@begin{2}{\isa{groups}}
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@nextplus{1}
\rail@endplus
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@end
\rail@begin{1}{\isa{dir}}
\rail@term{\isa{\isakeyword{in}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@end
\rail@begin{1}{\isa{description}}
\rail@term{\isa{\isakeyword{description}}}[]
\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
\rail@end
\rail@begin{1}{\isa{options}}
\rail@term{\isa{\isakeyword{options}}}[]
\rail@nont{\isa{opts}}[]
\rail@end
\rail@begin{3}{\isa{opts}}
\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
\rail@plus
\rail@bar
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@endbar
\rail@nextplus{2}
\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
\rail@endplus
\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
\rail@end
\rail@begin{2}{\isa{theories}}
\rail@term{\isa{\isakeyword{theories}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{opts}}[]
\rail@endbar
\rail@plus
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
\rail@begin{2}{\isa{files}}
\rail@term{\isa{\isakeyword{files}}}[]
\rail@plus
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
\end{railoutput}
\begin{description}
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3D}{\isacharequal}}\ B\ {\isaliteral{2B}{\isacharplus}}\ body{\isaliteral{22}{\isachardoublequote}}} defines a new
session \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} based on parent session \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{22}{\isachardoublequote}}}, with its
content given in \isa{body} (theories and auxiliary source files).
Note that a parent (like \isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{22}{\isachardoublequote}}}) 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. By default, names are
derived from parent ones by concatenation, i.e.\ \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{5C3C646173683E}{\isasymdash}}A{\isaliteral{22}{\isachardoublequote}}}
above. Cumulatively, this leads to session paths of the form \isa{{\isaliteral{22}{\isachardoublequote}}X{\isaliteral{5C3C646173683E}{\isasymdash}}Y{\isaliteral{5C3C646173683E}{\isasymdash}}Z{\isaliteral{5C3C646173683E}{\isasymdash}}W{\isaliteral{22}{\isachardoublequote}}}. Note that in the specification,
\isa{B} is already such a fully-qualified name, while \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}
is the new base name.
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{21}{\isacharbang}}\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{22}{\isachardoublequote}}} indicates a fresh start
in the naming scheme: the session is called just \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} instead
of \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{5C3C646173683E}{\isasymdash}}A{\isaliteral{22}{\isachardoublequote}}}. Here the name \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} should be
sufficiently long to stand on its own in a potentially large
library.
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{28}{\isacharparenleft}}groups{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} 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 \isa{{\isaliteral{22}{\isachardoublequote}}main{\isaliteral{22}{\isachardoublequote}}}. Other projects may invent their own
conventions, which requires some care to avoid clashes within this
unchecked name space.
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}dir{\isaliteral{22}{\isachardoublequote}}}
specifies an explicit directory for this session. By default,
\isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} abbreviates
\isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}. This
accommodates the common scheme where some base directory contains
several sessions in sub-directories of corresponding names. Another
common scheme is \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\verb|"."| to refer to the current
directory of the 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}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} is a free-form
annotation for this session.
\item \isakeyword{options}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} defines
separate options that are used when processing this session, but
\emph{without} propagation to child sessions; see also
\secref{sec:system-options}. Note that \isa{{\isaliteral{22}{\isachardoublequote}}z{\isaliteral{22}{\isachardoublequote}}} abbreviates
\isa{{\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{22}{\isachardoublequote}}} for Boolean options.
\item \isakeyword{theories}~\isa{{\isaliteral{22}{\isachardoublequote}}options\ names{\isaliteral{22}{\isachardoublequote}}} specifies a
block of theories that are processed within an environment that is
augmented further 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}~\isa{{\isaliteral{22}{\isachardoublequote}}files{\isaliteral{22}{\isachardoublequote}}} lists additional source
files that are somehow 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 specified in
formal theory headers as \hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} need not be declared
again.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Examples%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
See \verb|~~/src/HOL/ROOT| for a diversity of practically
relevant situations.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{System build options \label{sec:system-options}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
See \verb|~~/etc/options| for the main defaults provided by
the Isabelle distribution. Isabelle/jEdit (\secref{sec:tool-jedit})
includes a simple editing mode \verb|isabelle-options| for
this file-format.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Invoking the build process \label{sec:tool-build}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{build}\hypertarget{tool.build}{\hyperlink{tool.build}{\mbox{\isa{\isatt{build}}}}} utility invokes the build process for
Isabelle sessions. It manages dependencies between sessions,
related sources of theories and auxiliary files, and target heap
images. Accordingly, it runs instances of the prover process with
optional document preparation. Its command-line usage
is:\footnote{Isabelle/Scala provides the same functionality via
\texttt{isabelle.Build.build}.}
\begin{ttbox} Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
-a select all sessions
-b build heap images
-d DIR include session directory with ROOT file
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
-n no build -- test dependencies only
-o OPTION override session configuration OPTION
(via NAME=VAL or NAME)
-s system build mode: produce output in ISABELLE_HOME
-v verbose
Build and manage Isabelle sessions, depending on implicit
ISABELLE_BUILD_OPTIONS="..."
ML_PLATFORM="..."
ML_HOME="..."
ML_SYSTEM="..."
ML_OPTIONS="..."
\end{ttbox}
\medskip Isabelle sessions are defined via session ROOT files as
described in (\secref{sec:session-root}). The totality of sessions
is determined by collecting such specifications from all Isabelle
component directories (\secref{sec:components}), augmented by more
directories given via options \verb|-d|~\isa{{\isaliteral{22}{\isachardoublequote}}DIR{\isaliteral{22}{\isachardoublequote}}} on the
command line. Each such directory may contain a session
\texttt{ROOT} file and an additional catalog file \verb|etc/sessions| with further sub-directories (list of lines). Note
that a single \texttt{ROOT} file usually defines many sessions;
catalogs are are only required for extra scalability and modularity
of large libraries.
\medskip The subset of sessions to be managed is selected via
individual \isa{{\isaliteral{22}{\isachardoublequote}}SESSIONS{\isaliteral{22}{\isachardoublequote}}} given as command-line arguments, or
session groups that are specified via one or more options \verb|-g|~\isa{{\isaliteral{22}{\isachardoublequote}}NAME{\isaliteral{22}{\isachardoublequote}}}. Option \verb|-a| selects all sessions.
The build tool takes the hierarchy of sessions into account: the
selected set of sessions is completed by including all ancestors
according to the dependency structure.
\medskip The build process depends on additional options that are
passed to the prover session eventually, see also
(\secref{sec:system-options}). The settings variable \indexref{}{setting}{ISABELLE\_BUILD\_OPTIONS}\hyperlink{setting.ISABELLE-BUILD-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BUILD{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}} allows to provide additional defaults.
Moreover, the environment of system build options may be augmented
on the command line via \verb|-o|~\isa{{\isaliteral{22}{\isachardoublequote}}NAME{\isaliteral{3D}{\isacharequal}}VALUE{\isaliteral{22}{\isachardoublequote}}} or
\verb|-o|~\isa{{\isaliteral{22}{\isachardoublequote}}NAME{\isaliteral{22}{\isachardoublequote}}}, which abbreviates \verb|-o|~\isa{{\isaliteral{22}{\isachardoublequote}}NAME{\isaliteral{3D}{\isacharequal}}true{\isaliteral{22}{\isachardoublequote}}} for Boolean options. Multiple occurrences
of \verb|-o| on the command-line are applied in the given
order.
\medskip Option \verb|-b| ensures that heap images are
produced for all selected sessions. By default, images are only
saved for inner nodes of the hierarchy of sessions, as required for
other sessions to continue later on.
\medskip Option \verb|-j| specifies the maximum number of
parallel build jobs (prover processes). Note that each process is
subject to a separate limit of parallel threads, cf.\ system option
\indexref{}{system option}{threads}\hyperlink{system option.threads}{\mbox{\isa{\isatt{threads}}}}.
\medskip Option \verb|-s| enables \emph{system mode}, which
means that resulting heap images and log files are stored in
\verb|$ISABELLE_HOME/heaps| instead of the default location
\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}} (which is normally in \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}}, i.e.\ the user's home directory).
\medskip Option \verb|-n| omits the actual build process
after performing all dependency checks. The return code indicates
the status of the set of selected sessions.
\medskip Option \verb|-v| enables verbose mode.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Examples%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Build a specific logic image:
\begin{ttbox}
isabelle build -b HOLCF
\end{ttbox}
Build the main group of logic images (as determined by the session
ROOT specifications of the Isabelle distribution):
\begin{ttbox}
isabelle build -b -g main
\end{ttbox}
Provide a general overview of the status of all Isabelle sessions,
without building anything:
\begin{ttbox}
isabelle build -a -n -v
\end{ttbox}
Build all sessions with HTML browser info and PDF document
preparation:
\begin{ttbox}
isabelle build -a -o browser_info -o document=pdf
\end{ttbox}
Build all sessions with a maximum of 8 prover processes and 4
threads each (on a machine with many cores):
\begin{ttbox}
isabelle build -a -j8 -o threads=4
\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: