author | wenzelm |
Wed, 25 Oct 2017 13:47:53 +0200 | |
changeset 66916 | aca50a1572c5 |
parent 66851 | c75769065548 |
child 66970 | 13857f49d215 |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
61575 | 2 |
|
48578 | 3 |
theory Sessions |
4 |
imports Base |
|
5 |
begin |
|
6 |
||
58618 | 7 |
chapter \<open>Isabelle sessions and build management \label{ch:session}\<close> |
48584 | 8 |
|
61575 | 9 |
text \<open> |
10 |
An Isabelle \<^emph>\<open>session\<close> consists of a collection of related theories that may |
|
11 |
be associated with formal documents (\chref{ch:present}). There is also a |
|
12 |
notion of \<^emph>\<open>persistent heap\<close> image to capture the state of a session, |
|
13 |
similar to object-code in compiled programming languages. Thus the concept |
|
14 |
of session resembles that of a ``project'' in common IDE environments, but |
|
15 |
the specific name emphasizes the connection to interactive theorem proving: |
|
16 |
the session wraps-up the results of user-interaction with the prover in a |
|
17 |
persistent form. |
|
48584 | 18 |
|
61575 | 19 |
Application sessions are built on a given parent session, which may be built |
20 |
recursively on other parents. Following this path in the hierarchy |
|
21 |
eventually leads to some major object-logic session like \<open>HOL\<close>, which itself |
|
22 |
is based on \<open>Pure\<close> as the common root of all sessions. |
|
48584 | 23 |
|
61575 | 24 |
Processing sessions may take considerable time. Isabelle build management |
25 |
helps to organize this efficiently. This includes support for parallel build |
|
26 |
jobs, in addition to the multithreaded theory and proof checking that is |
|
27 |
already provided by the prover process itself. |
|
28 |
\<close> |
|
48604 | 29 |
|
48578 | 30 |
|
58618 | 31 |
section \<open>Session ROOT specifications \label{sec:session-root}\<close> |
48578 | 32 |
|
61575 | 33 |
text \<open> |
34 |
Session specifications reside in files called \<^verbatim>\<open>ROOT\<close> within certain |
|
35 |
directories, such as the home locations of registered Isabelle components or |
|
36 |
additional project directories given by the user. |
|
48579 | 37 |
|
61575 | 38 |
The ROOT file format follows the lexical conventions of the \<^emph>\<open>outer syntax\<close> |
39 |
of Isabelle/Isar, see also @{cite "isabelle-isar-ref"}. This defines common |
|
40 |
forms like identifiers, names, quoted strings, verbatim text, nested |
|
41 |
comments etc. The grammar for @{syntax session_chapter} and @{syntax |
|
42 |
session_entry} is given as syntax diagram below; each ROOT file may contain |
|
43 |
multiple specifications like this. Chapters help to organize browser info |
|
44 |
(\secref{sec:info}), but have no formal meaning. The default chapter is |
|
45 |
``\<open>Unsorted\<close>''. |
|
48579 | 46 |
|
61575 | 47 |
Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode |
48 |
\<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any |
|
49 |
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 |
||
66916 | 55 |
@{syntax_def session_entry}: @'session' spec '=' |
56 |
(@{syntax system_name} '+')? body |
|
48579 | 57 |
; |
66759 | 58 |
body: description? options? (theories+) \<newline> (document_files*) |
48579 | 59 |
; |
66916 | 60 |
spec: @{syntax system_name} groups? dir? |
48579 | 61 |
; |
62 |
groups: '(' (@{syntax name} +) ')' |
|
63 |
; |
|
64 |
dir: @'in' @{syntax name} |
|
65 |
; |
|
66 |
description: @'description' @{syntax text} |
|
67 |
; |
|
68 |
options: @'options' opts |
|
69 |
; |
|
48605
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
70 |
opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']' |
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
71 |
; |
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
72 |
value: @{syntax name} | @{syntax real} |
48579 | 73 |
; |
66916 | 74 |
sessions: @'sessions' (@{syntax system_name}+) |
65374 | 75 |
; |
76 |
theories: @'theories' opts? (theory_entry*) |
|
48579 | 77 |
; |
66916 | 78 |
theory_entry: @{syntax system_name} ('(' @'global' ')')? |
65504 | 79 |
; |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
55112
diff
changeset
|
80 |
document_files: @'document_files' ('(' dir ')')? (@{syntax name}+) |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
54705
diff
changeset
|
81 |
\<close>} |
48579 | 82 |
|
61575 | 83 |
\<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on |
66759 | 84 |
parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and |
85 |
theories). Note that a parent (like \<open>HOL\<close>) is mandatory in practical |
|
86 |
applications: only Isabelle/Pure can bootstrap itself from nothing. |
|
48579 | 87 |
|
65504 | 88 |
All such session specifications together describe a hierarchy (graph) of |
61575 | 89 |
sessions, with globally unique names. The new session name \<open>A\<close> should be |
90 |
sufficiently long and descriptive to stand on its own in a potentially large |
|
91 |
library. |
|
48579 | 92 |
|
61575 | 93 |
\<^descr> \isakeyword{session}~\<open>A (groups)\<close> indicates a collection of groups where |
94 |
the new session is a member. Group names are uninterpreted and merely follow |
|
95 |
certain conventions. For example, the Isabelle distribution tags some |
|
96 |
important sessions by the group name called ``\<open>main\<close>''. Other projects may |
|
97 |
invent their own conventions, but this requires some care to avoid clashes |
|
48604 | 98 |
within this unchecked name space. |
48579 | 99 |
|
61575 | 100 |
\<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close> specifies an explicit |
101 |
directory for this session; by default this is the current directory of the |
|
102 |
\<^verbatim>\<open>ROOT\<close> file. |
|
48579 | 103 |
|
66759 | 104 |
All theory files are located relatively to the session directory. The prover |
105 |
process is run within the same as its current working directory. |
|
48579 | 106 |
|
61575 | 107 |
\<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this |
108 |
session. |
|
48579 | 109 |
|
61575 | 110 |
\<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options |
111 |
(\secref{sec:system-options}) that are used when processing this session, |
|
112 |
but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z = |
|
113 |
true\<close> for Boolean options. |
|
114 |
||
65504 | 115 |
\<^descr> \isakeyword{sessions}~\<open>names\<close> specifies sessions that are \<^emph>\<open>imported\<close> into |
116 |
the current name space of theories. This allows to refer to a theory \<open>A\<close> |
|
117 |
from session \<open>B\<close> by the qualified name \<open>B.A\<close> --- although it is loaded again |
|
118 |
into the current ML process, which is in contrast to a theory that is |
|
119 |
already present in the \<^emph>\<open>parent\<close> session. |
|
120 |
||
65505 | 121 |
Theories that are imported from other sessions are excluded from the current |
122 |
session document. |
|
123 |
||
61575 | 124 |
\<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that |
125 |
are processed within an environment that is augmented by the given options, |
|
126 |
in addition to the global session options given before. Any number of blocks |
|
127 |
of \isakeyword{theories} may be given. Options are only active for each |
|
48604 | 128 |
\isakeyword{theories} block separately. |
48579 | 129 |
|
65374 | 130 |
A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated |
131 |
literally in other session specifications or theory imports. In contrast, |
|
132 |
the default is to qualify theory names by the session name, in order to |
|
65504 | 133 |
ensure globally unique names in big session graphs. |
65374 | 134 |
|
61575 | 135 |
\<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists |
136 |
source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for |
|
137 |
{\LaTeX}. Only these explicitly given files are copied from the base |
|
138 |
directory to the document output directory, before formal document |
|
139 |
processing is started (see also \secref{sec:tool-document}). The local path |
|
140 |
structure of the \<open>files\<close> is preserved, which allows to reconstruct the |
|
141 |
original directory hierarchy of \<open>base_dir\<close>. |
|
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
55112
diff
changeset
|
142 |
|
61493 | 143 |
\<^descr> \isakeyword{document_files}~\<open>files\<close> abbreviates |
61575 | 144 |
\isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>document) files\<close>, i.e.\ |
145 |
document sources are taken from the base directory \<^verbatim>\<open>document\<close> within the |
|
146 |
session root directory. |
|
58618 | 147 |
\<close> |
48579 | 148 |
|
51055 | 149 |
|
58618 | 150 |
subsubsection \<open>Examples\<close> |
48580 | 151 |
|
61575 | 152 |
text \<open> |
63680 | 153 |
See \<^file>\<open>~~/src/HOL/ROOT\<close> for a diversity of practically relevant situations, |
154 |
although it uses relatively complex quasi-hierarchic naming conventions like |
|
155 |
\<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified |
|
156 |
names that are relatively long and descriptive, as in the Archive of Formal |
|
157 |
Proofs (\<^url>\<open>http://afp.sourceforge.net\<close>), for example. |
|
61575 | 158 |
\<close> |
48578 | 159 |
|
160 |
||
58618 | 161 |
section \<open>System build options \label{sec:system-options}\<close> |
48578 | 162 |
|
61575 | 163 |
text \<open> |
63680 | 164 |
See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle |
61575 | 165 |
distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple |
166 |
editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format. |
|
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
167 |
|
61575 | 168 |
The following options are particularly relevant to build Isabelle sessions, |
169 |
in particular with document preparation (\chref{ch:present}). |
|
51055 | 170 |
|
61575 | 171 |
\<^item> @{system_option_def "browser_info"} controls output of HTML browser |
172 |
info, see also \secref{sec:info}. |
|
51055 | 173 |
|
61575 | 174 |
\<^item> @{system_option_def "document"} specifies the document output format, |
175 |
see @{tool document} option \<^verbatim>\<open>-o\<close> in \secref{sec:tool-document}. In |
|
176 |
practice, the most relevant values are \<^verbatim>\<open>document=false\<close> or |
|
177 |
\<^verbatim>\<open>document=pdf\<close>. |
|
51055 | 178 |
|
61575 | 179 |
\<^item> @{system_option_def "document_output"} specifies an alternative |
180 |
directory for generated output of the document preparation system; the |
|
181 |
default is within the @{setting "ISABELLE_BROWSER_INFO"} hierarchy as |
|
182 |
explained in \secref{sec:info}. See also @{tool mkroot}, which generates a |
|
183 |
default configuration with output readily available to the author of the |
|
184 |
document. |
|
51055 | 185 |
|
61575 | 186 |
\<^item> @{system_option_def "document_variants"} specifies document variants as |
187 |
a colon-separated list of \<open>name=tags\<close> entries, corresponding to @{tool |
|
188 |
document} options \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-t\<close>. |
|
51055 | 189 |
|
61575 | 190 |
For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates |
191 |
two documents: the one called \<^verbatim>\<open>document\<close> with default tags, and the other |
|
192 |
called \<^verbatim>\<open>outline\<close> where proofs and ML sections are folded. |
|
51055 | 193 |
|
61575 | 194 |
Document variant names are just a matter of conventions. It is also |
195 |
possible to use different document variant names (without tags) for |
|
196 |
different document root entries, see also \secref{sec:tool-document}. |
|
51055 | 197 |
|
61575 | 198 |
\<^item> @{system_option_def "threads"} determines the number of worker threads |
199 |
for parallel checking of theories and proofs. The default \<open>0\<close> means that a |
|
200 |
sensible maximum value is determined by the underlying hardware. For |
|
201 |
machines with many cores or with hyperthreading, this is often requires |
|
202 |
manual adjustment (on the command-line or within personal settings or |
|
203 |
preferences, not within a session \<^verbatim>\<open>ROOT\<close>). |
|
51055 | 204 |
|
63827
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
63680
diff
changeset
|
205 |
\<^item> @{system_option_def "checkpoint"} helps to fine-tune the global heap |
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
63680
diff
changeset
|
206 |
space management. This is relevant for big sessions that may exhaust the |
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
63680
diff
changeset
|
207 |
small 32-bit address space of the ML process (which is used by default). |
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
63680
diff
changeset
|
208 |
When the option is enabled for some \isakeyword{theories} block, a full |
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
63680
diff
changeset
|
209 |
sharing stage of immutable values in memory happens \<^emph>\<open>before\<close> loading the |
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
63680
diff
changeset
|
210 |
specified theories. |
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
63680
diff
changeset
|
211 |
|
61575 | 212 |
\<^item> @{system_option_def "condition"} specifies a comma-separated list of |
213 |
process environment variables (or Isabelle settings) that are required for |
|
214 |
the subsequent theories to be processed. Conditions are considered |
|
215 |
``true'' if the corresponding environment value is defined and non-empty. |
|
51055 | 216 |
|
61602 | 217 |
\<^item> @{system_option_def "timeout"} and @{system_option_def "timeout_scale"} |
218 |
specify a real wall-clock timeout for the session as a whole: the two |
|
219 |
values are multiplied and taken as the number of seconds. Typically, |
|
220 |
@{system_option "timeout"} is given for individual sessions, and |
|
221 |
@{system_option "timeout_scale"} as global adjustment to overall hardware |
|
222 |
performance. |
|
223 |
||
224 |
The timer is controlled outside the ML process by the JVM that runs |
|
225 |
Isabelle/Scala. Thus it is relatively reliable in canceling processes that |
|
226 |
get out of control, even if there is a deadlock without CPU time usage. |
|
51055 | 227 |
|
64308 | 228 |
\<^item> @{system_option_def "profiling"} specifies a mode for global ML |
229 |
profiling. Possible values are the empty string (disabled), \<^verbatim>\<open>time\<close> for |
|
230 |
@{ML profile_time} and \<^verbatim>\<open>allocations\<close> for @{ML profile_allocations}. |
|
231 |
Results appear near the bottom of the session log file. |
|
232 |
||
61575 | 233 |
The @{tool_def options} tool prints Isabelle system options. Its |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
234 |
command-line usage is: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
235 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
236 |
\<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...] |
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 |
Options are: |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
239 |
-b include $ISABELLE_BUILD_OPTIONS |
52735 | 240 |
-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
|
241 |
-l list options |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
242 |
-x FILE export to FILE in YXML format |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
243 |
|
50531
f841ac0cb757
clarified "isabelle options" command line, to make it more close to "isabelle components";
wenzelm
parents:
50406
diff
changeset
|
244 |
Report Isabelle system options, augmented by MORE_OPTIONS given as |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
245 |
arguments NAME=VAL or NAME.\<close>} |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
246 |
|
61575 | 247 |
The command line arguments provide additional system options of the form |
248 |
\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> for Boolean options. |
|
249 |
||
250 |
Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system options by the ones |
|
251 |
of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}. |
|
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
252 |
|
61575 | 253 |
Option \<^verbatim>\<open>-g\<close> prints the value of the given option. Option \<^verbatim>\<open>-l\<close> lists all |
254 |
options with their declaration and current value. |
|
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
255 |
|
61575 | 256 |
Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in YXML format, instead |
257 |
of printing it in human-readable form. |
|
58618 | 258 |
\<close> |
48578 | 259 |
|
260 |
||
58618 | 261 |
section \<open>Invoking the build process \label{sec:tool-build}\<close> |
48578 | 262 |
|
61575 | 263 |
text \<open> |
264 |
The @{tool_def build} tool invokes the build process for Isabelle sessions. |
|
265 |
It manages dependencies between sessions, related sources of theories and |
|
266 |
auxiliary files, and target heap images. Accordingly, it runs instances of |
|
267 |
the prover process with optional document preparation. Its command-line |
|
268 |
usage is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via |
|
61572 | 269 |
\<^verbatim>\<open>isabelle.Build.build\<close>.\<close> |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
270 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
271 |
\<open>Usage: isabelle build [OPTIONS] [SESSIONS ...] |
48578 | 272 |
|
273 |
Options are: |
|
66737
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66671
diff
changeset
|
274 |
-B NAME include session NAME and all descendants |
48737
f3bbb9ca57d6
added build option -D: include session directory and select its sessions;
wenzelm
parents:
48693
diff
changeset
|
275 |
-D DIR include session directory and select its sessions |
64265 | 276 |
-N cyclic shuffling of NUMA CPU nodes (performance tuning) |
49131 | 277 |
-R operate on requirements of selected sessions |
66745 | 278 |
-S soft build: only observe changes of sources, not heap images |
60106 | 279 |
-X NAME exclude sessions from group NAME and all descendants |
48578 | 280 |
-a select all sessions |
281 |
-b build heap images |
|
48595 | 282 |
-c clean build |
48737
f3bbb9ca57d6
added build option -D: include session directory and select its sessions;
wenzelm
parents:
48693
diff
changeset
|
283 |
-d DIR include session directory |
66841 | 284 |
-f fresh build |
48578 | 285 |
-g NAME select session group NAME |
286 |
-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
|
287 |
-k KEYWORD check theory sources for conflicts with proposed keywords |
48903 | 288 |
-l list session source files |
48578 | 289 |
-n no build -- test dependencies only |
52056 | 290 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
48578 | 291 |
-s system build mode: produce output in ISABELLE_HOME |
292 |
-v verbose |
|
60106 | 293 |
-x NAME exclude session NAME and all descendants |
48578 | 294 |
|
62596 | 295 |
Build and manage Isabelle sessions, depending on implicit settings: |
296 |
||
48578 | 297 |
ISABELLE_BUILD_OPTIONS="..." |
298 |
||
299 |
ML_PLATFORM="..." |
|
300 |
ML_HOME="..." |
|
301 |
ML_SYSTEM="..." |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
302 |
ML_OPTIONS="..."\<close>} |
48578 | 303 |
|
61406 | 304 |
\<^medskip> |
61575 | 305 |
Isabelle sessions are defined via session ROOT files as described in |
306 |
(\secref{sec:session-root}). The totality of sessions is determined by |
|
307 |
collecting such specifications from all Isabelle component directories |
|
308 |
(\secref{sec:components}), augmented by more directories given via options |
|
309 |
\<^verbatim>\<open>-d\<close>~\<open>DIR\<close> on the command line. Each such directory may contain a session |
|
61503 | 310 |
\<^verbatim>\<open>ROOT\<close> file with several session specifications. |
48578 | 311 |
|
61575 | 312 |
Any session root directory may refer recursively to further directories of |
313 |
the same kind, by listing them in a catalog file \<^verbatim>\<open>ROOTS\<close> line-by-line. This |
|
314 |
helps to organize large collections of session specifications, or to make |
|
66576 | 315 |
\<^verbatim>\<open>-d\<close> command line options persistent (e.g.\ in |
61503 | 316 |
\<^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
|
317 |
|
61406 | 318 |
\<^medskip> |
61575 | 319 |
The subset of sessions to be managed is determined via individual \<open>SESSIONS\<close> |
320 |
given as command-line arguments, or session groups that are given via one or |
|
321 |
more options \<^verbatim>\<open>-g\<close>~\<open>NAME\<close>. Option \<^verbatim>\<open>-a\<close> selects all sessions. The build tool |
|
322 |
takes session dependencies into account: the set of selected sessions is |
|
323 |
completed by including all ancestors. |
|
48578 | 324 |
|
61406 | 325 |
\<^medskip> |
66737
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66671
diff
changeset
|
326 |
One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions. All descendants |
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66671
diff
changeset
|
327 |
are included. |
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66671
diff
changeset
|
328 |
|
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66671
diff
changeset
|
329 |
\<^medskip> |
61575 | 330 |
One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded. All |
331 |
descendents of excluded sessions are removed from the selection as specified |
|
332 |
above. Option \<^verbatim>\<open>-X\<close> is analogous to this, but excluded sessions are |
|
333 |
specified by session group membership. |
|
59892
2a616319c171
added isabelle build option -x, to exclude sessions;
wenzelm
parents:
59891
diff
changeset
|
334 |
|
61406 | 335 |
\<^medskip> |
61575 | 336 |
Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense that it refers to its |
337 |
requirements: all ancestor sessions excluding the original selection. This |
|
338 |
allows to prepare the stage for some build process with different options, |
|
339 |
before running the main build itself (without option \<^verbatim>\<open>-R\<close>). |
|
49131 | 340 |
|
61406 | 341 |
\<^medskip> |
61575 | 342 |
Option \<^verbatim>\<open>-D\<close> is similar to \<^verbatim>\<open>-d\<close>, but selects all sessions that are defined |
343 |
in the given directories. |
|
48737
f3bbb9ca57d6
added build option -D: include session directory and select its sessions;
wenzelm
parents:
48693
diff
changeset
|
344 |
|
61406 | 345 |
\<^medskip> |
66745 | 346 |
Option \<^verbatim>\<open>-S\<close> indicates a ``soft build'': the selection is restricted to |
347 |
those sessions that have changed sources (according to actually imported |
|
348 |
theories). The status of heap images is ignored. |
|
349 |
||
350 |
\<^medskip> |
|
61406 | 351 |
The build process depends on additional options |
61575 | 352 |
(\secref{sec:system-options}) that are passed to the prover eventually. The |
353 |
settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide |
|
61602 | 354 |
additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>. |
355 |
Moreover, the environment of system build options may be augmented on the |
|
356 |
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 abbreviates |
|
357 |
\<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on |
|
358 |
the command-line are applied in the given order. |
|
48578 | 359 |
|
61406 | 360 |
\<^medskip> |
61575 | 361 |
Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected |
362 |
sessions. By default, images are only saved for inner nodes of the hierarchy |
|
363 |
of sessions, as required for other sessions to continue later on. |
|
48578 | 364 |
|
61406 | 365 |
\<^medskip> |
61575 | 366 |
Option \<^verbatim>\<open>-c\<close> cleans all descendants of the selected sessions before |
367 |
performing the specified build operation. |
|
48595 | 368 |
|
61406 | 369 |
\<^medskip> |
66841 | 370 |
Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their |
371 |
requirements. |
|
372 |
||
373 |
\<^medskip> |
|
61575 | 374 |
Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage |
375 |
(including optional cleanup). Note that the return code always indicates the |
|
376 |
status of the set of selected sessions. |
|
48595 | 377 |
|
61406 | 378 |
\<^medskip> |
61575 | 379 |
Option \<^verbatim>\<open>-j\<close> specifies the maximum number of parallel build jobs (prover |
380 |
processes). Each prover process is subject to a separate limit of parallel |
|
381 |
worker threads, cf.\ system option @{system_option_ref threads}. |
|
48578 | 382 |
|
61406 | 383 |
\<^medskip> |
64265 | 384 |
Option \<^verbatim>\<open>-N\<close> enables cyclic shuffling of NUMA CPU nodes. This may help |
385 |
performance tuning on Linux servers with separate CPU/memory modules. |
|
386 |
||
387 |
\<^medskip> |
|
61575 | 388 |
Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that resulting heap images |
63669 | 389 |
and log files are stored in @{path "$ISABELLE_HOME/heaps"} instead of the |
390 |
default location @{setting ISABELLE_OUTPUT} (which is normally in @{setting |
|
391 |
ISABELLE_HOME_USER}, i.e.\ the user's home directory). |
|
48578 | 392 |
|
61406 | 393 |
\<^medskip> |
61575 | 394 |
Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists |
395 |
the source files that contribute to a session. |
|
59891
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59446
diff
changeset
|
396 |
|
61406 | 397 |
\<^medskip> |
61575 | 398 |
Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax (multiple |
399 |
uses allowed). The theory sources are checked for conflicts wrt.\ this |
|
400 |
hypothetical change of syntax, e.g.\ to reveal occurrences of identifiers |
|
401 |
that need to be quoted. |
|
402 |
\<close> |
|
59891
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59446
diff
changeset
|
403 |
|
48578 | 404 |
|
58618 | 405 |
subsubsection \<open>Examples\<close> |
48578 | 406 |
|
58618 | 407 |
text \<open> |
48578 | 408 |
Build a specific logic image: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
409 |
@{verbatim [display] \<open>isabelle build -b HOLCF\<close>} |
48578 | 410 |
|
61406 | 411 |
\<^smallskip> |
412 |
Build the main group of logic images: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
413 |
@{verbatim [display] \<open>isabelle build -b -g main\<close>} |
48578 | 414 |
|
61406 | 415 |
\<^smallskip> |
66748 | 416 |
Build all descendants (and requirements) of \<^verbatim>\<open>FOL\<close> and \<^verbatim>\<open>ZF\<close>: |
417 |
@{verbatim [display] \<open>isabelle build -B FOL -B ZF\<close>} |
|
418 |
||
419 |
\<^smallskip> |
|
420 |
Build all sessions where sources have changed (ignoring heaps): |
|
421 |
@{verbatim [display] \<open>isabelle build -a -S\<close>} |
|
422 |
||
423 |
\<^smallskip> |
|
61575 | 424 |
Provide a general overview of the status of all Isabelle sessions, without |
425 |
building anything: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
426 |
@{verbatim [display] \<open>isabelle build -a -n -v\<close>} |
48578 | 427 |
|
61406 | 428 |
\<^smallskip> |
61575 | 429 |
Build all sessions with HTML browser info and PDF document preparation: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
430 |
@{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>} |
48578 | 431 |
|
61406 | 432 |
\<^smallskip> |
61575 | 433 |
Build all sessions with a maximum of 8 parallel prover processes and 4 |
434 |
worker threads each (on a machine with many cores): |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
435 |
@{verbatim [display] \<open>isabelle build -a -j8 -o threads=4\<close>} |
48595 | 436 |
|
61406 | 437 |
\<^smallskip> |
61575 | 438 |
Build some session images with cleanup of their descendants, while retaining |
439 |
their ancestry: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
440 |
@{verbatim [display] \<open>isabelle build -b -c HOL-Algebra HOL-Word\<close>} |
48595 | 441 |
|
61406 | 442 |
\<^smallskip> |
443 |
Clean all sessions without building anything: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
444 |
@{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
|
445 |
|
61406 | 446 |
\<^smallskip> |
61575 | 447 |
Build all sessions from some other directory hierarchy, according to the |
448 |
settings variable \<^verbatim>\<open>AFP\<close> that happens to be defined inside the Isabelle |
|
449 |
environment: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
450 |
@{verbatim [display] \<open>isabelle build -D '$AFP'\<close>} |
49131 | 451 |
|
61406 | 452 |
\<^smallskip> |
61575 | 453 |
Inform about the status of all sessions required for AFP, without building |
454 |
anything yet: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
455 |
@{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>} |
58618 | 456 |
\<close> |
48578 | 457 |
|
66671 | 458 |
|
459 |
section \<open>Maintain theory imports wrt.\ session structure\<close> |
|
460 |
||
461 |
text \<open> |
|
462 |
The @{tool_def "imports"} tool helps to maintain theory imports wrt.\ |
|
463 |
session structure. It supports three main operations via options \<^verbatim>\<open>-I\<close>, |
|
464 |
\<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>. Its command-line usage is: @{verbatim [display] |
|
465 |
\<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...] |
|
466 |
||
467 |
Options are: |
|
66737
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66671
diff
changeset
|
468 |
-B NAME include session NAME and all descendants |
66671 | 469 |
-D DIR include session directory and select its sessions |
66851
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
470 |
-I operation: report session imports |
66671 | 471 |
-M operation: Mercurial repository check for theory files |
472 |
-R operate on requirements of selected sessions |
|
473 |
-U operation: update theory imports to use session qualifiers |
|
474 |
-X NAME exclude sessions from group NAME and all descendants |
|
475 |
-a select all sessions |
|
476 |
-d DIR include session directory |
|
477 |
-g NAME select session group NAME |
|
478 |
-i incremental update according to session graph structure |
|
479 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
480 |
-v verbose |
|
481 |
-x NAME exclude session NAME and all descendants |
|
482 |
||
483 |
Maintain theory imports wrt. session structure. At least one operation |
|
484 |
needs to be specified (see options -I -M -U).\<close>} |
|
485 |
||
486 |
\<^medskip> |
|
487 |
The selection of sessions and session directories works as for @{tool build} |
|
66737
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66671
diff
changeset
|
488 |
via options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> (see |
66671 | 489 |
\secref{sec:tool-build}). |
490 |
||
491 |
\<^medskip> |
|
492 |
Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build} |
|
493 |
(see \secref{sec:tool-build}). |
|
494 |
||
495 |
\<^medskip> |
|
496 |
Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. |
|
497 |
||
498 |
\<^medskip> |
|
66851
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
499 |
Option \<^verbatim>\<open>-I\<close> determines reports session imports: |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
500 |
|
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
501 |
\<^descr>[Potential session imports] are derived from old-style use of theory |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
502 |
files from other sessions via the directory structure. After declaring |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
503 |
those as \isakeyword{sessions} in the corresponding \<^verbatim>\<open>ROOT\<close> file entry, a |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
504 |
proper session-qualified theory name can be used (cf.\ option \<^verbatim>\<open>-U\<close>). For |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
505 |
example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> becomes formal |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
506 |
\<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions} |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
507 |
\<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry. |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
508 |
|
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
509 |
\<^descr>[Actual session imports] are derived from the session qualifiers of all |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
510 |
currently imported theories. This helps to minimize dependencies in the |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66841
diff
changeset
|
511 |
session import structure to what is actually required. |
66671 | 512 |
|
513 |
\<^medskip> |
|
514 |
Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of |
|
515 |
the underlying session directories; non-repository directories are ignored. |
|
516 |
This helps to find files that are accidentally ignored, e.g.\ due to |
|
517 |
rearrangements of the session structure. |
|
518 |
||
519 |
\<^medskip> |
|
520 |
Option \<^verbatim>\<open>-U\<close> updates theory imports with old-style directory specifications |
|
521 |
to canonical session-qualified theory names, according to the theory name |
|
522 |
space imported via \isakeyword{sessions} within the \<^verbatim>\<open>ROOT\<close> specification. |
|
523 |
||
524 |
Option \<^verbatim>\<open>-i\<close> modifies the meaning of option \<^verbatim>\<open>-U\<close> to proceed incrementally, |
|
525 |
following to the session graph structure in bottom-up order. This may |
|
526 |
lead to more accurate results in complex session hierarchies. |
|
527 |
\<close> |
|
528 |
||
529 |
subsubsection \<open>Examples\<close> |
|
530 |
||
531 |
text \<open> |
|
532 |
Determine potential session imports for some project directory: |
|
533 |
@{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>} |
|
534 |
||
535 |
\<^smallskip> |
|
536 |
Mercurial repository check for some project directory: |
|
537 |
@{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>} |
|
538 |
||
539 |
\<^smallskip> |
|
540 |
Incremental update of theory imports for some project directory: |
|
541 |
@{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>} |
|
542 |
\<close> |
|
543 |
||
48578 | 544 |
end |