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