1.1 --- a/doc-src/System/Thy/Sessions.thy Mon Jul 30 14:29:12 2012 +0200
1.2 +++ b/doc-src/System/Thy/Sessions.thy Mon Jul 30 14:38:45 2012 +0200
1.3 @@ -5,27 +5,27 @@
1.4 chapter {* Isabelle sessions and build management \label{ch:session} *}
1.5
1.6 text {* An Isabelle \emph{session} consists of a collection of related
1.7 - theories that are associated with an optional formal document (see
1.8 - also \chref{ch:present}). There is also a notion of persistent
1.9 - \emph{heap image} to capture the state of a session, similar to
1.10 - object-code in compiled programming languages.
1.11 + theories that may be associated with formal documents (see also
1.12 + \chref{ch:present}). There is also a notion of \emph{persistent
1.13 + heap} image to capture the state of a session, similar to
1.14 + object-code in compiled programming languages. Thus the concept of
1.15 + session resembles that of a ``project'' in common IDE environments,
1.16 + but the specific name emphasizes the connection to interactive
1.17 + theorem proving: the session wraps-up the results of
1.18 + user-interaction with the prover in a persistent form.
1.19
1.20 - Thus the concept of session resembles that of a ``project'' in
1.21 - common IDE environments, but our specific name emphasizes the
1.22 - connection to interactive theorem proving: the session wraps-up the
1.23 - results of user-interaction with the prover in a persistent form.
1.24 + Application sessions are built on a given parent session, which may
1.25 + be built recursively on other parents. Following this path in the
1.26 + hierarchy eventually leads to some major object-logic session like
1.27 + @{text "HOL"}, which itself is based on @{text "Pure"} as the common
1.28 + root of all sessions.
1.29
1.30 - \medskip Application sessions are built on a given parent session.
1.31 - The resulting hierarchy eventually leads to some major object-logic
1.32 - session, notably @{text "HOL"}, which itself is based on @{text
1.33 - "Pure"} as the common root.
1.34 + Processing sessions may take considerable time. Isabelle build
1.35 + management helps to organize this efficiently. This includes
1.36 + support for parallel build jobs, in addition to the multithreaded
1.37 + theory and proof checking that is already provided by the prover
1.38 + process itself. *}
1.39
1.40 - Processing sessions may take considerable time. The tools for
1.41 - Isabelle build management help to organize this efficiently,
1.42 - including support for parallel build jobs --- in addition to the
1.43 - multithreaded theory and proof checking that is already provided by
1.44 - the prover process.
1.45 -*}
1.46
1.47 section {* Session ROOT specifications \label{sec:session-root} *}
1.48
1.49 @@ -93,9 +93,9 @@
1.50 collection of groups where the new session is a member. Group names
1.51 are uninterpreted and merely follow certain conventions. For
1.52 example, the Isabelle distribution tags some important sessions by
1.53 - the group name @{text "main"}. Other projects may invent their own
1.54 - conventions, which requires some care to avoid clashes within this
1.55 - unchecked name space.
1.56 + the group name called ``@{text "main"}''. Other projects may invent
1.57 + their own conventions, but this requires some care to avoid clashes
1.58 + within this unchecked name space.
1.59
1.60 \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
1.61 specifies an explicit directory for this session. By default,
1.62 @@ -115,21 +115,21 @@
1.63 annotation for this session.
1.64
1.65 \item \isakeyword{options}~@{text "[x = a, y = b, z]"} defines
1.66 - separate options that are used when processing this session, but
1.67 - \emph{without} propagation to child sessions; see also
1.68 - \secref{sec:system-options}. Note that @{text "z"} abbreviates
1.69 - @{text "z = true"} for Boolean options.
1.70 + separate options (\secref{sec:system-options}) that are used when
1.71 + processing this session, but \emph{without} propagation to child
1.72 + sessions. Note that @{text "z"} abbreviates @{text "z = true"} for
1.73 + Boolean options.
1.74
1.75 \item \isakeyword{theories}~@{text "options names"} specifies a
1.76 block of theories that are processed within an environment that is
1.77 - augmented further by the given options, in addition to the global
1.78 - session options given before. Any number of blocks of
1.79 - \isakeyword{theories} may be given. Options are only active for
1.80 - each \isakeyword{theories} block separately.
1.81 + augmented by the given options, in addition to the global session
1.82 + options given before. Any number of blocks of \isakeyword{theories}
1.83 + may be given. Options are only active for each
1.84 + \isakeyword{theories} block separately.
1.85
1.86 \item \isakeyword{files}~@{text "files"} lists additional source
1.87 - files that are somehow involved in the processing of this session.
1.88 - This should cover anything outside the formal content of the theory
1.89 + files that are involved in the processing of this session. This
1.90 + should cover anything outside the formal content of the theory
1.91 sources, say some auxiliary {\TeX} files that are required for
1.92 document processing. In contrast, files that are specified in
1.93 formal theory headers as @{keyword "uses"} need not be declared
1.94 @@ -199,24 +199,24 @@
1.95 catalogs are only required for extra scalability and modularity
1.96 of large libraries.
1.97
1.98 - \medskip The subset of sessions to be managed is selected via
1.99 + \medskip The subset of sessions to be managed is determined via
1.100 individual @{text "SESSIONS"} given as command-line arguments, or
1.101 - session groups that are specified via one or more options @{verbatim
1.102 + session groups that are given via one or more options @{verbatim
1.103 "-g"}~@{text "NAME"}. Option @{verbatim "-a"} selects all sessions.
1.104 - The build tool takes the hierarchy of sessions into account: the
1.105 - selected set of sessions is completed by including all ancestors
1.106 - according to the dependency structure.
1.107 + The build tool takes session dependencies into account: the set of
1.108 + selected sessions is completed by including all ancestors.
1.109
1.110 - \medskip The build process depends on additional options that are
1.111 - passed to the prover session eventually, see also
1.112 - (\secref{sec:system-options}). The settings variable @{setting_ref
1.113 - ISABELLE_BUILD_OPTIONS} allows to provide additional defaults.
1.114 - Moreover, the environment of system build options may be augmented
1.115 - on the command line via @{verbatim "-o"}~@{text "NAME=VALUE"} or
1.116 - @{verbatim "-o"}~@{text "NAME"}, which abbreviates @{verbatim
1.117 - "-o"}~@{text "NAME=true"} for Boolean options. Multiple occurrences
1.118 - of @{verbatim "-o"} on the command-line are applied in the given
1.119 - order.
1.120 + \medskip The build process depends on additional options
1.121 + (\secref{sec:system-options}) that are passed to the prover
1.122 + eventually. The settings variable @{setting_ref
1.123 + ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\
1.124 + \texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,
1.125 + the environment of system build options may be augmented on the
1.126 + command line via @{verbatim "-o"}~@{text "name"}@{verbatim
1.127 + "="}@{text "value"} or @{verbatim "-o"}~@{text "name"}, which
1.128 + abbreviates @{verbatim "-o"}~@{text "name"}@{verbatim"=true"} for
1.129 + Boolean options. Multiple occurrences of @{verbatim "-o"} on the
1.130 + command-line are applied in the given order.
1.131
1.132 \medskip Option @{verbatim "-b"} ensures that heap images are
1.133 produced for all selected sessions. By default, images are only
1.134 @@ -232,9 +232,9 @@
1.135 sessions.
1.136
1.137 \medskip Option @{verbatim "-j"} specifies the maximum number of
1.138 - parallel build jobs (prover processes). Note that each process is
1.139 - subject to a separate limit of parallel threads, cf.\ system option
1.140 - @{system_option_ref threads}.
1.141 + parallel build jobs (prover processes). Each prover process is
1.142 + subject to a separate limit of parallel worker threads, cf.\ system
1.143 + option @{system_option_ref threads}.
1.144
1.145 \medskip Option @{verbatim "-s"} enables \emph{system mode}, which
1.146 means that resulting heap images and log files are stored in
1.147 @@ -253,8 +253,7 @@
1.148 isabelle build -b HOLCF
1.149 \end{ttbox}
1.150
1.151 - \smallskip Build the main group of logic images (as determined by
1.152 - the session ROOT specifications of the Isabelle distribution):
1.153 + \smallskip Build the main group of logic images:
1.154 \begin{ttbox}
1.155 isabelle build -b -g main
1.156 \end{ttbox}
1.157 @@ -271,8 +270,8 @@
1.158 isabelle build -a -o browser_info -o document=pdf
1.159 \end{ttbox}
1.160
1.161 - \smallskip Build all sessions with a maximum of 8 prover processes
1.162 - and 4 threads each (on a machine with many cores):
1.163 + \smallskip Build all sessions with a maximum of 8 parallel prover
1.164 + processes and 4 worker threads each (on a machine with many cores):
1.165 \begin{ttbox}
1.166 isabelle build -a -j8 -o threads=4
1.167 \end{ttbox}
2.1 --- a/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 14:29:12 2012 +0200
2.2 +++ b/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 14:38:45 2012 +0200
2.3 @@ -24,25 +24,26 @@
2.4 %
2.5 \begin{isamarkuptext}%
2.6 An Isabelle \emph{session} consists of a collection of related
2.7 - theories that are associated with an optional formal document (see
2.8 - also \chref{ch:present}). There is also a notion of persistent
2.9 - \emph{heap image} to capture the state of a session, similar to
2.10 - object-code in compiled programming languages.
2.11 + theories that may be associated with formal documents (see also
2.12 + \chref{ch:present}). There is also a notion of \emph{persistent
2.13 + heap} image to capture the state of a session, similar to
2.14 + object-code in compiled programming languages. Thus the concept of
2.15 + session resembles that of a ``project'' in common IDE environments,
2.16 + but the specific name emphasizes the connection to interactive
2.17 + theorem proving: the session wraps-up the results of
2.18 + user-interaction with the prover in a persistent form.
2.19
2.20 - Thus the concept of session resembles that of a ``project'' in
2.21 - common IDE environments, but our specific name emphasizes the
2.22 - connection to interactive theorem proving: the session wraps-up the
2.23 - results of user-interaction with the prover in a persistent form.
2.24 + Application sessions are built on a given parent session, which may
2.25 + be built recursively on other parents. Following this path in the
2.26 + hierarchy eventually leads to some major object-logic session like
2.27 + \isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{22}{\isachardoublequote}}}, which itself is based on \isa{{\isaliteral{22}{\isachardoublequote}}Pure{\isaliteral{22}{\isachardoublequote}}} as the common
2.28 + root of all sessions.
2.29
2.30 - \medskip Application sessions are built on a given parent session.
2.31 - The resulting hierarchy eventually leads to some major object-logic
2.32 - 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.
2.33 -
2.34 - Processing sessions may take considerable time. The tools for
2.35 - Isabelle build management help to organize this efficiently,
2.36 - including support for parallel build jobs --- in addition to the
2.37 - multithreaded theory and proof checking that is already provided by
2.38 - the prover process.%
2.39 + Processing sessions may take considerable time. Isabelle build
2.40 + management helps to organize this efficiently. This includes
2.41 + support for parallel build jobs, in addition to the multithreaded
2.42 + theory and proof checking that is already provided by the prover
2.43 + process itself.%
2.44 \end{isamarkuptext}%
2.45 \isamarkuptrue%
2.46 %
2.47 @@ -193,9 +194,9 @@
2.48 collection of groups where the new session is a member. Group names
2.49 are uninterpreted and merely follow certain conventions. For
2.50 example, the Isabelle distribution tags some important sessions by
2.51 - the group name \isa{{\isaliteral{22}{\isachardoublequote}}main{\isaliteral{22}{\isachardoublequote}}}. Other projects may invent their own
2.52 - conventions, which requires some care to avoid clashes within this
2.53 - unchecked name space.
2.54 + the group name called ``\isa{{\isaliteral{22}{\isachardoublequote}}main{\isaliteral{22}{\isachardoublequote}}}''. Other projects may invent
2.55 + their own conventions, but this requires some care to avoid clashes
2.56 + within this unchecked name space.
2.57
2.58 \item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}dir{\isaliteral{22}{\isachardoublequote}}}
2.59 specifies an explicit directory for this session. By default,
2.60 @@ -214,21 +215,21 @@
2.61 annotation for this session.
2.62
2.63 \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
2.64 - separate options that are used when processing this session, but
2.65 - \emph{without} propagation to child sessions; see also
2.66 - \secref{sec:system-options}. Note that \isa{{\isaliteral{22}{\isachardoublequote}}z{\isaliteral{22}{\isachardoublequote}}} abbreviates
2.67 - \isa{{\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{22}{\isachardoublequote}}} for Boolean options.
2.68 + separate options (\secref{sec:system-options}) that are used when
2.69 + processing this session, but \emph{without} propagation to child
2.70 + 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
2.71 + Boolean options.
2.72
2.73 \item \isakeyword{theories}~\isa{{\isaliteral{22}{\isachardoublequote}}options\ names{\isaliteral{22}{\isachardoublequote}}} specifies a
2.74 block of theories that are processed within an environment that is
2.75 - augmented further by the given options, in addition to the global
2.76 - session options given before. Any number of blocks of
2.77 - \isakeyword{theories} may be given. Options are only active for
2.78 - each \isakeyword{theories} block separately.
2.79 + augmented by the given options, in addition to the global session
2.80 + options given before. Any number of blocks of \isakeyword{theories}
2.81 + may be given. Options are only active for each
2.82 + \isakeyword{theories} block separately.
2.83
2.84 \item \isakeyword{files}~\isa{{\isaliteral{22}{\isachardoublequote}}files{\isaliteral{22}{\isachardoublequote}}} lists additional source
2.85 - files that are somehow involved in the processing of this session.
2.86 - This should cover anything outside the formal content of the theory
2.87 + files that are involved in the processing of this session. This
2.88 + should cover anything outside the formal content of the theory
2.89 sources, say some auxiliary {\TeX} files that are required for
2.90 document processing. In contrast, files that are specified in
2.91 formal theory headers as \hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} need not be declared
2.92 @@ -308,21 +309,21 @@
2.93 catalogs are only required for extra scalability and modularity
2.94 of large libraries.
2.95
2.96 - \medskip The subset of sessions to be managed is selected via
2.97 + \medskip The subset of sessions to be managed is determined via
2.98 individual \isa{{\isaliteral{22}{\isachardoublequote}}SESSIONS{\isaliteral{22}{\isachardoublequote}}} given as command-line arguments, or
2.99 - 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.
2.100 - The build tool takes the hierarchy of sessions into account: the
2.101 - selected set of sessions is completed by including all ancestors
2.102 - according to the dependency structure.
2.103 + 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.
2.104 + The build tool takes session dependencies into account: the set of
2.105 + selected sessions is completed by including all ancestors.
2.106
2.107 - \medskip The build process depends on additional options that are
2.108 - passed to the prover session eventually, see also
2.109 - (\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.
2.110 - Moreover, the environment of system build options may be augmented
2.111 - on the command line via \verb|-o|~\isa{{\isaliteral{22}{\isachardoublequote}}NAME{\isaliteral{3D}{\isacharequal}}VALUE{\isaliteral{22}{\isachardoublequote}}} or
2.112 - \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
2.113 - of \verb|-o| on the command-line are applied in the given
2.114 - order.
2.115 + \medskip The build process depends on additional options
2.116 + (\secref{sec:system-options}) that are passed to the prover
2.117 + 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.\
2.118 + \texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,
2.119 + the environment of system build options may be augmented on the
2.120 + 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
2.121 + abbreviates \verb|-o|~\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{22}{\isachardoublequote}}}\verb|=true| for
2.122 + Boolean options. Multiple occurrences of \verb|-o| on the
2.123 + command-line are applied in the given order.
2.124
2.125 \medskip Option \verb|-b| ensures that heap images are
2.126 produced for all selected sessions. By default, images are only
2.127 @@ -338,9 +339,9 @@
2.128 sessions.
2.129
2.130 \medskip Option \verb|-j| specifies the maximum number of
2.131 - parallel build jobs (prover processes). Note that each process is
2.132 - subject to a separate limit of parallel threads, cf.\ system option
2.133 - \indexref{}{system option}{threads}\hyperlink{system option.threads}{\mbox{\isa{\isatt{threads}}}}.
2.134 + parallel build jobs (prover processes). Each prover process is
2.135 + subject to a separate limit of parallel worker threads, cf.\ system
2.136 + option \indexref{}{system option}{threads}\hyperlink{system option.threads}{\mbox{\isa{\isatt{threads}}}}.
2.137
2.138 \medskip Option \verb|-s| enables \emph{system mode}, which
2.139 means that resulting heap images and log files are stored in
2.140 @@ -361,8 +362,7 @@
2.141 isabelle build -b HOLCF
2.142 \end{ttbox}
2.143
2.144 - \smallskip Build the main group of logic images (as determined by
2.145 - the session ROOT specifications of the Isabelle distribution):
2.146 + \smallskip Build the main group of logic images:
2.147 \begin{ttbox}
2.148 isabelle build -b -g main
2.149 \end{ttbox}
2.150 @@ -379,8 +379,8 @@
2.151 isabelle build -a -o browser_info -o document=pdf
2.152 \end{ttbox}
2.153
2.154 - \smallskip Build all sessions with a maximum of 8 prover processes
2.155 - and 4 threads each (on a machine with many cores):
2.156 + \smallskip Build all sessions with a maximum of 8 parallel prover
2.157 + processes and 4 worker threads each (on a machine with many cores):
2.158 \begin{ttbox}
2.159 isabelle build -a -j8 -o threads=4
2.160 \end{ttbox}