1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/System/Thy/document/Sessions.tex Sat Jul 28 19:38:52 2012 +0200
1.3 @@ -0,0 +1,385 @@
1.4 +%
1.5 +\begin{isabellebody}%
1.6 +\def\isabellecontext{Sessions}%
1.7 +%
1.8 +\isadelimtheory
1.9 +%
1.10 +\endisadelimtheory
1.11 +%
1.12 +\isatagtheory
1.13 +\isacommand{theory}\isamarkupfalse%
1.14 +\ Sessions\isanewline
1.15 +\isakeyword{imports}\ Base\isanewline
1.16 +\isakeyword{begin}%
1.17 +\endisatagtheory
1.18 +{\isafoldtheory}%
1.19 +%
1.20 +\isadelimtheory
1.21 +%
1.22 +\endisadelimtheory
1.23 +%
1.24 +\isamarkupchapter{Isabelle sessions and build management%
1.25 +}
1.26 +\isamarkuptrue%
1.27 +%
1.28 +\begin{isamarkuptext}%
1.29 +FIXME%
1.30 +\end{isamarkuptext}%
1.31 +\isamarkuptrue%
1.32 +%
1.33 +\isamarkupsection{Session ROOT specifications \label{sec:session-root}%
1.34 +}
1.35 +\isamarkuptrue%
1.36 +%
1.37 +\begin{isamarkuptext}%
1.38 +Session specifications reside in files called \verb|ROOT|
1.39 + within certain directories, such as the home locations of registered
1.40 + Isabelle components or additional project directories given by the
1.41 + user.
1.42 +
1.43 + The ROOT file format follows the lexical conventions of the
1.44 + \emph{outer syntax} of Isabelle/Isar, see also
1.45 + \cite{isabelle-isar-ref}. This defines common forms like
1.46 + identifiers, names, quoted strings, verbatim text, nested comments
1.47 + etc. The grammar for a single \hyperlink{syntax.session-entry}{\mbox{\isa{session{\isaliteral{5F}{\isacharunderscore}}entry}}} is given as
1.48 + syntax diagram below; each ROOT file may contain multiple session
1.49 + specifications like this.
1.50 +
1.51 + Note that Isabelle/jEdit \secref{sec:tool-jedit} includes a simple
1.52 + editing mode for session ROOT files.
1.53 +
1.54 + \begin{railoutput}
1.55 +\rail@begin{2}{\indexdef{}{syntax}{session\_entry}\hypertarget{syntax.session-entry}{\hyperlink{syntax.session-entry}{\mbox{\isa{session{\isaliteral{5F}{\isacharunderscore}}entry}}}}}
1.56 +\rail@term{\isa{\isakeyword{session}}}[]
1.57 +\rail@nont{\isa{spec}}[]
1.58 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.59 +\rail@bar
1.60 +\rail@nextbar{1}
1.61 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.62 +\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
1.63 +\rail@endbar
1.64 +\rail@nont{\isa{body}}[]
1.65 +\rail@end
1.66 +\rail@begin{2}{\isa{body}}
1.67 +\rail@bar
1.68 +\rail@nextbar{1}
1.69 +\rail@nont{\isa{description}}[]
1.70 +\rail@endbar
1.71 +\rail@bar
1.72 +\rail@nextbar{1}
1.73 +\rail@nont{\isa{options}}[]
1.74 +\rail@endbar
1.75 +\rail@plus
1.76 +\rail@nextplus{1}
1.77 +\rail@cnont{\isa{theories}}[]
1.78 +\rail@endplus
1.79 +\rail@bar
1.80 +\rail@nextbar{1}
1.81 +\rail@nont{\isa{files}}[]
1.82 +\rail@endbar
1.83 +\rail@end
1.84 +\rail@begin{2}{\isa{spec}}
1.85 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.86 +\rail@bar
1.87 +\rail@nextbar{1}
1.88 +\rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
1.89 +\rail@endbar
1.90 +\rail@bar
1.91 +\rail@nextbar{1}
1.92 +\rail@nont{\isa{groups}}[]
1.93 +\rail@endbar
1.94 +\rail@bar
1.95 +\rail@nextbar{1}
1.96 +\rail@nont{\isa{dir}}[]
1.97 +\rail@endbar
1.98 +\rail@end
1.99 +\rail@begin{2}{\isa{groups}}
1.100 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.101 +\rail@plus
1.102 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.103 +\rail@nextplus{1}
1.104 +\rail@endplus
1.105 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.106 +\rail@end
1.107 +\rail@begin{1}{\isa{dir}}
1.108 +\rail@term{\isa{\isakeyword{in}}}[]
1.109 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.110 +\rail@end
1.111 +\rail@begin{1}{\isa{description}}
1.112 +\rail@term{\isa{\isakeyword{description}}}[]
1.113 +\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
1.114 +\rail@end
1.115 +\rail@begin{1}{\isa{options}}
1.116 +\rail@term{\isa{\isakeyword{options}}}[]
1.117 +\rail@nont{\isa{opts}}[]
1.118 +\rail@end
1.119 +\rail@begin{3}{\isa{opts}}
1.120 +\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
1.121 +\rail@plus
1.122 +\rail@bar
1.123 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.124 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.125 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.126 +\rail@nextbar{1}
1.127 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.128 +\rail@endbar
1.129 +\rail@nextplus{2}
1.130 +\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
1.131 +\rail@endplus
1.132 +\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
1.133 +\rail@end
1.134 +\rail@begin{2}{\isa{theories}}
1.135 +\rail@term{\isa{\isakeyword{theories}}}[]
1.136 +\rail@bar
1.137 +\rail@nextbar{1}
1.138 +\rail@nont{\isa{opts}}[]
1.139 +\rail@endbar
1.140 +\rail@plus
1.141 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.142 +\rail@nextplus{1}
1.143 +\rail@endplus
1.144 +\rail@end
1.145 +\rail@begin{2}{\isa{files}}
1.146 +\rail@term{\isa{\isakeyword{files}}}[]
1.147 +\rail@plus
1.148 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.149 +\rail@nextplus{1}
1.150 +\rail@endplus
1.151 +\rail@end
1.152 +\end{railoutput}
1.153 +
1.154 +
1.155 + \begin{description}
1.156 +
1.157 + \item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3D}{\isacharequal}}\ B\ {\isaliteral{2B}{\isacharplus}}\ body{\isaliteral{22}{\isachardoublequote}}} defines a new
1.158 + session \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} based on parent session \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{22}{\isachardoublequote}}}, with its
1.159 + content given in \isa{body} (theories and auxiliary source files).
1.160 + Note that a parent (like \isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{22}{\isachardoublequote}}}) is mandatory in practical
1.161 + applications: only Isabelle/Pure can bootstrap itself from nothing.
1.162 +
1.163 + All such session specifications together describe a hierarchy (tree)
1.164 + of sessions, with globally unique names. By default, names are
1.165 + derived from parent ones by concatenation, i.e.\ \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{5C3C646173683E}{\isasymdash}}A{\isaliteral{22}{\isachardoublequote}}}
1.166 + 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,
1.167 + \isa{B} is already such a fully-qualified name, while \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}
1.168 + is the new base name.
1.169 +
1.170 + \item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{21}{\isacharbang}}\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{22}{\isachardoublequote}}} indicates a fresh start
1.171 + in the naming scheme: the session is called just \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} instead
1.172 + 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
1.173 + sufficiently long to stand on its own in a potentially large
1.174 + library.
1.175 +
1.176 + \item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{28}{\isacharparenleft}}groups{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} indicates a
1.177 + collection of groups where the new session is a member. Group names
1.178 + are uninterpreted and merely follow certain conventions. For
1.179 + example, the Isabelle distribution tags some important sessions by
1.180 + the group name \isa{{\isaliteral{22}{\isachardoublequote}}main{\isaliteral{22}{\isachardoublequote}}}. Other projects may invent their own
1.181 + conventions, which requires some care to avoid clashes within this
1.182 + unchecked name space.
1.183 +
1.184 + \item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}dir{\isaliteral{22}{\isachardoublequote}}}
1.185 + specifies an explicit directory for this session. By default,
1.186 + \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} abbreviates
1.187 + \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}. This
1.188 + accommodates the common scheme where some base directory contains
1.189 + several sessions in sub-directories of corresponding names. Another
1.190 + common scheme is \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\verb|"."| to refer to the current
1.191 + directory of the ROOT file.
1.192 +
1.193 + All theories and auxiliary source files are located relatively to
1.194 + the session directory. The prover process is run within the same as
1.195 + its current working directory.
1.196 +
1.197 + \item \isakeyword{description}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} is a free-form
1.198 + annotation for this session.
1.199 +
1.200 + \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
1.201 + separate options that are used when processing this session, but
1.202 + \emph{without} propagation to child sessions; see also
1.203 + \secref{sec:system-options}. Note that \isa{{\isaliteral{22}{\isachardoublequote}}z{\isaliteral{22}{\isachardoublequote}}} abbreviates
1.204 + \isa{{\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{22}{\isachardoublequote}}} for Boolean options.
1.205 +
1.206 + \item \isakeyword{theories}~\isa{{\isaliteral{22}{\isachardoublequote}}options\ names{\isaliteral{22}{\isachardoublequote}}} specifies a
1.207 + block of theories that are processed within an environment that is
1.208 + augmented further by the given options, in addition to the global
1.209 + session options given before. Any number of blocks of
1.210 + \isakeyword{theories} may be given. Options are only active for
1.211 + each \isakeyword{theories} block separately.
1.212 +
1.213 + \item \isakeyword{files}~\isa{{\isaliteral{22}{\isachardoublequote}}files{\isaliteral{22}{\isachardoublequote}}} lists additional source
1.214 + files that are somehow involved in the processing of this session.
1.215 + This should cover anything outside the formal content of the theory
1.216 + sources, say some auxiliary {\TeX} files that are required for
1.217 + document processing. In contrast, files that are specified in
1.218 + formal theory headers as \hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} need not be declared
1.219 + again.
1.220 +
1.221 + \end{description}%
1.222 +\end{isamarkuptext}%
1.223 +\isamarkuptrue%
1.224 +%
1.225 +\isamarkupsubsubsection{Examples%
1.226 +}
1.227 +\isamarkuptrue%
1.228 +%
1.229 +\begin{isamarkuptext}%
1.230 +See \verb|~~/src/HOL/ROOT| for a diversity of practically
1.231 + relevant situations.%
1.232 +\end{isamarkuptext}%
1.233 +\isamarkuptrue%
1.234 +%
1.235 +\isamarkupsection{System build options \label{sec:system-options}%
1.236 +}
1.237 +\isamarkuptrue%
1.238 +%
1.239 +\begin{isamarkuptext}%
1.240 +See \verb|~~/etc/options| for the main defaults provided by
1.241 + the Isabelle distribution.
1.242 +
1.243 + Note that Isabelle/jEdit \secref{sec:tool-jedit} includes a simple
1.244 + editing mode \verb|isabelle-options| for this file-format.%
1.245 +\end{isamarkuptext}%
1.246 +\isamarkuptrue%
1.247 +%
1.248 +\isamarkupsection{Invoking the build process \label{sec:tool-build}%
1.249 +}
1.250 +\isamarkuptrue%
1.251 +%
1.252 +\begin{isamarkuptext}%
1.253 +The \indexdef{}{tool}{build}\hypertarget{tool.build}{\hyperlink{tool.build}{\mbox{\isa{\isatt{build}}}}} utility invokes the build process for
1.254 + Isabelle sessions. It manages dependencies between sessions,
1.255 + related sources of theories and auxiliary files, and target heap
1.256 + images. Accordingly, it runs instances of the prover process with
1.257 + optional document preparation. Its command-line usage
1.258 + is:\footnote{Isabelle/Scala provides the same functionality via
1.259 + \texttt{isabelle.Build.build}.}
1.260 +\begin{ttbox} Usage: isabelle build [OPTIONS] [SESSIONS ...]
1.261 +
1.262 + Options are:
1.263 + -a select all sessions
1.264 + -b build heap images
1.265 + -d DIR include session directory with ROOT file
1.266 + -g NAME select session group NAME
1.267 + -j INT maximum number of parallel jobs (default 1)
1.268 + -n no build -- test dependencies only
1.269 + -o OPTION override session configuration OPTION
1.270 + (via NAME=VAL or NAME)
1.271 + -s system build mode: produce output in ISABELLE_HOME
1.272 + -v verbose
1.273 +
1.274 + Build and manage Isabelle sessions, depending on implicit
1.275 + ISABELLE_BUILD_OPTIONS="..."
1.276 +
1.277 + ML_PLATFORM="..."
1.278 + ML_HOME="..."
1.279 + ML_SYSTEM="..."
1.280 + ML_OPTIONS="..."
1.281 +\end{ttbox}
1.282 +
1.283 + \medskip Isabelle sessions are defined via session ROOT files as
1.284 + described in (\secref{sec:session-root}). The totality of sessions
1.285 + is determined by collecting such specifications from all Isabelle
1.286 + component directories (\secref{sec:components}), augmented by more
1.287 + directories given via options \verb|-d|~\isa{{\isaliteral{22}{\isachardoublequote}}DIR{\isaliteral{22}{\isachardoublequote}}} on the
1.288 + command line. Each such directory may contain a session
1.289 + \texttt{ROOT} file and an additional catalog file \verb|etc/sessions| with further sub-directories (list of lines). Note
1.290 + that a single \texttt{ROOT} file usually defines many sessions;
1.291 + catalogs are are only required for extra scalability and modularity
1.292 + of large libraries.
1.293 +
1.294 + \medskip The subset of sessions to be managed is selected via
1.295 + individual \isa{{\isaliteral{22}{\isachardoublequote}}SESSIONS{\isaliteral{22}{\isachardoublequote}}} given as command-line arguments, or
1.296 + 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.
1.297 + The build tool takes the hierarchy of sessions into account: the
1.298 + selected set of sessions is completed by including all ancestors
1.299 + according to the dependency structure.
1.300 +
1.301 + \medskip The build process depends on additional options that are
1.302 + passed to the prover session eventually, see also
1.303 + (\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.
1.304 + Moreover, the environment of system build options may be augmented
1.305 + on the command line via \verb|-o|~\isa{{\isaliteral{22}{\isachardoublequote}}NAME{\isaliteral{3D}{\isacharequal}}VALUE{\isaliteral{22}{\isachardoublequote}}} or
1.306 + \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
1.307 + of \verb|-o| on the command-line are applied in the given
1.308 + order.
1.309 +
1.310 + \medskip Option \verb|-b| ensures that heap images are
1.311 + produced for all selected sessions. By default, images are only
1.312 + saved for inner nodes of the hierarchy of sessions, as required for
1.313 + other sessions to continue later on.
1.314 +
1.315 + \medskip Option \verb|-j| specifies the maximum number of
1.316 + parallel build jobs (prover processes). Note that each process is
1.317 + subject to a separate limit of parallel threads, cf.\ system option
1.318 + \indexref{}{system option}{threads}\hyperlink{system option.threads}{\mbox{\isa{\isatt{threads}}}}.
1.319 +
1.320 + \medskip Option \verb|-s| enables \emph{system mode}, which
1.321 + means that resulting heap images and log files are stored in
1.322 + \verb|$ISABELLE_HOME/heaps| instead of the default location
1.323 + \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).
1.324 +
1.325 + \medskip Option \verb|-n| omits the actual build process
1.326 + after performing all dependency checks. The return code indicates
1.327 + the status of the set of selected sessions.
1.328 +
1.329 + \medskip Option \verb|-v| enables verbose mode.%
1.330 +\end{isamarkuptext}%
1.331 +\isamarkuptrue%
1.332 +%
1.333 +\isamarkupsubsubsection{Examples%
1.334 +}
1.335 +\isamarkuptrue%
1.336 +%
1.337 +\begin{isamarkuptext}%
1.338 +Build a specific logic image:
1.339 +\begin{ttbox}
1.340 +isabelle build -b HOLCF
1.341 +\end{ttbox}
1.342 +
1.343 + Build the main group of logic images (as determined by the session
1.344 + ROOT specifications of the Isabelle distribution):
1.345 +\begin{ttbox}
1.346 +isabelle build -b -g main
1.347 +\end{ttbox}
1.348 +
1.349 + Provide a general overview of the status of all Isabelle sessions,
1.350 + without building anything:
1.351 +\begin{ttbox}
1.352 +isabelle build -a -n -v
1.353 +\end{ttbox}
1.354 +
1.355 + Build all sessions with HTML browser info and PDF document
1.356 + preparation:
1.357 +\begin{ttbox}
1.358 +isabelle build -a -o browser_info -o document=pdf
1.359 +\end{ttbox}
1.360 +
1.361 + Build all sessions with a maximum of 8 prover processes and 4
1.362 + threads each (on a machine with many cores):
1.363 +
1.364 +\begin{ttbox}
1.365 +isabelle build -a -j8 -o threads=4
1.366 +\end{ttbox}%
1.367 +\end{isamarkuptext}%
1.368 +\isamarkuptrue%
1.369 +%
1.370 +\isadelimtheory
1.371 +%
1.372 +\endisadelimtheory
1.373 +%
1.374 +\isatagtheory
1.375 +\isacommand{end}\isamarkupfalse%
1.376 +%
1.377 +\endisatagtheory
1.378 +{\isafoldtheory}%
1.379 +%
1.380 +\isadelimtheory
1.381 +%
1.382 +\endisadelimtheory
1.383 +\isanewline
1.384 +\end{isabellebody}%
1.385 +%%% Local Variables:
1.386 +%%% mode: latex
1.387 +%%% TeX-master: "root"
1.388 +%%% End: