--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/Thy/document/Sessions.tex Sat Jul 28 19:38:52 2012 +0200
@@ -0,0 +1,385 @@
+%
+\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.
+
+ Note that Isabelle/jEdit \secref{sec:tool-jedit} includes a simple
+ editing mode 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.
+
+ Note that 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: