author wenzelm Mon, 30 Jul 2012 14:38:45 +0200 changeset 48604 f651323139f0 parent 48603 a37463482e5f child 48605 e777363440d6
misc tuning;
--- 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}