# HG changeset patch # User wenzelm # Date 1343497132 -7200 # Node ID 240d6a6771938ffef92b5eebff01cdd98ec236f0 # Parent 9df76dd459009439feae93364def375d7756f74a added generated file; diff -r 9df76dd45900 -r 240d6a677193 doc-src/System/Thy/document/Sessions.tex --- /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: