--- a/doc-src/System/Thy/Sessions.thy Mon Jul 30 14:29:12 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy Mon Jul 30 14:38:45 2012 +0200
@@ -5,27 +5,27 @@
chapter {* Isabelle sessions and build management \label{ch:session} *}
text {* An Isabelle \emph{session} consists of a collection of related
- theories that are associated with an optional formal document (see
- also \chref{ch:present}). There is also a notion of persistent
- \emph{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 our 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.
+ 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.
- \medskip Application sessions are built on a given parent session.
- The resulting hierarchy eventually leads to some major object-logic
- session, notably @{text "HOL"}, which itself is based on @{text
- "Pure"} as the common root.
+ 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
+ @{text "HOL"}, which itself is based on @{text "Pure"} as the common
+ root of all sessions.
- Processing sessions may take considerable time. The tools for
- Isabelle build management help to organize this efficiently,
- including support for parallel build jobs --- in addition to the
- multithreaded theory and proof checking that is already provided by
- the prover process.
-*}
+ 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. *}
+
section {* Session ROOT specifications \label{sec:session-root} *}
@@ -93,9 +93,9 @@
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 @{text "main"}. Other projects may invent their own
- conventions, which requires some care to avoid clashes within this
- unchecked name space.
+ the group name called ``@{text "main"}''. Other projects may invent
+ their own conventions, but this requires some care to avoid clashes
+ within this unchecked name space.
\item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
specifies an explicit directory for this session. By default,
@@ -115,21 +115,21 @@
annotation for this session.
\item \isakeyword{options}~@{text "[x = a, y = b, z]"} 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 @{text "z"} abbreviates
- @{text "z = true"} for Boolean options.
+ separate options (\secref{sec:system-options}) that are used when
+ processing this session, but \emph{without} propagation to child
+ sessions. Note that @{text "z"} abbreviates @{text "z = true"} for
+ Boolean options.
\item \isakeyword{theories}~@{text "options names"} 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.
+ 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}~@{text "files"} 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
+ 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 @{keyword "uses"} need not be declared
@@ -199,24 +199,24 @@
catalogs are only required for extra scalability and modularity
of large libraries.
- \medskip The subset of sessions to be managed is selected via
+ \medskip The subset of sessions to be managed is determined via
individual @{text "SESSIONS"} given as command-line arguments, or
- session groups that are specified via one or more options @{verbatim
+ session groups that are given via one or more options @{verbatim
"-g"}~@{text "NAME"}. Option @{verbatim "-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.
+ 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 that are
- passed to the prover session eventually, see also
- (\secref{sec:system-options}). The settings variable @{setting_ref
- ISABELLE_BUILD_OPTIONS} allows to provide additional defaults.
- Moreover, the environment of system build options may be augmented
- on the command line via @{verbatim "-o"}~@{text "NAME=VALUE"} or
- @{verbatim "-o"}~@{text "NAME"}, which abbreviates @{verbatim
- "-o"}~@{text "NAME=true"} for Boolean options. Multiple occurrences
- of @{verbatim "-o"} on the command-line are applied in the given
- order.
+ \medskip The build process depends on additional options
+ (\secref{sec:system-options}) that are passed to the prover
+ eventually. The settings variable @{setting_ref
+ ISABELLE_BUILD_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 @{verbatim "-o"}~@{text "name"}@{verbatim
+ "="}@{text "value"} or @{verbatim "-o"}~@{text "name"}, which
+ abbreviates @{verbatim "-o"}~@{text "name"}@{verbatim"=true"} for
+ Boolean options. Multiple occurrences of @{verbatim "-o"} on the
+ command-line are applied in the given order.
\medskip Option @{verbatim "-b"} ensures that heap images are
produced for all selected sessions. By default, images are only
@@ -232,9 +232,9 @@
sessions.
\medskip Option @{verbatim "-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
- @{system_option_ref threads}.
+ parallel build jobs (prover processes). Each prover process is
+ subject to a separate limit of parallel worker threads, cf.\ system
+ option @{system_option_ref threads}.
\medskip Option @{verbatim "-s"} enables \emph{system mode}, which
means that resulting heap images and log files are stored in
@@ -253,8 +253,7 @@
isabelle build -b HOLCF
\end{ttbox}
- \smallskip Build the main group of logic images (as determined by
- the session ROOT specifications of the Isabelle distribution):
+ \smallskip Build the main group of logic images:
\begin{ttbox}
isabelle build -b -g main
\end{ttbox}
@@ -271,8 +270,8 @@
isabelle build -a -o browser_info -o document=pdf
\end{ttbox}
- \smallskip Build all sessions with a maximum of 8 prover processes
- and 4 threads each (on a machine with many cores):
+ \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}
--- a/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 14:29:12 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 14:38:45 2012 +0200
@@ -24,25 +24,26 @@
%
\begin{isamarkuptext}%
An Isabelle \emph{session} consists of a collection of related
- theories that are associated with an optional formal document (see
- also \chref{ch:present}). There is also a notion of persistent
- \emph{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 our 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.
+ 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.
- \medskip Application sessions are built on a given parent session.
- The resulting hierarchy eventually leads to some major object-logic
- session, notably \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.
+ 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. The tools for
- Isabelle build management help to organize this efficiently,
- including support for parallel build jobs --- in addition to the
- multithreaded theory and proof checking that is already provided by
- the prover process.%
+ 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%
%
@@ -193,9 +194,9 @@
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.
+ 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,
@@ -214,21 +215,21 @@
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.
+ 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 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.
+ 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 somehow involved in the processing of this session.
- This should cover anything outside the formal content of the theory
+ 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
@@ -308,21 +309,21 @@
catalogs are only required for extra scalability and modularity
of large libraries.
- \medskip The subset of sessions to be managed is selected via
+ \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 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.
+ 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 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 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
@@ -338,9 +339,9 @@
sessions.
\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}}}}.
+ 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
@@ -361,8 +362,7 @@
isabelle build -b HOLCF
\end{ttbox}
- \smallskip Build the main group of logic images (as determined by
- the session ROOT specifications of the Isabelle distribution):
+ \smallskip Build the main group of logic images:
\begin{ttbox}
isabelle build -b -g main
\end{ttbox}
@@ -379,8 +379,8 @@
isabelle build -a -o browser_info -o document=pdf
\end{ttbox}
- \smallskip Build all sessions with a maximum of 8 prover processes
- and 4 threads each (on a machine with many cores):
+ \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}