48581
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Sessions}%
|
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
\isacommand{theory}\isamarkupfalse%
|
|
11 |
\ Sessions\isanewline
|
|
12 |
\isakeyword{imports}\ Base\isanewline
|
|
13 |
\isakeyword{begin}%
|
|
14 |
\endisatagtheory
|
|
15 |
{\isafoldtheory}%
|
|
16 |
%
|
|
17 |
\isadelimtheory
|
|
18 |
%
|
|
19 |
\endisadelimtheory
|
|
20 |
%
|
48584
|
21 |
\isamarkupchapter{Isabelle sessions and build management \label{ch:session}%
|
48581
|
22 |
}
|
|
23 |
\isamarkuptrue%
|
|
24 |
%
|
|
25 |
\begin{isamarkuptext}%
|
48584
|
26 |
An Isabelle \emph{session} consists of a collection of related
|
48604
|
27 |
theories that may be associated with formal documents (see also
|
|
28 |
\chref{ch:present}). There is also a notion of \emph{persistent
|
|
29 |
heap} image to capture the state of a session, similar to
|
|
30 |
object-code in compiled programming languages. Thus the concept of
|
|
31 |
session resembles that of a ``project'' in common IDE environments,
|
|
32 |
but the specific name emphasizes the connection to interactive
|
|
33 |
theorem proving: the session wraps-up the results of
|
|
34 |
user-interaction with the prover in a persistent form.
|
48584
|
35 |
|
48604
|
36 |
Application sessions are built on a given parent session, which may
|
|
37 |
be built recursively on other parents. Following this path in the
|
|
38 |
hierarchy eventually leads to some major object-logic session like
|
|
39 |
\isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{22}{\isachardoublequote}}}, which itself is based on \isa{{\isaliteral{22}{\isachardoublequote}}Pure{\isaliteral{22}{\isachardoublequote}}} as the common
|
|
40 |
root of all sessions.
|
48584
|
41 |
|
48604
|
42 |
Processing sessions may take considerable time. Isabelle build
|
|
43 |
management helps to organize this efficiently. This includes
|
|
44 |
support for parallel build jobs, in addition to the multithreaded
|
|
45 |
theory and proof checking that is already provided by the prover
|
|
46 |
process itself.%
|
48581
|
47 |
\end{isamarkuptext}%
|
|
48 |
\isamarkuptrue%
|
|
49 |
%
|
|
50 |
\isamarkupsection{Session ROOT specifications \label{sec:session-root}%
|
|
51 |
}
|
|
52 |
\isamarkuptrue%
|
|
53 |
%
|
|
54 |
\begin{isamarkuptext}%
|
|
55 |
Session specifications reside in files called \verb|ROOT|
|
|
56 |
within certain directories, such as the home locations of registered
|
|
57 |
Isabelle components or additional project directories given by the
|
|
58 |
user.
|
|
59 |
|
|
60 |
The ROOT file format follows the lexical conventions of the
|
|
61 |
\emph{outer syntax} of Isabelle/Isar, see also
|
|
62 |
\cite{isabelle-isar-ref}. This defines common forms like
|
|
63 |
identifiers, names, quoted strings, verbatim text, nested comments
|
|
64 |
etc. The grammar for a single \hyperlink{syntax.session-entry}{\mbox{\isa{session{\isaliteral{5F}{\isacharunderscore}}entry}}} is given as
|
|
65 |
syntax diagram below; each ROOT file may contain multiple session
|
|
66 |
specifications like this.
|
|
67 |
|
48582
|
68 |
Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
|
|
69 |
mode \verb|isabelle-root| for session ROOT files.
|
48581
|
70 |
|
|
71 |
\begin{railoutput}
|
|
72 |
\rail@begin{2}{\indexdef{}{syntax}{session\_entry}\hypertarget{syntax.session-entry}{\hyperlink{syntax.session-entry}{\mbox{\isa{session{\isaliteral{5F}{\isacharunderscore}}entry}}}}}
|
|
73 |
\rail@term{\isa{\isakeyword{session}}}[]
|
|
74 |
\rail@nont{\isa{spec}}[]
|
|
75 |
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
|
|
76 |
\rail@bar
|
|
77 |
\rail@nextbar{1}
|
|
78 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
|
|
79 |
\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
|
|
80 |
\rail@endbar
|
|
81 |
\rail@nont{\isa{body}}[]
|
|
82 |
\rail@end
|
|
83 |
\rail@begin{2}{\isa{body}}
|
|
84 |
\rail@bar
|
|
85 |
\rail@nextbar{1}
|
|
86 |
\rail@nont{\isa{description}}[]
|
|
87 |
\rail@endbar
|
|
88 |
\rail@bar
|
|
89 |
\rail@nextbar{1}
|
|
90 |
\rail@nont{\isa{options}}[]
|
|
91 |
\rail@endbar
|
|
92 |
\rail@plus
|
|
93 |
\rail@nextplus{1}
|
|
94 |
\rail@cnont{\isa{theories}}[]
|
|
95 |
\rail@endplus
|
|
96 |
\rail@bar
|
|
97 |
\rail@nextbar{1}
|
|
98 |
\rail@nont{\isa{files}}[]
|
|
99 |
\rail@endbar
|
|
100 |
\rail@end
|
|
101 |
\rail@begin{2}{\isa{spec}}
|
|
102 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
|
|
103 |
\rail@bar
|
|
104 |
\rail@nextbar{1}
|
|
105 |
\rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
|
|
106 |
\rail@endbar
|
|
107 |
\rail@bar
|
|
108 |
\rail@nextbar{1}
|
|
109 |
\rail@nont{\isa{groups}}[]
|
|
110 |
\rail@endbar
|
|
111 |
\rail@bar
|
|
112 |
\rail@nextbar{1}
|
|
113 |
\rail@nont{\isa{dir}}[]
|
|
114 |
\rail@endbar
|
|
115 |
\rail@end
|
|
116 |
\rail@begin{2}{\isa{groups}}
|
|
117 |
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
|
|
118 |
\rail@plus
|
|
119 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
|
|
120 |
\rail@nextplus{1}
|
|
121 |
\rail@endplus
|
|
122 |
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
|
|
123 |
\rail@end
|
|
124 |
\rail@begin{1}{\isa{dir}}
|
|
125 |
\rail@term{\isa{\isakeyword{in}}}[]
|
|
126 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
|
|
127 |
\rail@end
|
|
128 |
\rail@begin{1}{\isa{description}}
|
|
129 |
\rail@term{\isa{\isakeyword{description}}}[]
|
|
130 |
\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
|
|
131 |
\rail@end
|
|
132 |
\rail@begin{1}{\isa{options}}
|
|
133 |
\rail@term{\isa{\isakeyword{options}}}[]
|
|
134 |
\rail@nont{\isa{opts}}[]
|
|
135 |
\rail@end
|
|
136 |
\rail@begin{3}{\isa{opts}}
|
|
137 |
\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
|
|
138 |
\rail@plus
|
|
139 |
\rail@bar
|
|
140 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
|
|
141 |
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
|
|
142 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
|
|
143 |
\rail@nextbar{1}
|
|
144 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
|
|
145 |
\rail@endbar
|
|
146 |
\rail@nextplus{2}
|
|
147 |
\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
|
|
148 |
\rail@endplus
|
|
149 |
\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
|
|
150 |
\rail@end
|
|
151 |
\rail@begin{2}{\isa{theories}}
|
|
152 |
\rail@term{\isa{\isakeyword{theories}}}[]
|
|
153 |
\rail@bar
|
|
154 |
\rail@nextbar{1}
|
|
155 |
\rail@nont{\isa{opts}}[]
|
|
156 |
\rail@endbar
|
|
157 |
\rail@plus
|
|
158 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
|
|
159 |
\rail@nextplus{1}
|
|
160 |
\rail@endplus
|
|
161 |
\rail@end
|
|
162 |
\rail@begin{2}{\isa{files}}
|
|
163 |
\rail@term{\isa{\isakeyword{files}}}[]
|
|
164 |
\rail@plus
|
|
165 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
|
|
166 |
\rail@nextplus{1}
|
|
167 |
\rail@endplus
|
|
168 |
\rail@end
|
|
169 |
\end{railoutput}
|
|
170 |
|
|
171 |
|
|
172 |
\begin{description}
|
|
173 |
|
|
174 |
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3D}{\isacharequal}}\ B\ {\isaliteral{2B}{\isacharplus}}\ body{\isaliteral{22}{\isachardoublequote}}} defines a new
|
|
175 |
session \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} based on parent session \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{22}{\isachardoublequote}}}, with its
|
|
176 |
content given in \isa{body} (theories and auxiliary source files).
|
|
177 |
Note that a parent (like \isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{22}{\isachardoublequote}}}) is mandatory in practical
|
|
178 |
applications: only Isabelle/Pure can bootstrap itself from nothing.
|
|
179 |
|
|
180 |
All such session specifications together describe a hierarchy (tree)
|
|
181 |
of sessions, with globally unique names. By default, names are
|
|
182 |
derived from parent ones by concatenation, i.e.\ \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{5C3C646173683E}{\isasymdash}}A{\isaliteral{22}{\isachardoublequote}}}
|
|
183 |
above. Cumulatively, this leads to session paths of the form \isa{{\isaliteral{22}{\isachardoublequote}}X{\isaliteral{5C3C646173683E}{\isasymdash}}Y{\isaliteral{5C3C646173683E}{\isasymdash}}Z{\isaliteral{5C3C646173683E}{\isasymdash}}W{\isaliteral{22}{\isachardoublequote}}}. Note that in the specification,
|
|
184 |
\isa{B} is already such a fully-qualified name, while \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}
|
|
185 |
is the new base name.
|
|
186 |
|
|
187 |
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{21}{\isacharbang}}\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{22}{\isachardoublequote}}} indicates a fresh start
|
|
188 |
in the naming scheme: the session is called just \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} instead
|
|
189 |
of \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{5C3C646173683E}{\isasymdash}}A{\isaliteral{22}{\isachardoublequote}}}. Here the name \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} should be
|
|
190 |
sufficiently long to stand on its own in a potentially large
|
|
191 |
library.
|
|
192 |
|
|
193 |
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{28}{\isacharparenleft}}groups{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} indicates a
|
|
194 |
collection of groups where the new session is a member. Group names
|
|
195 |
are uninterpreted and merely follow certain conventions. For
|
|
196 |
example, the Isabelle distribution tags some important sessions by
|
48604
|
197 |
the group name called ``\isa{{\isaliteral{22}{\isachardoublequote}}main{\isaliteral{22}{\isachardoublequote}}}''. Other projects may invent
|
|
198 |
their own conventions, but this requires some care to avoid clashes
|
|
199 |
within this unchecked name space.
|
48581
|
200 |
|
|
201 |
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}dir{\isaliteral{22}{\isachardoublequote}}}
|
|
202 |
specifies an explicit directory for this session. By default,
|
|
203 |
\isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} abbreviates
|
|
204 |
\isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}. This
|
|
205 |
accommodates the common scheme where some base directory contains
|
|
206 |
several sessions in sub-directories of corresponding names. Another
|
|
207 |
common scheme is \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\verb|"."| to refer to the current
|
|
208 |
directory of the ROOT file.
|
|
209 |
|
|
210 |
All theories and auxiliary source files are located relatively to
|
|
211 |
the session directory. The prover process is run within the same as
|
|
212 |
its current working directory.
|
|
213 |
|
|
214 |
\item \isakeyword{description}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} is a free-form
|
|
215 |
annotation for this session.
|
|
216 |
|
|
217 |
\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
|
48604
|
218 |
separate options (\secref{sec:system-options}) that are used when
|
|
219 |
processing this session, but \emph{without} propagation to child
|
|
220 |
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
|
|
221 |
Boolean options.
|
48581
|
222 |
|
|
223 |
\item \isakeyword{theories}~\isa{{\isaliteral{22}{\isachardoublequote}}options\ names{\isaliteral{22}{\isachardoublequote}}} specifies a
|
|
224 |
block of theories that are processed within an environment that is
|
48604
|
225 |
augmented by the given options, in addition to the global session
|
|
226 |
options given before. Any number of blocks of \isakeyword{theories}
|
|
227 |
may be given. Options are only active for each
|
|
228 |
\isakeyword{theories} block separately.
|
48581
|
229 |
|
|
230 |
\item \isakeyword{files}~\isa{{\isaliteral{22}{\isachardoublequote}}files{\isaliteral{22}{\isachardoublequote}}} lists additional source
|
48604
|
231 |
files that are involved in the processing of this session. This
|
|
232 |
should cover anything outside the formal content of the theory
|
48581
|
233 |
sources, say some auxiliary {\TeX} files that are required for
|
|
234 |
document processing. In contrast, files that are specified in
|
|
235 |
formal theory headers as \hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} need not be declared
|
|
236 |
again.
|
|
237 |
|
|
238 |
\end{description}%
|
|
239 |
\end{isamarkuptext}%
|
|
240 |
\isamarkuptrue%
|
|
241 |
%
|
|
242 |
\isamarkupsubsubsection{Examples%
|
|
243 |
}
|
|
244 |
\isamarkuptrue%
|
|
245 |
%
|
|
246 |
\begin{isamarkuptext}%
|
|
247 |
See \verb|~~/src/HOL/ROOT| for a diversity of practically
|
|
248 |
relevant situations.%
|
|
249 |
\end{isamarkuptext}%
|
|
250 |
\isamarkuptrue%
|
|
251 |
%
|
|
252 |
\isamarkupsection{System build options \label{sec:system-options}%
|
|
253 |
}
|
|
254 |
\isamarkuptrue%
|
|
255 |
%
|
|
256 |
\begin{isamarkuptext}%
|
|
257 |
See \verb|~~/etc/options| for the main defaults provided by
|
48582
|
258 |
the Isabelle distribution. Isabelle/jEdit (\secref{sec:tool-jedit})
|
|
259 |
includes a simple editing mode \verb|isabelle-options| for
|
|
260 |
this file-format.%
|
48581
|
261 |
\end{isamarkuptext}%
|
|
262 |
\isamarkuptrue%
|
|
263 |
%
|
|
264 |
\isamarkupsection{Invoking the build process \label{sec:tool-build}%
|
|
265 |
}
|
|
266 |
\isamarkuptrue%
|
|
267 |
%
|
|
268 |
\begin{isamarkuptext}%
|
48602
|
269 |
The \indexdef{}{tool}{build}\hypertarget{tool.build}{\hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}}} tool invokes the build process for
|
48581
|
270 |
Isabelle sessions. It manages dependencies between sessions,
|
|
271 |
related sources of theories and auxiliary files, and target heap
|
|
272 |
images. Accordingly, it runs instances of the prover process with
|
|
273 |
optional document preparation. Its command-line usage
|
|
274 |
is:\footnote{Isabelle/Scala provides the same functionality via
|
|
275 |
\texttt{isabelle.Build.build}.}
|
48602
|
276 |
\begin{ttbox}
|
|
277 |
Usage: isabelle build [OPTIONS] [SESSIONS ...]
|
48581
|
278 |
|
|
279 |
Options are:
|
|
280 |
-a select all sessions
|
|
281 |
-b build heap images
|
48595
|
282 |
-c clean build
|
48581
|
283 |
-d DIR include session directory with ROOT file
|
|
284 |
-g NAME select session group NAME
|
|
285 |
-j INT maximum number of parallel jobs (default 1)
|
|
286 |
-n no build -- test dependencies only
|
|
287 |
-o OPTION override session configuration OPTION
|
|
288 |
(via NAME=VAL or NAME)
|
|
289 |
-s system build mode: produce output in ISABELLE_HOME
|
|
290 |
-v verbose
|
|
291 |
|
|
292 |
Build and manage Isabelle sessions, depending on implicit
|
|
293 |
ISABELLE_BUILD_OPTIONS="..."
|
|
294 |
|
|
295 |
ML_PLATFORM="..."
|
|
296 |
ML_HOME="..."
|
|
297 |
ML_SYSTEM="..."
|
|
298 |
ML_OPTIONS="..."
|
|
299 |
\end{ttbox}
|
|
300 |
|
|
301 |
\medskip Isabelle sessions are defined via session ROOT files as
|
|
302 |
described in (\secref{sec:session-root}). The totality of sessions
|
|
303 |
is determined by collecting such specifications from all Isabelle
|
|
304 |
component directories (\secref{sec:components}), augmented by more
|
|
305 |
directories given via options \verb|-d|~\isa{{\isaliteral{22}{\isachardoublequote}}DIR{\isaliteral{22}{\isachardoublequote}}} on the
|
|
306 |
command line. Each such directory may contain a session
|
|
307 |
\texttt{ROOT} file and an additional catalog file \verb|etc/sessions| with further sub-directories (list of lines). Note
|
|
308 |
that a single \texttt{ROOT} file usually defines many sessions;
|
48591
|
309 |
catalogs are only required for extra scalability and modularity
|
48581
|
310 |
of large libraries.
|
|
311 |
|
48604
|
312 |
\medskip The subset of sessions to be managed is determined via
|
48581
|
313 |
individual \isa{{\isaliteral{22}{\isachardoublequote}}SESSIONS{\isaliteral{22}{\isachardoublequote}}} given as command-line arguments, or
|
48604
|
314 |
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.
|
|
315 |
The build tool takes session dependencies into account: the set of
|
|
316 |
selected sessions is completed by including all ancestors.
|
48581
|
317 |
|
48604
|
318 |
\medskip The build process depends on additional options
|
|
319 |
(\secref{sec:system-options}) that are passed to the prover
|
|
320 |
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.\
|
|
321 |
\texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,
|
|
322 |
the environment of system build options may be augmented on the
|
|
323 |
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
|
|
324 |
abbreviates \verb|-o|~\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{22}{\isachardoublequote}}}\verb|=true| for
|
|
325 |
Boolean options. Multiple occurrences of \verb|-o| on the
|
|
326 |
command-line are applied in the given order.
|
48581
|
327 |
|
|
328 |
\medskip Option \verb|-b| ensures that heap images are
|
|
329 |
produced for all selected sessions. By default, images are only
|
|
330 |
saved for inner nodes of the hierarchy of sessions, as required for
|
|
331 |
other sessions to continue later on.
|
|
332 |
|
48595
|
333 |
\medskip Option \verb|-c| cleans all descendants of the
|
|
334 |
selected sessions before performing the specified build operation.
|
|
335 |
|
|
336 |
\medskip Option \verb|-n| omits the actual build process
|
|
337 |
after the preparatory stage (including optional cleanup). Note that
|
|
338 |
the return code always indicates the status of the set of selected
|
|
339 |
sessions.
|
|
340 |
|
48581
|
341 |
\medskip Option \verb|-j| specifies the maximum number of
|
48604
|
342 |
parallel build jobs (prover processes). Each prover process is
|
|
343 |
subject to a separate limit of parallel worker threads, cf.\ system
|
|
344 |
option \indexref{}{system option}{threads}\hyperlink{system option.threads}{\mbox{\isa{\isatt{threads}}}}.
|
48581
|
345 |
|
|
346 |
\medskip Option \verb|-s| enables \emph{system mode}, which
|
|
347 |
means that resulting heap images and log files are stored in
|
|
348 |
\verb|$ISABELLE_HOME/heaps| instead of the default location
|
|
349 |
\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}} (which is normally in \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}}, i.e.\ the user's home directory).
|
|
350 |
|
|
351 |
\medskip Option \verb|-v| enables verbose mode.%
|
|
352 |
\end{isamarkuptext}%
|
|
353 |
\isamarkuptrue%
|
|
354 |
%
|
|
355 |
\isamarkupsubsubsection{Examples%
|
|
356 |
}
|
|
357 |
\isamarkuptrue%
|
|
358 |
%
|
|
359 |
\begin{isamarkuptext}%
|
|
360 |
Build a specific logic image:
|
|
361 |
\begin{ttbox}
|
|
362 |
isabelle build -b HOLCF
|
|
363 |
\end{ttbox}
|
|
364 |
|
48604
|
365 |
\smallskip Build the main group of logic images:
|
48581
|
366 |
\begin{ttbox}
|
|
367 |
isabelle build -b -g main
|
|
368 |
\end{ttbox}
|
|
369 |
|
48595
|
370 |
\smallskip Provide a general overview of the status of all Isabelle
|
|
371 |
sessions, without building anything:
|
48581
|
372 |
\begin{ttbox}
|
|
373 |
isabelle build -a -n -v
|
|
374 |
\end{ttbox}
|
|
375 |
|
48595
|
376 |
\smallskip Build all sessions with HTML browser info and PDF
|
|
377 |
document preparation:
|
48581
|
378 |
\begin{ttbox}
|
|
379 |
isabelle build -a -o browser_info -o document=pdf
|
|
380 |
\end{ttbox}
|
|
381 |
|
48604
|
382 |
\smallskip Build all sessions with a maximum of 8 parallel prover
|
|
383 |
processes and 4 worker threads each (on a machine with many cores):
|
48581
|
384 |
\begin{ttbox}
|
|
385 |
isabelle build -a -j8 -o threads=4
|
48595
|
386 |
\end{ttbox}
|
|
387 |
|
|
388 |
\smallskip Build some session images with cleanup of their
|
|
389 |
descendants, while retaining their ancestry:
|
|
390 |
\begin{ttbox}
|
|
391 |
isabelle build -b -c HOL-Boogie HOL-SPARK
|
|
392 |
\end{ttbox}
|
|
393 |
|
|
394 |
\smallskip Clean all sessions without building anything:
|
|
395 |
\begin{ttbox}
|
|
396 |
isabelle build -a -n -c
|
48581
|
397 |
\end{ttbox}%
|
|
398 |
\end{isamarkuptext}%
|
|
399 |
\isamarkuptrue%
|
|
400 |
%
|
|
401 |
\isadelimtheory
|
|
402 |
%
|
|
403 |
\endisadelimtheory
|
|
404 |
%
|
|
405 |
\isatagtheory
|
|
406 |
\isacommand{end}\isamarkupfalse%
|
|
407 |
%
|
|
408 |
\endisatagtheory
|
|
409 |
{\isafoldtheory}%
|
|
410 |
%
|
|
411 |
\isadelimtheory
|
|
412 |
%
|
|
413 |
\endisadelimtheory
|
|
414 |
\isanewline
|
|
415 |
\end{isabellebody}%
|
|
416 |
%%% Local Variables:
|
|
417 |
%%% mode: latex
|
|
418 |
%%% TeX-master: "root"
|
|
419 |
%%% End:
|