author | wenzelm |
Sun, 05 Aug 2012 20:11:32 +0200 | |
changeset 48683 | eeb4480b5877 |
parent 48650 | 47330b712f8f |
child 48684 | 9170e10c651e |
permissions | -rw-r--r-- |
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}}}}[] |
|
48605
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
142 |
\rail@nont{\isa{value}}[] |
48581 | 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 |
|
48605
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
151 |
\rail@begin{2}{\isa{value}} |
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
152 |
\rail@bar |
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
153 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
154 |
\rail@nextbar{1} |
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
155 |
\rail@nont{\hyperlink{syntax.real}{\mbox{\isa{real}}}}[] |
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
156 |
\rail@endbar |
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
157 |
\rail@end |
48581 | 158 |
\rail@begin{2}{\isa{theories}} |
159 |
\rail@term{\isa{\isakeyword{theories}}}[] |
|
160 |
\rail@bar |
|
161 |
\rail@nextbar{1} |
|
162 |
\rail@nont{\isa{opts}}[] |
|
163 |
\rail@endbar |
|
164 |
\rail@plus |
|
165 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
|
166 |
\rail@nextplus{1} |
|
167 |
\rail@endplus |
|
168 |
\rail@end |
|
169 |
\rail@begin{2}{\isa{files}} |
|
170 |
\rail@term{\isa{\isakeyword{files}}}[] |
|
171 |
\rail@plus |
|
172 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
|
173 |
\rail@nextplus{1} |
|
174 |
\rail@endplus |
|
175 |
\rail@end |
|
176 |
\end{railoutput} |
|
177 |
||
178 |
||
179 |
\begin{description} |
|
180 |
||
181 |
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3D}{\isacharequal}}\ B\ {\isaliteral{2B}{\isacharplus}}\ body{\isaliteral{22}{\isachardoublequote}}} defines a new |
|
182 |
session \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} based on parent session \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{22}{\isachardoublequote}}}, with its |
|
183 |
content given in \isa{body} (theories and auxiliary source files). |
|
184 |
Note that a parent (like \isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{22}{\isachardoublequote}}}) is mandatory in practical |
|
185 |
applications: only Isabelle/Pure can bootstrap itself from nothing. |
|
186 |
||
187 |
All such session specifications together describe a hierarchy (tree) |
|
188 |
of sessions, with globally unique names. By default, names are |
|
189 |
derived from parent ones by concatenation, i.e.\ \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{5C3C646173683E}{\isasymdash}}A{\isaliteral{22}{\isachardoublequote}}} |
|
190 |
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, |
|
191 |
\isa{B} is already such a fully-qualified name, while \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} |
|
192 |
is the new base name. |
|
193 |
||
194 |
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{21}{\isacharbang}}\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{22}{\isachardoublequote}}} indicates a fresh start |
|
195 |
in the naming scheme: the session is called just \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} instead |
|
196 |
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 |
|
197 |
sufficiently long to stand on its own in a potentially large |
|
198 |
library. |
|
199 |
||
200 |
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{28}{\isacharparenleft}}groups{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} indicates a |
|
201 |
collection of groups where the new session is a member. Group names |
|
202 |
are uninterpreted and merely follow certain conventions. For |
|
203 |
example, the Isabelle distribution tags some important sessions by |
|
48604 | 204 |
the group name called ``\isa{{\isaliteral{22}{\isachardoublequote}}main{\isaliteral{22}{\isachardoublequote}}}''. Other projects may invent |
205 |
their own conventions, but this requires some care to avoid clashes |
|
206 |
within this unchecked name space. |
|
48581 | 207 |
|
208 |
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}dir{\isaliteral{22}{\isachardoublequote}}} |
|
209 |
specifies an explicit directory for this session. By default, |
|
210 |
\isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} abbreviates |
|
211 |
\isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}. This |
|
212 |
accommodates the common scheme where some base directory contains |
|
213 |
several sessions in sub-directories of corresponding names. Another |
|
214 |
common scheme is \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\verb|"."| to refer to the current |
|
215 |
directory of the ROOT file. |
|
216 |
||
217 |
All theories and auxiliary source files are located relatively to |
|
218 |
the session directory. The prover process is run within the same as |
|
219 |
its current working directory. |
|
220 |
||
221 |
\item \isakeyword{description}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} is a free-form |
|
222 |
annotation for this session. |
|
223 |
||
224 |
\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 | 225 |
separate options (\secref{sec:system-options}) that are used when |
226 |
processing this session, but \emph{without} propagation to child |
|
227 |
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 |
|
228 |
Boolean options. |
|
48581 | 229 |
|
230 |
\item \isakeyword{theories}~\isa{{\isaliteral{22}{\isachardoublequote}}options\ names{\isaliteral{22}{\isachardoublequote}}} specifies a |
|
231 |
block of theories that are processed within an environment that is |
|
48604 | 232 |
augmented by the given options, in addition to the global session |
233 |
options given before. Any number of blocks of \isakeyword{theories} |
|
234 |
may be given. Options are only active for each |
|
235 |
\isakeyword{theories} block separately. |
|
48581 | 236 |
|
237 |
\item \isakeyword{files}~\isa{{\isaliteral{22}{\isachardoublequote}}files{\isaliteral{22}{\isachardoublequote}}} lists additional source |
|
48604 | 238 |
files that are involved in the processing of this session. This |
239 |
should cover anything outside the formal content of the theory |
|
48581 | 240 |
sources, say some auxiliary {\TeX} files that are required for |
241 |
document processing. In contrast, files that are specified in |
|
242 |
formal theory headers as \hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} need not be declared |
|
243 |
again. |
|
244 |
||
245 |
\end{description}% |
|
246 |
\end{isamarkuptext}% |
|
247 |
\isamarkuptrue% |
|
248 |
% |
|
249 |
\isamarkupsubsubsection{Examples% |
|
250 |
} |
|
251 |
\isamarkuptrue% |
|
252 |
% |
|
253 |
\begin{isamarkuptext}% |
|
254 |
See \verb|~~/src/HOL/ROOT| for a diversity of practically |
|
255 |
relevant situations.% |
|
256 |
\end{isamarkuptext}% |
|
257 |
\isamarkuptrue% |
|
258 |
% |
|
259 |
\isamarkupsection{System build options \label{sec:system-options}% |
|
260 |
} |
|
261 |
\isamarkuptrue% |
|
262 |
% |
|
263 |
\begin{isamarkuptext}% |
|
264 |
See \verb|~~/etc/options| for the main defaults provided by |
|
48582 | 265 |
the Isabelle distribution. Isabelle/jEdit (\secref{sec:tool-jedit}) |
266 |
includes a simple editing mode \verb|isabelle-options| for |
|
267 |
this file-format.% |
|
48581 | 268 |
\end{isamarkuptext}% |
269 |
\isamarkuptrue% |
|
270 |
% |
|
271 |
\isamarkupsection{Invoking the build process \label{sec:tool-build}% |
|
272 |
} |
|
273 |
\isamarkuptrue% |
|
274 |
% |
|
275 |
\begin{isamarkuptext}% |
|
48602 | 276 |
The \indexdef{}{tool}{build}\hypertarget{tool.build}{\hyperlink{tool.build}{\mbox{\isa{\isatool{build}}}}} tool invokes the build process for |
48581 | 277 |
Isabelle sessions. It manages dependencies between sessions, |
278 |
related sources of theories and auxiliary files, and target heap |
|
279 |
images. Accordingly, it runs instances of the prover process with |
|
280 |
optional document preparation. Its command-line usage |
|
281 |
is:\footnote{Isabelle/Scala provides the same functionality via |
|
282 |
\texttt{isabelle.Build.build}.} |
|
48602 | 283 |
\begin{ttbox} |
284 |
Usage: isabelle build [OPTIONS] [SESSIONS ...] |
|
48581 | 285 |
|
286 |
Options are: |
|
287 |
-a select all sessions |
|
288 |
-b build heap images |
|
48595 | 289 |
-c clean build |
48581 | 290 |
-d DIR include session directory with ROOT file |
291 |
-g NAME select session group NAME |
|
292 |
-j INT maximum number of parallel jobs (default 1) |
|
293 |
-n no build -- test dependencies only |
|
294 |
-o OPTION override session configuration OPTION |
|
295 |
(via NAME=VAL or NAME) |
|
296 |
-s system build mode: produce output in ISABELLE_HOME |
|
297 |
-v verbose |
|
298 |
||
299 |
Build and manage Isabelle sessions, depending on implicit |
|
300 |
ISABELLE_BUILD_OPTIONS="..." |
|
301 |
||
302 |
ML_PLATFORM="..." |
|
303 |
ML_HOME="..." |
|
304 |
ML_SYSTEM="..." |
|
305 |
ML_OPTIONS="..." |
|
306 |
\end{ttbox} |
|
307 |
||
308 |
\medskip Isabelle sessions are defined via session ROOT files as |
|
309 |
described in (\secref{sec:session-root}). The totality of sessions |
|
310 |
is determined by collecting such specifications from all Isabelle |
|
311 |
component directories (\secref{sec:components}), augmented by more |
|
312 |
directories given via options \verb|-d|~\isa{{\isaliteral{22}{\isachardoublequote}}DIR{\isaliteral{22}{\isachardoublequote}}} on the |
|
313 |
command line. Each such directory may contain a session |
|
48650 | 314 |
\texttt{ROOT} file with several session specifications. |
48581 | 315 |
|
48604 | 316 |
\medskip The subset of sessions to be managed is determined via |
48581 | 317 |
individual \isa{{\isaliteral{22}{\isachardoublequote}}SESSIONS{\isaliteral{22}{\isachardoublequote}}} given as command-line arguments, or |
48604 | 318 |
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. |
319 |
The build tool takes session dependencies into account: the set of |
|
320 |
selected sessions is completed by including all ancestors. |
|
48581 | 321 |
|
48604 | 322 |
\medskip The build process depends on additional options |
323 |
(\secref{sec:system-options}) that are passed to the prover |
|
324 |
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.\ |
|
325 |
\texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover, |
|
326 |
the environment of system build options may be augmented on the |
|
327 |
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 |
|
328 |
abbreviates \verb|-o|~\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{22}{\isachardoublequote}}}\verb|=true| for |
|
329 |
Boolean options. Multiple occurrences of \verb|-o| on the |
|
330 |
command-line are applied in the given order. |
|
48581 | 331 |
|
332 |
\medskip Option \verb|-b| ensures that heap images are |
|
333 |
produced for all selected sessions. By default, images are only |
|
334 |
saved for inner nodes of the hierarchy of sessions, as required for |
|
335 |
other sessions to continue later on. |
|
336 |
||
48595 | 337 |
\medskip Option \verb|-c| cleans all descendants of the |
338 |
selected sessions before performing the specified build operation. |
|
339 |
||
340 |
\medskip Option \verb|-n| omits the actual build process |
|
341 |
after the preparatory stage (including optional cleanup). Note that |
|
342 |
the return code always indicates the status of the set of selected |
|
343 |
sessions. |
|
344 |
||
48581 | 345 |
\medskip Option \verb|-j| specifies the maximum number of |
48604 | 346 |
parallel build jobs (prover processes). Each prover process is |
347 |
subject to a separate limit of parallel worker threads, cf.\ system |
|
348 |
option \indexref{}{system option}{threads}\hyperlink{system option.threads}{\mbox{\isa{\isatt{threads}}}}. |
|
48581 | 349 |
|
350 |
\medskip Option \verb|-s| enables \emph{system mode}, which |
|
351 |
means that resulting heap images and log files are stored in |
|
352 |
\verb|$ISABELLE_HOME/heaps| instead of the default location |
|
353 |
\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). |
|
354 |
||
355 |
\medskip Option \verb|-v| enables verbose mode.% |
|
356 |
\end{isamarkuptext}% |
|
357 |
\isamarkuptrue% |
|
358 |
% |
|
359 |
\isamarkupsubsubsection{Examples% |
|
360 |
} |
|
361 |
\isamarkuptrue% |
|
362 |
% |
|
363 |
\begin{isamarkuptext}% |
|
364 |
Build a specific logic image: |
|
365 |
\begin{ttbox} |
|
366 |
isabelle build -b HOLCF |
|
367 |
\end{ttbox} |
|
368 |
||
48604 | 369 |
\smallskip Build the main group of logic images: |
48581 | 370 |
\begin{ttbox} |
371 |
isabelle build -b -g main |
|
372 |
\end{ttbox} |
|
373 |
||
48595 | 374 |
\smallskip Provide a general overview of the status of all Isabelle |
375 |
sessions, without building anything: |
|
48581 | 376 |
\begin{ttbox} |
377 |
isabelle build -a -n -v |
|
378 |
\end{ttbox} |
|
379 |
||
48595 | 380 |
\smallskip Build all sessions with HTML browser info and PDF |
381 |
document preparation: |
|
48581 | 382 |
\begin{ttbox} |
383 |
isabelle build -a -o browser_info -o document=pdf |
|
384 |
\end{ttbox} |
|
385 |
||
48604 | 386 |
\smallskip Build all sessions with a maximum of 8 parallel prover |
387 |
processes and 4 worker threads each (on a machine with many cores): |
|
48581 | 388 |
\begin{ttbox} |
389 |
isabelle build -a -j8 -o threads=4 |
|
48595 | 390 |
\end{ttbox} |
391 |
||
392 |
\smallskip Build some session images with cleanup of their |
|
393 |
descendants, while retaining their ancestry: |
|
394 |
\begin{ttbox} |
|
395 |
isabelle build -b -c HOL-Boogie HOL-SPARK |
|
396 |
\end{ttbox} |
|
397 |
||
398 |
\smallskip Clean all sessions without building anything: |
|
399 |
\begin{ttbox} |
|
400 |
isabelle build -a -n -c |
|
48581 | 401 |
\end{ttbox}% |
402 |
\end{isamarkuptext}% |
|
403 |
\isamarkuptrue% |
|
404 |
% |
|
48683 | 405 |
\isamarkupsection{Preparing session root directories \label{sec:tool-mkroot}% |
406 |
} |
|
407 |
\isamarkuptrue% |
|
408 |
% |
|
409 |
\begin{isamarkuptext}% |
|
410 |
The \indexdef{}{tool}{mkroot}\hypertarget{tool.mkroot}{\hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}}} tool prepares Isabelle session source |
|
411 |
directories, including some \verb|ROOT| entry, an example |
|
412 |
theory file, and some initial configuration for document preparation |
|
413 |
(see also \chref{ch:present}). The usage of \hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} is: |
|
414 |
||
415 |
\begin{ttbox} |
|
416 |
Usage: isabelle mkroot NAME |
|
417 |
||
418 |
Prepare session root directory, adding session NAME with |
|
419 |
built-in document preparation. |
|
420 |
\end{ttbox} |
|
421 |
||
422 |
All session-specific files are placed into a separate sub-directory |
|
423 |
given as \verb|NAME| above. The \verb|ROOT| file is in |
|
424 |
the parent position relative to that --- it could refer to several |
|
425 |
such sessions. The \hyperlink{tool.mkroot}{\mbox{\isa{\isatool{mkroot}}}} tool is conservative in the sense |
|
426 |
that does not overwrite an existing session sub-directory; an |
|
427 |
already existing \verb|ROOT| file is extended. |
|
428 |
||
429 |
The implicit Isabelle settings variable \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LOGIC}}}} |
|
430 |
specifies the parent session, and \hyperlink{setting.ISABELLE-DOCUMENT-FORMAT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DOCUMENT{\isaliteral{5F}{\isacharunderscore}}FORMAT}}}} the document format to be filled filled |
|
431 |
into the generated \verb|ROOT| file.% |
|
432 |
\end{isamarkuptext}% |
|
433 |
\isamarkuptrue% |
|
434 |
% |
|
435 |
\isamarkupsubsubsection{Examples% |
|
436 |
} |
|
437 |
\isamarkuptrue% |
|
438 |
% |
|
439 |
\begin{isamarkuptext}% |
|
440 |
The following produces an example session, relatively to the |
|
441 |
\verb|ROOT| in the current directory: |
|
442 |
\begin{ttbox} |
|
443 |
isabelle mkroot Test && isabelle build -v -d. Test |
|
444 |
\end{ttbox} |
|
445 |
||
446 |
Option \verb|-v| is not required, but useful to reveal the |
|
447 |
the location of generated documents.% |
|
448 |
\end{isamarkuptext}% |
|
449 |
\isamarkuptrue% |
|
450 |
% |
|
48581 | 451 |
\isadelimtheory |
452 |
% |
|
453 |
\endisadelimtheory |
|
454 |
% |
|
455 |
\isatagtheory |
|
456 |
\isacommand{end}\isamarkupfalse% |
|
457 |
% |
|
458 |
\endisatagtheory |
|
459 |
{\isafoldtheory}% |
|
460 |
% |
|
461 |
\isadelimtheory |
|
462 |
% |
|
463 |
\endisadelimtheory |
|
464 |
\isanewline |
|
465 |
\end{isabellebody}% |
|
466 |
%%% Local Variables: |
|
467 |
%%% mode: latex |
|
468 |
%%% TeX-master: "root" |
|
469 |
%%% End: |