author | wenzelm |
Thu, 22 Oct 2015 21:16:49 +0200 | |
changeset 61503 | 28e788ca2c5d |
parent 61493 | 0debd22f0c0e |
child 61568 | 26c76e143b77 |
permissions | -rw-r--r-- |
48578 | 1 |
theory Sessions |
2 |
imports Base |
|
3 |
begin |
|
4 |
||
58618 | 5 |
chapter \<open>Isabelle sessions and build management \label{ch:session}\<close> |
48584 | 6 |
|
61477 | 7 |
text \<open>An Isabelle \<^emph>\<open>session\<close> consists of a collection of related |
51055 | 8 |
theories that may be associated with formal documents |
61477 | 9 |
(\chref{ch:present}). There is also a notion of \<^emph>\<open>persistent |
10 |
heap\<close> image to capture the state of a session, similar to |
|
48604 | 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 |
|
61493 | 20 |
\<open>HOL\<close>, which itself is based on \<open>Pure\<close> as the common |
48604 | 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 |
|
58618 | 27 |
process itself.\<close> |
48604 | 28 |
|
48578 | 29 |
|
58618 | 30 |
section \<open>Session ROOT specifications \label{sec:session-root}\<close> |
48578 | 31 |
|
61503 | 32 |
text \<open>Session specifications reside in files called \<^verbatim>\<open>ROOT\<close> |
48579 | 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 |
|
61477 | 38 |
\<^emph>\<open>outer syntax\<close> of Isabelle/Isar, see also |
58553 | 39 |
@{cite "isabelle-isar-ref"}. This defines common forms like |
48579 | 40 |
identifiers, names, quoted strings, verbatim text, nested comments |
51417 | 41 |
etc. The grammar for @{syntax session_chapter} and @{syntax |
42 |
session_entry} is given as syntax diagram below; each ROOT file may |
|
43 |
contain multiple specifications like this. Chapters help to |
|
44 |
organize browser info (\secref{sec:info}), but have no formal |
|
61493 | 45 |
meaning. The default chapter is ``\<open>Unsorted\<close>''. |
48579 | 46 |
|
58553 | 47 |
Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing |
61503 | 48 |
mode \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is |
51055 | 49 |
enabled by default for any file of that name. |
48579 | 50 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
54705
diff
changeset
|
51 |
@{rail \<open> |
51417 | 52 |
@{syntax_def session_chapter}: @'chapter' @{syntax name} |
53 |
; |
|
54 |
||
48579 | 55 |
@{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body |
56 |
; |
|
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
55112
diff
changeset
|
57 |
body: description? options? (theories+) \<newline> files? (document_files*) |
48579 | 58 |
; |
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48737
diff
changeset
|
59 |
spec: @{syntax name} groups? dir? |
48579 | 60 |
; |
61 |
groups: '(' (@{syntax name} +) ')' |
|
62 |
; |
|
63 |
dir: @'in' @{syntax name} |
|
64 |
; |
|
65 |
description: @'description' @{syntax text} |
|
66 |
; |
|
67 |
options: @'options' opts |
|
68 |
; |
|
48605
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
69 |
opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']' |
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
70 |
; |
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
71 |
value: @{syntax name} | @{syntax real} |
48579 | 72 |
; |
48739 | 73 |
theories: @'theories' opts? ( @{syntax name} * ) |
48579 | 74 |
; |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
55112
diff
changeset
|
75 |
files: @'files' (@{syntax name}+) |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
55112
diff
changeset
|
76 |
; |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
55112
diff
changeset
|
77 |
document_files: @'document_files' ('(' dir ')')? (@{syntax name}+) |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
54705
diff
changeset
|
78 |
\<close>} |
48579 | 79 |
|
61493 | 80 |
\<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new |
81 |
session \<open>A\<close> based on parent session \<open>B\<close>, with its |
|
82 |
content given in \<open>body\<close> (theories and auxiliary source files). |
|
83 |
Note that a parent (like \<open>HOL\<close>) is mandatory in practical |
|
48579 | 84 |
applications: only Isabelle/Pure can bootstrap itself from nothing. |
85 |
||
86 |
All such session specifications together describe a hierarchy (tree) |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48737
diff
changeset
|
87 |
of sessions, with globally unique names. The new session name |
61493 | 88 |
\<open>A\<close> should be sufficiently long and descriptive to stand on |
51055 | 89 |
its own in a potentially large library. |
48579 | 90 |
|
61493 | 91 |
\<^descr> \isakeyword{session}~\<open>A (groups)\<close> indicates a |
48579 | 92 |
collection of groups where the new session is a member. Group names |
93 |
are uninterpreted and merely follow certain conventions. For |
|
94 |
example, the Isabelle distribution tags some important sessions by |
|
61493 | 95 |
the group name called ``\<open>main\<close>''. Other projects may invent |
48604 | 96 |
their own conventions, but this requires some care to avoid clashes |
97 |
within this unchecked name space. |
|
48579 | 98 |
|
61493 | 99 |
\<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close> |
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48737
diff
changeset
|
100 |
specifies an explicit directory for this session; by default this is |
61503 | 101 |
the current directory of the \<^verbatim>\<open>ROOT\<close> file. |
48579 | 102 |
|
103 |
All theories and auxiliary source files are located relatively to |
|
104 |
the session directory. The prover process is run within the same as |
|
105 |
its current working directory. |
|
106 |
||
61493 | 107 |
\<^descr> \isakeyword{description}~\<open>text\<close> is a free-form |
48579 | 108 |
annotation for this session. |
109 |
||
61493 | 110 |
\<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines |
48604 | 111 |
separate options (\secref{sec:system-options}) that are used when |
61477 | 112 |
processing this session, but \<^emph>\<open>without\<close> propagation to child |
61493 | 113 |
sessions. Note that \<open>z\<close> abbreviates \<open>z = true\<close> for |
48604 | 114 |
Boolean options. |
48579 | 115 |
|
61493 | 116 |
\<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a |
48579 | 117 |
block of theories that are processed within an environment that is |
48604 | 118 |
augmented by the given options, in addition to the global session |
119 |
options given before. Any number of blocks of \isakeyword{theories} |
|
120 |
may be given. Options are only active for each |
|
121 |
\isakeyword{theories} block separately. |
|
48579 | 122 |
|
61493 | 123 |
\<^descr> \isakeyword{files}~\<open>files\<close> lists additional source |
48604 | 124 |
files that are involved in the processing of this session. This |
125 |
should cover anything outside the formal content of the theory |
|
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
55112
diff
changeset
|
126 |
sources. In contrast, files that are loaded formally |
58931 | 127 |
within a theory, e.g.\ via @{command "ML_file"}, need not be |
51055 | 128 |
declared again. |
48579 | 129 |
|
61493 | 130 |
\<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists source files for document preparation, |
61503 | 131 |
typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for {\LaTeX}. |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
55112
diff
changeset
|
132 |
Only these explicitly given files are copied from the base directory |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
55112
diff
changeset
|
133 |
to the document output directory, before formal document processing |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
55112
diff
changeset
|
134 |
is started (see also \secref{sec:tool-document}). The local path |
61493 | 135 |
structure of the \<open>files\<close> is preserved, which allows to |
136 |
reconstruct the original directory hierarchy of \<open>base_dir\<close>. |
|
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
55112
diff
changeset
|
137 |
|
61493 | 138 |
\<^descr> \isakeyword{document_files}~\<open>files\<close> abbreviates |
139 |
\isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>document) files\<close>, i.e.\ document sources are taken from the base |
|
61503 | 140 |
directory \<^verbatim>\<open>document\<close> within the session root directory. |
58618 | 141 |
\<close> |
48579 | 142 |
|
51055 | 143 |
|
58618 | 144 |
subsubsection \<open>Examples\<close> |
48580 | 145 |
|
58618 | 146 |
text \<open>See @{file "~~/src/HOL/ROOT"} for a diversity of practically |
51055 | 147 |
relevant situations, although it uses relatively complex |
61493 | 148 |
quasi-hierarchic naming conventions like \<open>HOL\<dash>SPARK\<close>, |
149 |
\<open>HOL\<dash>SPARK\<dash>Examples\<close>. An alternative is to use |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48737
diff
changeset
|
150 |
unqualified names that are relatively long and descriptive, as in |
54704 | 151 |
the Archive of Formal Proofs (@{url "http://afp.sourceforge.net"}), for |
58618 | 152 |
example.\<close> |
48578 | 153 |
|
154 |
||
58618 | 155 |
section \<open>System build options \label{sec:system-options}\<close> |
48578 | 156 |
|
58618 | 157 |
text \<open>See @{file "~~/etc/options"} for the main defaults provided by |
58553 | 158 |
the Isabelle distribution. Isabelle/jEdit @{cite "isabelle-jedit"} |
61503 | 159 |
includes a simple editing mode \<^verbatim>\<open>isabelle-options\<close> for |
48582 | 160 |
this file-format. |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
161 |
|
56604 | 162 |
The following options are particularly relevant to build Isabelle |
51055 | 163 |
sessions, in particular with document preparation |
164 |
(\chref{ch:present}). |
|
165 |
||
61406 | 166 |
\<^item> @{system_option_def "browser_info"} controls output of HTML |
51055 | 167 |
browser info, see also \secref{sec:info}. |
168 |
||
61406 | 169 |
\<^item> @{system_option_def "document"} specifies the document output |
61503 | 170 |
format, see @{tool document} option \<^verbatim>\<open>-o\<close> in |
51055 | 171 |
\secref{sec:tool-document}. In practice, the most relevant values |
61503 | 172 |
are \<^verbatim>\<open>document=false\<close> or \<^verbatim>\<open>document=pdf\<close>. |
51055 | 173 |
|
61406 | 174 |
\<^item> @{system_option_def "document_output"} specifies an |
51055 | 175 |
alternative directory for generated output of the document |
176 |
preparation system; the default is within the @{setting |
|
177 |
"ISABELLE_BROWSER_INFO"} hierarchy as explained in |
|
178 |
\secref{sec:info}. See also @{tool mkroot}, which generates a |
|
179 |
default configuration with output readily available to the author of |
|
180 |
the document. |
|
181 |
||
61406 | 182 |
\<^item> @{system_option_def "document_variants"} specifies document |
61493 | 183 |
variants as a colon-separated list of \<open>name=tags\<close> entries, |
61503 | 184 |
corresponding to @{tool document} options \<^verbatim>\<open>-n\<close> and |
185 |
\<^verbatim>\<open>-t\<close>. |
|
51055 | 186 |
|
61503 | 187 |
For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates |
188 |
two documents: the one called \<^verbatim>\<open>document\<close> with default tags, |
|
189 |
and the other called \<^verbatim>\<open>outline\<close> where proofs and ML |
|
51055 | 190 |
sections are folded. |
191 |
||
192 |
Document variant names are just a matter of conventions. It is also |
|
193 |
possible to use different document variant names (without tags) for |
|
194 |
different document root entries, see also |
|
195 |
\secref{sec:tool-document}. |
|
196 |
||
61406 | 197 |
\<^item> @{system_option_def "threads"} determines the number of worker |
51055 | 198 |
threads for parallel checking of theories and proofs. The default |
61493 | 199 |
\<open>0\<close> means that a sensible maximum value is determined by the |
51055 | 200 |
underlying hardware. For machines with many cores or with |
201 |
hyperthreading, this is often requires manual adjustment (on the |
|
202 |
command-line or within personal settings or preferences, not within |
|
61503 | 203 |
a session \<^verbatim>\<open>ROOT\<close>). |
51055 | 204 |
|
61406 | 205 |
\<^item> @{system_option_def "condition"} specifies a comma-separated |
51055 | 206 |
list of process environment variables (or Isabelle settings) that |
207 |
are required for the subsequent theories to be processed. |
|
208 |
Conditions are considered ``true'' if the corresponding environment |
|
209 |
value is defined and non-empty. |
|
210 |
||
61503 | 211 |
For example, the \<^verbatim>\<open>condition=ISABELLE_FULL_TEST\<close> may be |
51055 | 212 |
used to guard extraordinary theories, which are meant to be enabled |
61503 | 213 |
explicitly via some shell prefix \<^verbatim>\<open>env ISABELLE_FULL_TEST=true\<close> |
51055 | 214 |
before invoking @{tool build}. |
215 |
||
61406 | 216 |
\<^item> @{system_option_def "timeout"} specifies a real wall-clock |
51055 | 217 |
timeout (in seconds) for the session as a whole. The timer is |
218 |
controlled outside the ML process by the JVM that runs |
|
219 |
Isabelle/Scala. Thus it is relatively reliable in canceling |
|
220 |
processes that get out of control, even if there is a deadlock |
|
221 |
without CPU time usage. |
|
222 |
||
223 |
||
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
224 |
The @{tool_def options} tool prints Isabelle system options. Its |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
225 |
command-line usage is: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
226 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
227 |
\<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...] |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
228 |
|
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
229 |
Options are: |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
230 |
-b include $ISABELLE_BUILD_OPTIONS |
52735 | 231 |
-g OPTION get value of OPTION |
50531
f841ac0cb757
clarified "isabelle options" command line, to make it more close to "isabelle components";
wenzelm
parents:
50406
diff
changeset
|
232 |
-l list options |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
233 |
-x FILE export to FILE in YXML format |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
234 |
|
50531
f841ac0cb757
clarified "isabelle options" command line, to make it more close to "isabelle components";
wenzelm
parents:
50406
diff
changeset
|
235 |
Report Isabelle system options, augmented by MORE_OPTIONS given as |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
236 |
arguments NAME=VAL or NAME.\<close>} |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
237 |
|
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
238 |
The command line arguments provide additional system options of the |
61503 | 239 |
form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
240 |
for Boolean options. |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
241 |
|
61503 | 242 |
Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
243 |
options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
244 |
\secref{sec:tool-build}. |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
245 |
|
61503 | 246 |
Option \<^verbatim>\<open>-g\<close> prints the value of the given option. |
247 |
Option \<^verbatim>\<open>-l\<close> lists all options with their declaration and |
|
54347 | 248 |
current value. |
52735 | 249 |
|
61503 | 250 |
Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
251 |
YXML format, instead of printing it in human-readable form. |
58618 | 252 |
\<close> |
48578 | 253 |
|
254 |
||
58618 | 255 |
section \<open>Invoking the build process \label{sec:tool-build}\<close> |
48578 | 256 |
|
58618 | 257 |
text \<open>The @{tool_def build} tool invokes the build process for |
48578 | 258 |
Isabelle sessions. It manages dependencies between sessions, |
259 |
related sources of theories and auxiliary files, and target heap |
|
260 |
images. Accordingly, it runs instances of the prover process with |
|
261 |
optional document preparation. Its command-line usage |
|
262 |
is:\footnote{Isabelle/Scala provides the same functionality via |
|
61503 | 263 |
\<^verbatim>\<open>isabelle.Build.build\<close>.} |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
264 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
265 |
\<open>Usage: isabelle build [OPTIONS] [SESSIONS ...] |
48578 | 266 |
|
267 |
Options are: |
|
48737
f3bbb9ca57d6
added build option -D: include session directory and select its sessions;
wenzelm
parents:
48693
diff
changeset
|
268 |
-D DIR include session directory and select its sessions |
49131 | 269 |
-R operate on requirements of selected sessions |
60106 | 270 |
-X NAME exclude sessions from group NAME and all descendants |
48578 | 271 |
-a select all sessions |
272 |
-b build heap images |
|
48595 | 273 |
-c clean build |
48737
f3bbb9ca57d6
added build option -D: include session directory and select its sessions;
wenzelm
parents:
48693
diff
changeset
|
274 |
-d DIR include session directory |
48578 | 275 |
-g NAME select session group NAME |
276 |
-j INT maximum number of parallel jobs (default 1) |
|
59891
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59446
diff
changeset
|
277 |
-k KEYWORD check theory sources for conflicts with proposed keywords |
48903 | 278 |
-l list session source files |
48578 | 279 |
-n no build -- test dependencies only |
52056 | 280 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
48578 | 281 |
-s system build mode: produce output in ISABELLE_HOME |
282 |
-v verbose |
|
60106 | 283 |
-x NAME exclude session NAME and all descendants |
48578 | 284 |
|
285 |
Build and manage Isabelle sessions, depending on implicit |
|
286 |
ISABELLE_BUILD_OPTIONS="..." |
|
287 |
||
288 |
ML_PLATFORM="..." |
|
289 |
ML_HOME="..." |
|
290 |
ML_SYSTEM="..." |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
291 |
ML_OPTIONS="..."\<close>} |
48578 | 292 |
|
61406 | 293 |
\<^medskip> |
294 |
Isabelle sessions are defined via session ROOT files as |
|
48578 | 295 |
described in (\secref{sec:session-root}). The totality of sessions |
296 |
is determined by collecting such specifications from all Isabelle |
|
297 |
component directories (\secref{sec:components}), augmented by more |
|
61503 | 298 |
directories given via options \<^verbatim>\<open>-d\<close>~\<open>DIR\<close> on the |
48578 | 299 |
command line. Each such directory may contain a session |
61503 | 300 |
\<^verbatim>\<open>ROOT\<close> file with several session specifications. |
48578 | 301 |
|
48684
9170e10c651e
re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
wenzelm
parents:
48683
diff
changeset
|
302 |
Any session root directory may refer recursively to further |
9170e10c651e
re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
wenzelm
parents:
48683
diff
changeset
|
303 |
directories of the same kind, by listing them in a catalog file |
61503 | 304 |
\<^verbatim>\<open>ROOTS\<close> line-by-line. This helps to organize large |
305 |
collections of session specifications, or to make \<^verbatim>\<open>-d\<close> |
|
306 |
command line options persistent (say within |
|
307 |
\<^verbatim>\<open>$ISABELLE_HOME_USER/ROOTS\<close>). |
|
48684
9170e10c651e
re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
wenzelm
parents:
48683
diff
changeset
|
308 |
|
61406 | 309 |
\<^medskip> |
310 |
The subset of sessions to be managed is determined via |
|
61493 | 311 |
individual \<open>SESSIONS\<close> given as command-line arguments, or |
61503 | 312 |
session groups that are given via one or more options \<^verbatim>\<open>-g\<close>~\<open>NAME\<close>. |
313 |
Option \<^verbatim>\<open>-a\<close> selects all sessions. |
|
48604 | 314 |
The build tool takes session dependencies into account: the set of |
315 |
selected sessions is completed by including all ancestors. |
|
48578 | 316 |
|
61406 | 317 |
\<^medskip> |
61503 | 318 |
One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify |
59892
2a616319c171
added isabelle build option -x, to exclude sessions;
wenzelm
parents:
59891
diff
changeset
|
319 |
sessions to be excluded. All descendents of excluded sessions are removed |
61503 | 320 |
from the selection as specified above. Option \<^verbatim>\<open>-X\<close> is |
60106 | 321 |
analogous to this, but excluded sessions are specified by session group |
322 |
membership. |
|
59892
2a616319c171
added isabelle build option -x, to exclude sessions;
wenzelm
parents:
59891
diff
changeset
|
323 |
|
61406 | 324 |
\<^medskip> |
61503 | 325 |
Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense |
49131 | 326 |
that it refers to its requirements: all ancestor sessions excluding |
327 |
the original selection. This allows to prepare the stage for some |
|
328 |
build process with different options, before running the main build |
|
61503 | 329 |
itself (without option \<^verbatim>\<open>-R\<close>). |
49131 | 330 |
|
61406 | 331 |
\<^medskip> |
61503 | 332 |
Option \<^verbatim>\<open>-D\<close> is similar to \<^verbatim>\<open>-d\<close>, but |
48737
f3bbb9ca57d6
added build option -D: include session directory and select its sessions;
wenzelm
parents:
48693
diff
changeset
|
333 |
selects all sessions that are defined in the given directories. |
f3bbb9ca57d6
added build option -D: include session directory and select its sessions;
wenzelm
parents:
48693
diff
changeset
|
334 |
|
61406 | 335 |
\<^medskip> |
336 |
The build process depends on additional options |
|
48604 | 337 |
(\secref{sec:system-options}) that are passed to the prover |
338 |
eventually. The settings variable @{setting_ref |
|
339 |
ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\ |
|
61503 | 340 |
\<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>. Moreover, |
48604 | 341 |
the environment of system build options may be augmented on the |
61503 | 342 |
command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>, which |
343 |
abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for |
|
344 |
Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on the |
|
48604 | 345 |
command-line are applied in the given order. |
48578 | 346 |
|
61406 | 347 |
\<^medskip> |
61503 | 348 |
Option \<^verbatim>\<open>-b\<close> ensures that heap images are |
48578 | 349 |
produced for all selected sessions. By default, images are only |
350 |
saved for inner nodes of the hierarchy of sessions, as required for |
|
351 |
other sessions to continue later on. |
|
352 |
||
61406 | 353 |
\<^medskip> |
61503 | 354 |
Option \<^verbatim>\<open>-c\<close> cleans all descendants of the |
48595 | 355 |
selected sessions before performing the specified build operation. |
356 |
||
61406 | 357 |
\<^medskip> |
61503 | 358 |
Option \<^verbatim>\<open>-n\<close> omits the actual build process |
48595 | 359 |
after the preparatory stage (including optional cleanup). Note that |
360 |
the return code always indicates the status of the set of selected |
|
361 |
sessions. |
|
362 |
||
61406 | 363 |
\<^medskip> |
61503 | 364 |
Option \<^verbatim>\<open>-j\<close> specifies the maximum number of |
48604 | 365 |
parallel build jobs (prover processes). Each prover process is |
366 |
subject to a separate limit of parallel worker threads, cf.\ system |
|
367 |
option @{system_option_ref threads}. |
|
48578 | 368 |
|
61406 | 369 |
\<^medskip> |
61503 | 370 |
Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which |
48578 | 371 |
means that resulting heap images and log files are stored in |
54705 | 372 |
@{file_unchecked "$ISABELLE_HOME/heaps"} instead of the default location |
48578 | 373 |
@{setting ISABELLE_OUTPUT} (which is normally in @{setting |
374 |
ISABELLE_HOME_USER}, i.e.\ the user's home directory). |
|
375 |
||
61406 | 376 |
\<^medskip> |
61503 | 377 |
Option \<^verbatim>\<open>-v\<close> increases the general level of |
378 |
verbosity. Option \<^verbatim>\<open>-l\<close> lists the source files that |
|
48903 | 379 |
contribute to a session. |
59891
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59446
diff
changeset
|
380 |
|
61406 | 381 |
\<^medskip> |
61503 | 382 |
Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for |
59891
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59446
diff
changeset
|
383 |
outer syntax (multiple uses allowed). The theory sources are checked for |
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59446
diff
changeset
|
384 |
conflicts wrt.\ this hypothetical change of syntax, e.g.\ to reveal |
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59446
diff
changeset
|
385 |
occurrences of identifiers that need to be quoted.\<close> |
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59446
diff
changeset
|
386 |
|
48578 | 387 |
|
58618 | 388 |
subsubsection \<open>Examples\<close> |
48578 | 389 |
|
58618 | 390 |
text \<open> |
48578 | 391 |
Build a specific logic image: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
392 |
@{verbatim [display] \<open>isabelle build -b HOLCF\<close>} |
48578 | 393 |
|
61406 | 394 |
\<^smallskip> |
395 |
Build the main group of logic images: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
396 |
@{verbatim [display] \<open>isabelle build -b -g main\<close>} |
48578 | 397 |
|
61406 | 398 |
\<^smallskip> |
399 |
Provide a general overview of the status of all Isabelle |
|
48595 | 400 |
sessions, without building anything: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
401 |
@{verbatim [display] \<open>isabelle build -a -n -v\<close>} |
48578 | 402 |
|
61406 | 403 |
\<^smallskip> |
404 |
Build all sessions with HTML browser info and PDF |
|
48595 | 405 |
document preparation: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
406 |
@{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>} |
48578 | 407 |
|
61406 | 408 |
\<^smallskip> |
409 |
Build all sessions with a maximum of 8 parallel prover |
|
48604 | 410 |
processes and 4 worker threads each (on a machine with many cores): |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
411 |
@{verbatim [display] \<open>isabelle build -a -j8 -o threads=4\<close>} |
48595 | 412 |
|
61406 | 413 |
\<^smallskip> |
414 |
Build some session images with cleanup of their |
|
48595 | 415 |
descendants, while retaining their ancestry: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
416 |
@{verbatim [display] \<open>isabelle build -b -c HOL-Algebra HOL-Word\<close>} |
48595 | 417 |
|
61406 | 418 |
\<^smallskip> |
419 |
Clean all sessions without building anything: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
420 |
@{verbatim [display] \<open>isabelle build -a -n -c\<close>} |
48737
f3bbb9ca57d6
added build option -D: include session directory and select its sessions;
wenzelm
parents:
48693
diff
changeset
|
421 |
|
61406 | 422 |
\<^smallskip> |
423 |
Build all sessions from some other directory hierarchy, |
|
61503 | 424 |
according to the settings variable \<^verbatim>\<open>AFP\<close> that happens to |
48737
f3bbb9ca57d6
added build option -D: include session directory and select its sessions;
wenzelm
parents:
48693
diff
changeset
|
425 |
be defined inside the Isabelle environment: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
426 |
@{verbatim [display] \<open>isabelle build -D '$AFP'\<close>} |
49131 | 427 |
|
61406 | 428 |
\<^smallskip> |
429 |
Inform about the status of all sessions required for AFP, |
|
49131 | 430 |
without building anything yet: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
431 |
@{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>} |
58618 | 432 |
\<close> |
48578 | 433 |
|
434 |
end |