%
\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 \label{ch:session}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
An Isabelle \emph{session} consists of a collection of related
theories that may be associated with formal documents (see also
\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
\isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{22}{\isachardoublequote}}}, which itself is based on \isa{{\isaliteral{22}{\isachardoublequote}}Pure{\isaliteral{22}{\isachardoublequote}}} 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.%
\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{\isa{value}}[]
\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{value}}
\rail@bar
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.real}{\mbox{\isa{real}}}}[]
\rail@endbar
\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 called ``\isa{{\isaliteral{22}{\isachardoublequote}}main{\isaliteral{22}{\isachardoublequote}}}''. Other projects may invent
their own conventions, but this 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 (\secref{sec:system-options}) that are used when
processing this session, but \emph{without} propagation to child
sessions. 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 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 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{\isatool{build}}}}} tool 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
-c clean build
-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 with several session specifications.
\medskip The subset of sessions to be managed is determined via
individual \isa{{\isaliteral{22}{\isachardoublequote}}SESSIONS{\isaliteral{22}{\isachardoublequote}}} given as command-line arguments, or
session groups that are given 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 session dependencies into account: the set of
selected sessions is completed by including all ancestors.
\medskip The build process depends on additional options
(\secref{sec:system-options}) that are passed to the prover
eventually. 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, e.g.\
\texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,
the environment of system build options may be augmented on the
command line via \verb|-o|~\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{22}{\isachardoublequote}}}\verb|=|\isa{{\isaliteral{22}{\isachardoublequote}}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{22}{\isachardoublequote}}}\verb|=true| 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|-c| cleans all descendants of the
selected sessions before performing the specified build operation.
\medskip Option \verb|-n| omits the actual build process
after the preparatory stage (including optional cleanup). Note that
the return code always indicates the status of the set of selected
sessions.
\medskip Option \verb|-j| specifies the maximum number of
parallel build jobs (prover processes). Each prover process is
subject to a separate limit of parallel worker 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|-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}
\smallskip Build the main group of logic images:
\begin{ttbox}
isabelle build -b -g main
\end{ttbox}
\smallskip Provide a general overview of the status of all Isabelle
sessions, without building anything:
\begin{ttbox}
isabelle build -a -n -v
\end{ttbox}
\smallskip Build all sessions with HTML browser info and PDF
document preparation:
\begin{ttbox}
isabelle build -a -o browser_info -o document=pdf
\end{ttbox}
\smallskip Build all sessions with a maximum of 8 parallel prover
processes and 4 worker threads each (on a machine with many cores):
\begin{ttbox}
isabelle build -a -j8 -o threads=4
\end{ttbox}
\smallskip Build some session images with cleanup of their
descendants, while retaining their ancestry:
\begin{ttbox}
isabelle build -b -c HOL-Boogie HOL-SPARK
\end{ttbox}
\smallskip Clean all sessions without building anything:
\begin{ttbox}
isabelle build -a -n -c
\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Preparing session root directories \label{sec:tool-mkroot}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The \indexdef{}{tool}{mkroot}\hypertarget{tool.mkroot}{\hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}}} tool prepares Isabelle session source
directories, including some \verb|ROOT| entry, an example
theory file, and some initial configuration for document preparation
(see also \chref{ch:present}). The usage of \hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} is:
\begin{ttbox}
Usage: isabelle mkroot NAME
Prepare session root directory, adding session NAME with
built-in document preparation.
\end{ttbox}
All session-specific files are placed into a separate sub-directory
given as \verb|NAME| above. The \verb|ROOT| file is in
the parent position relative to that --- it could refer to several
such sessions. The \hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} tool is conservative in the sense
that does not overwrite an existing session sub-directory; an
already existing \verb|ROOT| file is extended.
The implicit Isabelle settings variable \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LOGIC}}}}
specifies the parent session, and \hyperlink{setting.ISABELLE-DOCUMENT-FORMAT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DOCUMENT{\isaliteral{5F}{\isacharunderscore}}FORMAT}}}} the document format to be filled filled
into the generated \verb|ROOT| file.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Examples%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The following produces an example session, relatively to the
\verb|ROOT| in the current directory:
\begin{ttbox}
isabelle mkroot Test && isabelle build -v -d. Test
\end{ttbox}
Option \verb|-v| is not required, but useful to reveal the
the location of generated documents.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: