48578
|
1 |
theory Sessions
|
|
2 |
imports Base
|
|
3 |
begin
|
|
4 |
|
48584
|
5 |
chapter {* Isabelle sessions and build management \label{ch:session} *}
|
|
6 |
|
|
7 |
text {* An Isabelle \emph{session} consists of a collection of related
|
48604
|
8 |
theories that may be associated with formal documents (see also
|
|
9 |
\chref{ch:present}). There is also a notion of \emph{persistent
|
|
10 |
heap} image to capture the state of a session, similar to
|
|
11 |
object-code in compiled programming languages. Thus the concept of
|
|
12 |
session resembles that of a ``project'' in common IDE environments,
|
|
13 |
but the specific name emphasizes the connection to interactive
|
|
14 |
theorem proving: the session wraps-up the results of
|
|
15 |
user-interaction with the prover in a persistent form.
|
48584
|
16 |
|
48604
|
17 |
Application sessions are built on a given parent session, which may
|
|
18 |
be built recursively on other parents. Following this path in the
|
|
19 |
hierarchy eventually leads to some major object-logic session like
|
|
20 |
@{text "HOL"}, which itself is based on @{text "Pure"} as the common
|
|
21 |
root of all sessions.
|
48584
|
22 |
|
48604
|
23 |
Processing sessions may take considerable time. Isabelle build
|
|
24 |
management helps to organize this efficiently. This includes
|
|
25 |
support for parallel build jobs, in addition to the multithreaded
|
|
26 |
theory and proof checking that is already provided by the prover
|
|
27 |
process itself. *}
|
|
28 |
|
48578
|
29 |
|
|
30 |
section {* Session ROOT specifications \label{sec:session-root} *}
|
|
31 |
|
48579
|
32 |
text {* Session specifications reside in files called @{verbatim ROOT}
|
|
33 |
within certain directories, such as the home locations of registered
|
|
34 |
Isabelle components or additional project directories given by the
|
|
35 |
user.
|
|
36 |
|
|
37 |
The ROOT file format follows the lexical conventions of the
|
|
38 |
\emph{outer syntax} of Isabelle/Isar, see also
|
|
39 |
\cite{isabelle-isar-ref}. This defines common forms like
|
|
40 |
identifiers, names, quoted strings, verbatim text, nested comments
|
|
41 |
etc. The grammar for a single @{syntax session_entry} is given as
|
|
42 |
syntax diagram below; each ROOT file may contain multiple session
|
|
43 |
specifications like this.
|
|
44 |
|
48582
|
45 |
Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
|
|
46 |
mode @{verbatim "isabelle-root"} for session ROOT files.
|
48579
|
47 |
|
|
48 |
@{rail "
|
|
49 |
@{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
|
|
50 |
;
|
|
51 |
body: description? options? ( theories * ) files?
|
|
52 |
;
|
|
53 |
spec: @{syntax name} '!'? groups? dir?
|
|
54 |
;
|
|
55 |
groups: '(' (@{syntax name} +) ')'
|
|
56 |
;
|
|
57 |
dir: @'in' @{syntax name}
|
|
58 |
;
|
|
59 |
description: @'description' @{syntax text}
|
|
60 |
;
|
|
61 |
options: @'options' opts
|
|
62 |
;
|
|
63 |
opts: '[' ( (@{syntax name} '=' @{syntax name} | @{syntax name}) + ',' ) ']'
|
|
64 |
;
|
|
65 |
theories: @'theories' opts? ( @{syntax name} + )
|
|
66 |
;
|
|
67 |
files: @'files' ( @{syntax name} + )
|
|
68 |
"}
|
|
69 |
|
|
70 |
\begin{description}
|
|
71 |
|
|
72 |
\item \isakeyword{session}~@{text "A = B + body"} defines a new
|
|
73 |
session @{text "A"} based on parent session @{text "B"}, with its
|
|
74 |
content given in @{text body} (theories and auxiliary source files).
|
|
75 |
Note that a parent (like @{text "HOL"}) is mandatory in practical
|
|
76 |
applications: only Isabelle/Pure can bootstrap itself from nothing.
|
|
77 |
|
|
78 |
All such session specifications together describe a hierarchy (tree)
|
|
79 |
of sessions, with globally unique names. By default, names are
|
|
80 |
derived from parent ones by concatenation, i.e.\ @{text "B\<dash>A"}
|
|
81 |
above. Cumulatively, this leads to session paths of the form @{text
|
|
82 |
"X\<dash>Y\<dash>Z\<dash>W"}. Note that in the specification,
|
|
83 |
@{text B} is already such a fully-qualified name, while @{text "A"}
|
|
84 |
is the new base name.
|
|
85 |
|
|
86 |
\item \isakeyword{session}~@{text "A! = B"} indicates a fresh start
|
|
87 |
in the naming scheme: the session is called just @{text "A"} instead
|
|
88 |
of @{text "B\<dash>A"}. Here the name @{text "A"} should be
|
|
89 |
sufficiently long to stand on its own in a potentially large
|
|
90 |
library.
|
|
91 |
|
|
92 |
\item \isakeyword{session}~@{text "A (groups)"} indicates a
|
|
93 |
collection of groups where the new session is a member. Group names
|
|
94 |
are uninterpreted and merely follow certain conventions. For
|
|
95 |
example, the Isabelle distribution tags some important sessions by
|
48604
|
96 |
the group name called ``@{text "main"}''. Other projects may invent
|
|
97 |
their own conventions, but this requires some care to avoid clashes
|
|
98 |
within this unchecked name space.
|
48579
|
99 |
|
|
100 |
\item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
|
|
101 |
specifies an explicit directory for this session. By default,
|
|
102 |
\isakeyword{session}~@{text "A"} abbreviates
|
|
103 |
\isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "A"}. This
|
|
104 |
accommodates the common scheme where some base directory contains
|
|
105 |
several sessions in sub-directories of corresponding names. Another
|
|
106 |
common scheme is \isakeyword{session}~@{text
|
|
107 |
"A"}~\isakeyword{in}~@{verbatim "\".\""} to refer to the current
|
|
108 |
directory of the ROOT file.
|
|
109 |
|
|
110 |
All theories and auxiliary source files are located relatively to
|
|
111 |
the session directory. The prover process is run within the same as
|
|
112 |
its current working directory.
|
|
113 |
|
|
114 |
\item \isakeyword{description}~@{text "text"} is a free-form
|
|
115 |
annotation for this session.
|
|
116 |
|
|
117 |
\item \isakeyword{options}~@{text "[x = a, y = b, z]"} defines
|
48604
|
118 |
separate options (\secref{sec:system-options}) that are used when
|
|
119 |
processing this session, but \emph{without} propagation to child
|
|
120 |
sessions. Note that @{text "z"} abbreviates @{text "z = true"} for
|
|
121 |
Boolean options.
|
48579
|
122 |
|
|
123 |
\item \isakeyword{theories}~@{text "options names"} specifies a
|
|
124 |
block of theories that are processed within an environment that is
|
48604
|
125 |
augmented by the given options, in addition to the global session
|
|
126 |
options given before. Any number of blocks of \isakeyword{theories}
|
|
127 |
may be given. Options are only active for each
|
|
128 |
\isakeyword{theories} block separately.
|
48579
|
129 |
|
|
130 |
\item \isakeyword{files}~@{text "files"} lists additional source
|
48604
|
131 |
files that are involved in the processing of this session. This
|
|
132 |
should cover anything outside the formal content of the theory
|
48579
|
133 |
sources, say some auxiliary {\TeX} files that are required for
|
|
134 |
document processing. In contrast, files that are specified in
|
|
135 |
formal theory headers as @{keyword "uses"} need not be declared
|
|
136 |
again.
|
|
137 |
|
|
138 |
\end{description}
|
48580
|
139 |
*}
|
48579
|
140 |
|
48580
|
141 |
subsubsection {* Examples *}
|
|
142 |
|
|
143 |
text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
|
|
144 |
relevant situations. *}
|
48578
|
145 |
|
|
146 |
|
|
147 |
section {* System build options \label{sec:system-options} *}
|
|
148 |
|
48580
|
149 |
text {* See @{file "~~/etc/options"} for the main defaults provided by
|
48582
|
150 |
the Isabelle distribution. Isabelle/jEdit (\secref{sec:tool-jedit})
|
|
151 |
includes a simple editing mode @{verbatim "isabelle-options"} for
|
|
152 |
this file-format.
|
48580
|
153 |
*}
|
48578
|
154 |
|
|
155 |
|
|
156 |
section {* Invoking the build process \label{sec:tool-build} *}
|
|
157 |
|
48602
|
158 |
text {* The @{tool_def build} tool invokes the build process for
|
48578
|
159 |
Isabelle sessions. It manages dependencies between sessions,
|
|
160 |
related sources of theories and auxiliary files, and target heap
|
|
161 |
images. Accordingly, it runs instances of the prover process with
|
|
162 |
optional document preparation. Its command-line usage
|
|
163 |
is:\footnote{Isabelle/Scala provides the same functionality via
|
|
164 |
\texttt{isabelle.Build.build}.}
|
48602
|
165 |
\begin{ttbox}
|
|
166 |
Usage: isabelle build [OPTIONS] [SESSIONS ...]
|
48578
|
167 |
|
|
168 |
Options are:
|
|
169 |
-a select all sessions
|
|
170 |
-b build heap images
|
48595
|
171 |
-c clean build
|
48578
|
172 |
-d DIR include session directory with ROOT file
|
|
173 |
-g NAME select session group NAME
|
|
174 |
-j INT maximum number of parallel jobs (default 1)
|
|
175 |
-n no build -- test dependencies only
|
|
176 |
-o OPTION override session configuration OPTION
|
|
177 |
(via NAME=VAL or NAME)
|
|
178 |
-s system build mode: produce output in ISABELLE_HOME
|
|
179 |
-v verbose
|
|
180 |
|
|
181 |
Build and manage Isabelle sessions, depending on implicit
|
|
182 |
ISABELLE_BUILD_OPTIONS="..."
|
|
183 |
|
|
184 |
ML_PLATFORM="..."
|
|
185 |
ML_HOME="..."
|
|
186 |
ML_SYSTEM="..."
|
|
187 |
ML_OPTIONS="..."
|
|
188 |
\end{ttbox}
|
|
189 |
|
|
190 |
\medskip Isabelle sessions are defined via session ROOT files as
|
|
191 |
described in (\secref{sec:session-root}). The totality of sessions
|
|
192 |
is determined by collecting such specifications from all Isabelle
|
|
193 |
component directories (\secref{sec:components}), augmented by more
|
|
194 |
directories given via options @{verbatim "-d"}~@{text "DIR"} on the
|
|
195 |
command line. Each such directory may contain a session
|
|
196 |
\texttt{ROOT} file and an additional catalog file @{verbatim
|
|
197 |
"etc/sessions"} with further sub-directories (list of lines). Note
|
|
198 |
that a single \texttt{ROOT} file usually defines many sessions;
|
48591
|
199 |
catalogs are only required for extra scalability and modularity
|
48578
|
200 |
of large libraries.
|
|
201 |
|
48604
|
202 |
\medskip The subset of sessions to be managed is determined via
|
48578
|
203 |
individual @{text "SESSIONS"} given as command-line arguments, or
|
48604
|
204 |
session groups that are given via one or more options @{verbatim
|
48578
|
205 |
"-g"}~@{text "NAME"}. Option @{verbatim "-a"} selects all sessions.
|
48604
|
206 |
The build tool takes session dependencies into account: the set of
|
|
207 |
selected sessions is completed by including all ancestors.
|
48578
|
208 |
|
48604
|
209 |
\medskip The build process depends on additional options
|
|
210 |
(\secref{sec:system-options}) that are passed to the prover
|
|
211 |
eventually. The settings variable @{setting_ref
|
|
212 |
ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\
|
|
213 |
\texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,
|
|
214 |
the environment of system build options may be augmented on the
|
|
215 |
command line via @{verbatim "-o"}~@{text "name"}@{verbatim
|
|
216 |
"="}@{text "value"} or @{verbatim "-o"}~@{text "name"}, which
|
|
217 |
abbreviates @{verbatim "-o"}~@{text "name"}@{verbatim"=true"} for
|
|
218 |
Boolean options. Multiple occurrences of @{verbatim "-o"} on the
|
|
219 |
command-line are applied in the given order.
|
48578
|
220 |
|
|
221 |
\medskip Option @{verbatim "-b"} ensures that heap images are
|
|
222 |
produced for all selected sessions. By default, images are only
|
|
223 |
saved for inner nodes of the hierarchy of sessions, as required for
|
|
224 |
other sessions to continue later on.
|
|
225 |
|
48595
|
226 |
\medskip Option @{verbatim "-c"} cleans all descendants of the
|
|
227 |
selected sessions before performing the specified build operation.
|
|
228 |
|
|
229 |
\medskip Option @{verbatim "-n"} omits the actual build process
|
|
230 |
after the preparatory stage (including optional cleanup). Note that
|
|
231 |
the return code always indicates the status of the set of selected
|
|
232 |
sessions.
|
|
233 |
|
48578
|
234 |
\medskip Option @{verbatim "-j"} specifies the maximum number of
|
48604
|
235 |
parallel build jobs (prover processes). Each prover process is
|
|
236 |
subject to a separate limit of parallel worker threads, cf.\ system
|
|
237 |
option @{system_option_ref threads}.
|
48578
|
238 |
|
|
239 |
\medskip Option @{verbatim "-s"} enables \emph{system mode}, which
|
|
240 |
means that resulting heap images and log files are stored in
|
|
241 |
@{verbatim "$ISABELLE_HOME/heaps"} instead of the default location
|
|
242 |
@{setting ISABELLE_OUTPUT} (which is normally in @{setting
|
|
243 |
ISABELLE_HOME_USER}, i.e.\ the user's home directory).
|
|
244 |
|
|
245 |
\medskip Option @{verbatim "-v"} enables verbose mode.
|
|
246 |
*}
|
|
247 |
|
|
248 |
subsubsection {* Examples *}
|
|
249 |
|
|
250 |
text {*
|
|
251 |
Build a specific logic image:
|
|
252 |
\begin{ttbox}
|
|
253 |
isabelle build -b HOLCF
|
|
254 |
\end{ttbox}
|
|
255 |
|
48604
|
256 |
\smallskip Build the main group of logic images:
|
48578
|
257 |
\begin{ttbox}
|
|
258 |
isabelle build -b -g main
|
|
259 |
\end{ttbox}
|
|
260 |
|
48595
|
261 |
\smallskip Provide a general overview of the status of all Isabelle
|
|
262 |
sessions, without building anything:
|
48578
|
263 |
\begin{ttbox}
|
|
264 |
isabelle build -a -n -v
|
|
265 |
\end{ttbox}
|
|
266 |
|
48595
|
267 |
\smallskip Build all sessions with HTML browser info and PDF
|
|
268 |
document preparation:
|
48578
|
269 |
\begin{ttbox}
|
|
270 |
isabelle build -a -o browser_info -o document=pdf
|
|
271 |
\end{ttbox}
|
|
272 |
|
48604
|
273 |
\smallskip Build all sessions with a maximum of 8 parallel prover
|
|
274 |
processes and 4 worker threads each (on a machine with many cores):
|
48578
|
275 |
\begin{ttbox}
|
|
276 |
isabelle build -a -j8 -o threads=4
|
|
277 |
\end{ttbox}
|
48595
|
278 |
|
|
279 |
\smallskip Build some session images with cleanup of their
|
|
280 |
descendants, while retaining their ancestry:
|
|
281 |
\begin{ttbox}
|
|
282 |
isabelle build -b -c HOL-Boogie HOL-SPARK
|
|
283 |
\end{ttbox}
|
|
284 |
|
|
285 |
\smallskip Clean all sessions without building anything:
|
|
286 |
\begin{ttbox}
|
|
287 |
isabelle build -a -n -c
|
|
288 |
\end{ttbox}
|
48578
|
289 |
*}
|
|
290 |
|
|
291 |
end
|