author | wenzelm |
Sat, 24 Feb 2024 22:56:56 +0100 | |
changeset 79724 | 54d0f6edfe3a |
parent 79652 | 93e6ca9e7595 |
child 80178 | 438d583ab378 |
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> |
76987 | 39 |
of Isabelle/Isar, see also \<^cite>\<open>"isabelle-isar-ref"\<close>. This defines common |
61575 | 40 |
forms like identifiers, names, quoted strings, verbatim text, nested |
75986
27d98da31985
support 'chapter_definition' with description for presentation purposes;
wenzelm
parents:
75559
diff
changeset
|
41 |
comments etc. The grammar for @{syntax chapter_def}, @{syntax chapter_entry} |
27d98da31985
support 'chapter_definition' with description for presentation purposes;
wenzelm
parents:
75559
diff
changeset
|
42 |
and @{syntax session_entry} is given as syntax diagram below. Each ROOT file |
27d98da31985
support 'chapter_definition' with description for presentation purposes;
wenzelm
parents:
75559
diff
changeset
|
43 |
may contain multiple specifications like this. Chapters help to organize |
27d98da31985
support 'chapter_definition' with description for presentation purposes;
wenzelm
parents:
75559
diff
changeset
|
44 |
browser info (\secref{sec:info}), but have no formal meaning. The default |
76005
a9bbf075f431
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);
wenzelm
parents:
75998
diff
changeset
|
45 |
chapter is ``\<open>Unsorted\<close>''. Chapter definitions, which are optional, allow to |
a9bbf075f431
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);
wenzelm
parents:
75998
diff
changeset
|
46 |
associate additional information. |
48579 | 47 |
|
76987 | 48 |
Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close> includes a simple editing mode |
61575 | 49 |
\<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any |
50 |
file of that name. |
|
48579 | 51 |
|
69593 | 52 |
\<^rail>\<open> |
76005
a9bbf075f431
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);
wenzelm
parents:
75998
diff
changeset
|
53 |
@{syntax_def chapter_def}: @'chapter_definition' @{syntax name} \<newline> |
a9bbf075f431
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);
wenzelm
parents:
75998
diff
changeset
|
54 |
groups? description? |
75986
27d98da31985
support 'chapter_definition' with description for presentation purposes;
wenzelm
parents:
75559
diff
changeset
|
55 |
; |
27d98da31985
support 'chapter_definition' with description for presentation purposes;
wenzelm
parents:
75559
diff
changeset
|
56 |
|
27d98da31985
support 'chapter_definition' with description for presentation purposes;
wenzelm
parents:
75559
diff
changeset
|
57 |
@{syntax_def chapter_entry}: @'chapter' @{syntax name} |
51417 | 58 |
; |
59 |
||
66971 | 60 |
@{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline> |
70678
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70677
diff
changeset
|
61 |
(@{syntax system_name} '+')? description? options? \<newline> |
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70677
diff
changeset
|
62 |
sessions? directories? (theories*) \<newline> |
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72574
diff
changeset
|
63 |
(document_theories?) (document_files*) \<newline> |
76110
0605eb327e60
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
wenzelm
parents:
76107
diff
changeset
|
64 |
(export_files*) (export_classpath?) |
48579 | 65 |
; |
66 |
groups: '(' (@{syntax name} +) ')' |
|
67 |
; |
|
68808 | 68 |
dir: @'in' @{syntax embedded} |
48579 | 69 |
; |
70 |
description: @'description' @{syntax text} |
|
71 |
; |
|
72 |
options: @'options' opts |
|
73 |
; |
|
48605
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
74 |
opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']' |
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
75 |
; |
e777363440d6
allow negative int values as well, according to real = int | float;
wenzelm
parents:
48604
diff
changeset
|
76 |
value: @{syntax name} | @{syntax real} |
48579 | 77 |
; |
66916 | 78 |
sessions: @'sessions' (@{syntax system_name}+) |
65374 | 79 |
; |
70681 | 80 |
directories: @'directories' (dir+) |
70678
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70677
diff
changeset
|
81 |
; |
66970
13857f49d215
clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;
wenzelm
parents:
66916
diff
changeset
|
82 |
theories: @'theories' opts? (theory_entry+) |
48579 | 83 |
; |
66916 | 84 |
theory_entry: @{syntax system_name} ('(' @'global' ')')? |
65504 | 85 |
; |
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72574
diff
changeset
|
86 |
document_theories: @'document_theories' (@{syntax name}+) |
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72574
diff
changeset
|
87 |
; |
68808 | 88 |
document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+) |
68292 | 89 |
; |
69671 | 90 |
export_files: @'export_files' ('(' dir ')')? ('[' nat ']')? \<newline> |
91 |
(@{syntax embedded}+) |
|
76110
0605eb327e60
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
wenzelm
parents:
76107
diff
changeset
|
92 |
; |
0605eb327e60
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
wenzelm
parents:
76107
diff
changeset
|
93 |
export_classpath: @'export_classpath' (@{syntax embedded}*) |
69593 | 94 |
\<close> |
48579 | 95 |
|
76005
a9bbf075f431
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);
wenzelm
parents:
75998
diff
changeset
|
96 |
\<^descr> \isakeyword{chapter{\isacharunderscorekeyword}definition}~\<open>A (groups)\<close> |
a9bbf075f431
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);
wenzelm
parents:
75998
diff
changeset
|
97 |
associates a collection of groups with chapter \<open>A\<close>. All sessions that belong |
a9bbf075f431
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);
wenzelm
parents:
75998
diff
changeset
|
98 |
to this chapter will automatically become members of these groups. |
a9bbf075f431
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);
wenzelm
parents:
75998
diff
changeset
|
99 |
|
61575 | 100 |
\<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on |
66759 | 101 |
parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and |
102 |
theories). Note that a parent (like \<open>HOL\<close>) is mandatory in practical |
|
103 |
applications: only Isabelle/Pure can bootstrap itself from nothing. |
|
48579 | 104 |
|
65504 | 105 |
All such session specifications together describe a hierarchy (graph) of |
61575 | 106 |
sessions, with globally unique names. The new session name \<open>A\<close> should be |
107 |
sufficiently long and descriptive to stand on its own in a potentially large |
|
108 |
library. |
|
48579 | 109 |
|
61575 | 110 |
\<^descr> \isakeyword{session}~\<open>A (groups)\<close> indicates a collection of groups where |
111 |
the new session is a member. Group names are uninterpreted and merely follow |
|
112 |
certain conventions. For example, the Isabelle distribution tags some |
|
113 |
important sessions by the group name called ``\<open>main\<close>''. Other projects may |
|
114 |
invent their own conventions, but this requires some care to avoid clashes |
|
48604 | 115 |
within this unchecked name space. |
48579 | 116 |
|
61575 | 117 |
\<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close> specifies an explicit |
118 |
directory for this session; by default this is the current directory of the |
|
119 |
\<^verbatim>\<open>ROOT\<close> file. |
|
48579 | 120 |
|
66759 | 121 |
All theory files are located relatively to the session directory. The prover |
122 |
process is run within the same as its current working directory. |
|
48579 | 123 |
|
76005
a9bbf075f431
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);
wenzelm
parents:
75998
diff
changeset
|
124 |
\<^descr> \isakeyword{description}~\<open>text\<close> is a free-form description for this |
a9bbf075f431
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);
wenzelm
parents:
75998
diff
changeset
|
125 |
session (or chapter), e.g. for presentation purposes. |
48579 | 126 |
|
61575 | 127 |
\<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options |
128 |
(\secref{sec:system-options}) that are used when processing this session, |
|
129 |
but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z = |
|
130 |
true\<close> for Boolean options. |
|
131 |
||
65504 | 132 |
\<^descr> \isakeyword{sessions}~\<open>names\<close> specifies sessions that are \<^emph>\<open>imported\<close> into |
133 |
the current name space of theories. This allows to refer to a theory \<open>A\<close> |
|
134 |
from session \<open>B\<close> by the qualified name \<open>B.A\<close> --- although it is loaded again |
|
135 |
into the current ML process, which is in contrast to a theory that is |
|
136 |
already present in the \<^emph>\<open>parent\<close> session. |
|
137 |
||
65505 | 138 |
Theories that are imported from other sessions are excluded from the current |
139 |
session document. |
|
140 |
||
70678
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70677
diff
changeset
|
141 |
\<^descr> \isakeyword{directories}~\<open>dirs\<close> specifies additional directories for |
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70677
diff
changeset
|
142 |
import of theory files via \isakeyword{theories} within \<^verbatim>\<open>ROOT\<close> or |
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70677
diff
changeset
|
143 |
\<^theory_text>\<open>imports\<close> within a theory; \<open>dirs\<close> are relative to the main session |
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70677
diff
changeset
|
144 |
directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\<open>dir\<close>). These |
70681 | 145 |
directories need to be exclusively assigned to a unique session, without |
146 |
implicit sharing of file-system locations. |
|
70678
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70677
diff
changeset
|
147 |
|
61575 | 148 |
\<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that |
149 |
are processed within an environment that is augmented by the given options, |
|
150 |
in addition to the global session options given before. Any number of blocks |
|
151 |
of \isakeyword{theories} may be given. Options are only active for each |
|
48604 | 152 |
\isakeyword{theories} block separately. |
48579 | 153 |
|
65374 | 154 |
A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated |
66993 | 155 |
literally in other session specifications or theory imports --- the normal |
156 |
situation is to qualify theory names by the session name; this ensures |
|
157 |
globally unique names in big session graphs. Global theories are usually the |
|
158 |
entry points to major logic sessions: \<open>Pure\<close>, \<open>Main\<close>, \<open>Complex_Main\<close>, |
|
159 |
\<open>HOLCF\<close>, \<open>IFOL\<close>, \<open>FOL\<close>, \<open>ZF\<close>, \<open>ZFC\<close> etc. Regular Isabelle applications |
|
160 |
should not claim any global theory names. |
|
65374 | 161 |
|
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72574
diff
changeset
|
162 |
\<^descr> \isakeyword{document_theories}~\<open>names\<close> specifies theories from other |
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72574
diff
changeset
|
163 |
sessions that should be included in the generated document source directory. |
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72574
diff
changeset
|
164 |
These theories need to be explicit imports in the current session, or |
72769 | 165 |
implicit imports from the underlying hierarchy of parent sessions. The |
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72574
diff
changeset
|
166 |
generated \<^verbatim>\<open>session.tex\<close> file is not affected: the session's {\LaTeX} setup |
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72574
diff
changeset
|
167 |
needs to \<^verbatim>\<open>\input{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> generated \<^verbatim>\<open>.tex\<close> files separately. |
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72574
diff
changeset
|
168 |
|
61575 | 169 |
\<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists |
170 |
source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for |
|
171 |
{\LaTeX}. Only these explicitly given files are copied from the base |
|
172 |
directory to the document output directory, before formal document |
|
173 |
processing is started (see also \secref{sec:tool-document}). The local path |
|
174 |
structure of the \<open>files\<close> is preserved, which allows to reconstruct the |
|
68292 | 175 |
original directory hierarchy of \<open>base_dir\<close>. The default \<open>base_dir\<close> is |
176 |
\<^verbatim>\<open>document\<close> within the session root directory. |
|
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
55112
diff
changeset
|
177 |
|
69671 | 178 |
\<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) [number] |
69811
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
179 |
patterns\<close> specifies theory exports that may get written to the file-system, |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
180 |
e.g. via @{tool_ref build} with option \<^verbatim>\<open>-e\<close> (\secref{sec:tool-build}). The |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
181 |
\<open>target_dir\<close> specification is relative to the session root directory; its |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
182 |
default is \<^verbatim>\<open>export\<close>. Exports are selected via \<open>patterns\<close> as in @{tool_ref |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
183 |
export} (\secref{sec:tool-export}). The number given in brackets (default: |
75161
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
184 |
0) specifies the prefix of elements that should be removed from each name: |
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
185 |
it allows to reduce the resulting directory hierarchy at the danger of |
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
186 |
overwriting files due to loss of uniqueness. |
76110
0605eb327e60
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
wenzelm
parents:
76107
diff
changeset
|
187 |
|
0605eb327e60
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
wenzelm
parents:
76107
diff
changeset
|
188 |
\<^descr> \isakeyword{export_classpath}~\<open>patterns\<close> specifies export artifacts that |
0605eb327e60
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
wenzelm
parents:
76107
diff
changeset
|
189 |
should be included into the local Java/Scala classpath of this session |
0605eb327e60
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
wenzelm
parents:
76107
diff
changeset
|
190 |
context. This is only relevant for tools that allow dynamic loading of |
0605eb327e60
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
wenzelm
parents:
76107
diff
changeset
|
191 |
service classes (\secref{sec:scala-build}), while most other Isabelle/Scala |
0605eb327e60
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
wenzelm
parents:
76107
diff
changeset
|
192 |
tools require global configuration during system startup. An empty list of |
0605eb327e60
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
wenzelm
parents:
76107
diff
changeset
|
193 |
\<open>patterns\<close> defaults to \<^verbatim>\<open>"*:classpath/*.jar"\<close>, which fits to the naming |
0605eb327e60
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
wenzelm
parents:
76107
diff
changeset
|
194 |
convention of JAR modules produced by the Isabelle/Isar command |
76987 | 195 |
\<^theory_text>\<open>scala_build_generated_files\<close> \<^cite>\<open>"isabelle-isar-ref"\<close>. |
58618 | 196 |
\<close> |
48579 | 197 |
|
51055 | 198 |
|
58618 | 199 |
subsubsection \<open>Examples\<close> |
48580 | 200 |
|
61575 | 201 |
text \<open> |
63680 | 202 |
See \<^file>\<open>~~/src/HOL/ROOT\<close> for a diversity of practically relevant situations, |
203 |
although it uses relatively complex quasi-hierarchic naming conventions like |
|
204 |
\<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified |
|
205 |
names that are relatively long and descriptive, as in the Archive of Formal |
|
67605 | 206 |
Proofs (\<^url>\<open>https://isa-afp.org\<close>), for example. |
61575 | 207 |
\<close> |
48578 | 208 |
|
209 |
||
58618 | 210 |
section \<open>System build options \label{sec:system-options}\<close> |
48578 | 211 |
|
61575 | 212 |
text \<open> |
63680 | 213 |
See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle |
76987 | 214 |
distribution. Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close> includes a simple |
61575 | 215 |
editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format. |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
216 |
|
61575 | 217 |
The following options are particularly relevant to build Isabelle sessions, |
218 |
in particular with document preparation (\chref{ch:present}). |
|
51055 | 219 |
|
61575 | 220 |
\<^item> @{system_option_def "browser_info"} controls output of HTML browser |
221 |
info, see also \secref{sec:info}. |
|
51055 | 222 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72515
diff
changeset
|
223 |
\<^item> @{system_option_def "document"} controls document output for a |
73826
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73777
diff
changeset
|
224 |
particular session or theory; \<^verbatim>\<open>document=pdf\<close> or \<^verbatim>\<open>document=true\<close> means |
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73777
diff
changeset
|
225 |
enabled, \<^verbatim>\<open>document=""\<close> or \<^verbatim>\<open>document=false\<close> means disabled (especially |
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73777
diff
changeset
|
226 |
for particular theories). |
51055 | 227 |
|
61575 | 228 |
\<^item> @{system_option_def "document_output"} specifies an alternative |
229 |
directory for generated output of the document preparation system; the |
|
230 |
default is within the @{setting "ISABELLE_BROWSER_INFO"} hierarchy as |
|
231 |
explained in \secref{sec:info}. See also @{tool mkroot}, which generates a |
|
232 |
default configuration with output readily available to the author of the |
|
233 |
document. |
|
51055 | 234 |
|
74873 | 235 |
\<^item> @{system_option_def "document_echo"} informs about document file names |
236 |
during session presentation. |
|
237 |
||
61575 | 238 |
\<^item> @{system_option_def "document_variants"} specifies document variants as |
75161
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
239 |
a colon-separated list of \<open>name=tags\<close> entries. The default name is |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72515
diff
changeset
|
240 |
\<^verbatim>\<open>document\<close>, without additional tags. |
51055 | 241 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72515
diff
changeset
|
242 |
Tags are specified as a comma separated list of modifier/name pairs and |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72515
diff
changeset
|
243 |
tell {\LaTeX} how to interpret certain Isabelle command regions: |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72515
diff
changeset
|
244 |
``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to drop, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72515
diff
changeset
|
245 |
and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72515
diff
changeset
|
246 |
equivalent to the tag specification |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72515
diff
changeset
|
247 |
``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible,+important,+unimportant\<close>''; |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72515
diff
changeset
|
248 |
see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72515
diff
changeset
|
249 |
\<^verbatim>\<open>\isafoldtag\<close>, in \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72515
diff
changeset
|
250 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72515
diff
changeset
|
251 |
In contrast, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates |
61575 | 252 |
two documents: the one called \<^verbatim>\<open>document\<close> with default tags, and the other |
253 |
called \<^verbatim>\<open>outline\<close> where proofs and ML sections are folded. |
|
51055 | 254 |
|
61575 | 255 |
Document variant names are just a matter of conventions. It is also |
256 |
possible to use different document variant names (without tags) for |
|
257 |
different document root entries, see also \secref{sec:tool-document}. |
|
51055 | 258 |
|
68513 | 259 |
\<^item> @{system_option_def "document_tags"} specifies alternative command tags |
260 |
as a comma-separated list of items: either ``\<open>command\<close>\<^verbatim>\<open>%\<close>\<open>tag\<close>'' for a |
|
261 |
specific command, or ``\<^verbatim>\<open>%\<close>\<open>tag\<close>'' as default for all other commands. This |
|
262 |
is occasionally useful to control the global visibility of commands via |
|
263 |
session options (e.g.\ in \<^verbatim>\<open>ROOT\<close>). |
|
67140 | 264 |
|
74873 | 265 |
\<^item> @{system_option_def "document_comment_latex"} enables regular {\LaTeX} |
266 |
\<^verbatim>\<open>comment.sty\<close>, instead of the historic version for plain {\TeX} |
|
267 |
(default). The latter is much faster, but in conflict with {\LaTeX} |
|
268 |
classes like Dagstuhl |
|
269 |
LIPIcs\<^footnote>\<open>\<^url>\<open>https://github.com/dagstuhl-publishing/styles\<close>\<close>. |
|
270 |
||
73743 | 271 |
\<^item> @{system_option_def "document_bibliography"} explicitly enables the use |
272 |
of \<^verbatim>\<open>bibtex\<close>; the default is to check the presence of \<^verbatim>\<open>root.bib\<close>, but it |
|
273 |
could have a different name. |
|
274 |
||
74873 | 275 |
\<^item> @{system_option_def "document_heading_prefix"} specifies a prefix for |
276 |
the {\LaTeX} macro names generated from Isar commands like \<^theory_text>\<open>chapter\<close>, |
|
277 |
\<^theory_text>\<open>section\<close> etc. The default is \<^verbatim>\<open>isamarkup\<close>, e.g. \<^theory_text>\<open>section\<close> becomes |
|
278 |
\<^verbatim>\<open>\isamarkupsection\<close>. |
|
279 |
||
61575 | 280 |
\<^item> @{system_option_def "threads"} determines the number of worker threads |
281 |
for parallel checking of theories and proofs. The default \<open>0\<close> means that a |
|
79652 | 282 |
sensible value is guessed from the underlying hardware. This sometimes |
283 |
requires manual adjustment (on the command-line or within personal |
|
284 |
settings or preferences, not within a session \<^verbatim>\<open>ROOT\<close>). |
|
51055 | 285 |
|
61575 | 286 |
\<^item> @{system_option_def "condition"} specifies a comma-separated list of |
287 |
process environment variables (or Isabelle settings) that are required for |
|
288 |
the subsequent theories to be processed. Conditions are considered |
|
289 |
``true'' if the corresponding environment value is defined and non-empty. |
|
51055 | 290 |
|
61602 | 291 |
\<^item> @{system_option_def "timeout"} and @{system_option_def "timeout_scale"} |
292 |
specify a real wall-clock timeout for the session as a whole: the two |
|
293 |
values are multiplied and taken as the number of seconds. Typically, |
|
294 |
@{system_option "timeout"} is given for individual sessions, and |
|
295 |
@{system_option "timeout_scale"} as global adjustment to overall hardware |
|
296 |
performance. |
|
297 |
||
298 |
The timer is controlled outside the ML process by the JVM that runs |
|
299 |
Isabelle/Scala. Thus it is relatively reliable in canceling processes that |
|
300 |
get out of control, even if there is a deadlock without CPU time usage. |
|
51055 | 301 |
|
64308 | 302 |
\<^item> @{system_option_def "profiling"} specifies a mode for global ML |
303 |
profiling. Possible values are the empty string (disabled), \<^verbatim>\<open>time\<close> for |
|
69593 | 304 |
\<^ML>\<open>profile_time\<close> and \<^verbatim>\<open>allocations\<close> for \<^ML>\<open>profile_allocations\<close>. |
64308 | 305 |
Results appear near the bottom of the session log file. |
306 |
||
73777
52e43a93d51f
clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
wenzelm
parents:
73774
diff
changeset
|
307 |
\<^item> @{system_option_def system_log} specifies an optional log file for |
52e43a93d51f
clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
wenzelm
parents:
73774
diff
changeset
|
308 |
low-level messages produced by \<^ML>\<open>Output.system_message\<close> in |
74827
c1b5d6e6ff74
clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true";
wenzelm
parents:
74733
diff
changeset
|
309 |
Isabelle/ML; the standard value ``\<^verbatim>\<open>-\<close>'' refers to console progress of the |
c1b5d6e6ff74
clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true";
wenzelm
parents:
74733
diff
changeset
|
310 |
build job. |
73777
52e43a93d51f
clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
wenzelm
parents:
73774
diff
changeset
|
311 |
|
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69811
diff
changeset
|
312 |
\<^item> @{system_option_def "system_heaps"} determines the directories for |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69811
diff
changeset
|
313 |
session heap images: \<^path>\<open>$ISABELLE_HEAPS\<close> is the user directory and |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69811
diff
changeset
|
314 |
\<^path>\<open>$ISABELLE_HEAPS_SYSTEM\<close> the system directory (usually within the |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69811
diff
changeset
|
315 |
Isabelle application). For \<^verbatim>\<open>system_heaps=false\<close>, heaps are stored in the |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69811
diff
changeset
|
316 |
user directory and may be loaded from both directories. For |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69811
diff
changeset
|
317 |
\<^verbatim>\<open>system_heaps=true\<close>, store and load happens only in the system directory. |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69811
diff
changeset
|
318 |
|
61575 | 319 |
The @{tool_def options} tool prints Isabelle system options. Its |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
320 |
command-line usage is: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
321 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
322 |
\<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...] |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
323 |
|
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
324 |
Options are: |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
325 |
-b include $ISABELLE_BUILD_OPTIONS |
52735 | 326 |
-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
|
327 |
-l list options |
77616 | 328 |
-t TAGS restrict list to given tags (comma-separated) |
329 |
-x FILE export options to FILE in YXML format |
|
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
330 |
|
50531
f841ac0cb757
clarified "isabelle options" command line, to make it more close to "isabelle components";
wenzelm
parents:
50406
diff
changeset
|
331 |
Report Isabelle system options, augmented by MORE_OPTIONS given as |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
332 |
arguments NAME=VAL or NAME.\<close>} |
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
333 |
|
61575 | 334 |
The command line arguments provide additional system options of the form |
335 |
\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> for Boolean options. |
|
336 |
||
337 |
Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system options by the ones |
|
338 |
of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}. |
|
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
339 |
|
61575 | 340 |
Option \<^verbatim>\<open>-g\<close> prints the value of the given option. Option \<^verbatim>\<open>-l\<close> lists all |
77616 | 341 |
options with their declaration and current value. Option \<^verbatim>\<open>-t\<close> restricts the |
342 |
listing to given tags (as comma-separated list), e.g. \<^verbatim>\<open>-t build,document\<close>. |
|
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48684
diff
changeset
|
343 |
|
61575 | 344 |
Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in YXML format, instead |
345 |
of printing it in human-readable form. |
|
58618 | 346 |
\<close> |
48578 | 347 |
|
348 |
||
58618 | 349 |
section \<open>Invoking the build process \label{sec:tool-build}\<close> |
48578 | 350 |
|
61575 | 351 |
text \<open> |
352 |
The @{tool_def build} tool invokes the build process for Isabelle sessions. |
|
353 |
It manages dependencies between sessions, related sources of theories and |
|
354 |
auxiliary files, and target heap images. Accordingly, it runs instances of |
|
355 |
the prover process with optional document preparation. Its command-line |
|
356 |
usage is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via |
|
71896
ce06d6456cc8
clarified signature --- fit within limit of 22 arguments;
wenzelm
parents:
71893
diff
changeset
|
357 |
\<^scala_method>\<open>isabelle.Build.build\<close>.\<close> |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
358 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
359 |
\<open>Usage: isabelle build [OPTIONS] [SESSIONS ...] |
48578 | 360 |
|
361 |
Options are: |
|
78587 | 362 |
-A ROOT include AFP with given root directory (":" for $AFP_BASE) |
66737
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66671
diff
changeset
|
363 |
-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
|
364 |
-D DIR include session directory and select its sessions |
79615 | 365 |
-H HOSTS additional cluster host specifications of the form |
366 |
NAMES:PARAMETERS (separated by commas) |
|
64265 | 367 |
-N cyclic shuffling of NUMA CPU nodes (performance tuning) |
72648 | 368 |
-P DIR enable HTML/PDF presentation in directory (":" for default) |
71807 | 369 |
-R refer to requirements of selected sessions |
66745 | 370 |
-S soft build: only observe changes of sources, not heap images |
60106 | 371 |
-X NAME exclude sessions from group NAME and all descendants |
48578 | 372 |
-a select all sessions |
373 |
-b build heap images |
|
48595 | 374 |
-c clean build |
48737
f3bbb9ca57d6
added build option -D: include session directory and select its sessions;
wenzelm
parents:
48693
diff
changeset
|
375 |
-d DIR include session directory |
69811
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
376 |
-e export files from session specification into file-system |
66841 | 377 |
-f fresh build |
48578 | 378 |
-g NAME select session group NAME |
79647 | 379 |
-j INT maximum number of parallel jobs |
380 |
(default: 1 for local build, 0 for build cluster) |
|
59891
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59446
diff
changeset
|
381 |
-k KEYWORD check theory sources for conflicts with proposed keywords |
48903 | 382 |
-l list session source files |
77554
4465d9dff448
clarified terminology of "session build database", while "build database" is the one underlying Build_Process;
wenzelm
parents:
76987
diff
changeset
|
383 |
-n no build -- take existing session build databases |
52056 | 384 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
48578 | 385 |
-v verbose |
60106 | 386 |
-x NAME exclude session NAME and all descendants |
48578 | 387 |
|
77647 | 388 |
Build and manage Isabelle sessions: ML heaps, session databases, documents. |
62596 | 389 |
|
79615 | 390 |
Parameters for cluster host specifications (-H), apart from system options: |
78587 | 391 |
... |
392 |
||
77647 | 393 |
Notable system options: see "isabelle options -l -t build" |
48578 | 394 |
|
77647 | 395 |
Notable system settings: |
396 |
ISABELLE_TOOL_JAVA_OPTIONS="..." |
|
397 |
ISABELLE_BUILD_OPTIONS="..." |
|
398 |
||
399 |
ML_PLATFORM="..." |
|
400 |
ML_HOME="..." |
|
401 |
ML_SYSTEM="..." |
|
402 |
ML_OPTIONS="..."\<close>} |
|
48578 | 403 |
|
61406 | 404 |
\<^medskip> |
61575 | 405 |
Isabelle sessions are defined via session ROOT files as described in |
406 |
(\secref{sec:session-root}). The totality of sessions is determined by |
|
407 |
collecting such specifications from all Isabelle component directories |
|
408 |
(\secref{sec:components}), augmented by more directories given via options |
|
409 |
\<^verbatim>\<open>-d\<close>~\<open>DIR\<close> on the command line. Each such directory may contain a session |
|
61503 | 410 |
\<^verbatim>\<open>ROOT\<close> file with several session specifications. |
48578 | 411 |
|
61575 | 412 |
Any session root directory may refer recursively to further directories of |
413 |
the same kind, by listing them in a catalog file \<^verbatim>\<open>ROOTS\<close> line-by-line. This |
|
414 |
helps to organize large collections of session specifications, or to make |
|
66576 | 415 |
\<^verbatim>\<open>-d\<close> command line options persistent (e.g.\ in |
61503 | 416 |
\<^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
|
417 |
|
61406 | 418 |
\<^medskip> |
61575 | 419 |
The subset of sessions to be managed is determined via individual \<open>SESSIONS\<close> |
420 |
given as command-line arguments, or session groups that are given via one or |
|
421 |
more options \<^verbatim>\<open>-g\<close>~\<open>NAME\<close>. Option \<^verbatim>\<open>-a\<close> selects all sessions. The build tool |
|
422 |
takes session dependencies into account: the set of selected sessions is |
|
423 |
completed by including all ancestors. |
|
48578 | 424 |
|
61406 | 425 |
\<^medskip> |
68734
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68523
diff
changeset
|
426 |
One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions to be included (all |
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68523
diff
changeset
|
427 |
descendants wrt.\ the session parent or import graph). |
66737
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66671
diff
changeset
|
428 |
|
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66671
diff
changeset
|
429 |
\<^medskip> |
68734
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68523
diff
changeset
|
430 |
One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded (all |
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68523
diff
changeset
|
431 |
descendants wrt.\ the session parent or import graph). Option \<^verbatim>\<open>-X\<close> is |
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68523
diff
changeset
|
432 |
analogous to this, but excluded sessions are specified by session group |
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68523
diff
changeset
|
433 |
membership. |
59892
2a616319c171
added isabelle build option -x, to exclude sessions;
wenzelm
parents:
59891
diff
changeset
|
434 |
|
61406 | 435 |
\<^medskip> |
61575 | 436 |
Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense that it refers to its |
437 |
requirements: all ancestor sessions excluding the original selection. This |
|
438 |
allows to prepare the stage for some build process with different options, |
|
439 |
before running the main build itself (without option \<^verbatim>\<open>-R\<close>). |
|
49131 | 440 |
|
61406 | 441 |
\<^medskip> |
61575 | 442 |
Option \<^verbatim>\<open>-D\<close> is similar to \<^verbatim>\<open>-d\<close>, but selects all sessions that are defined |
443 |
in the given directories. |
|
48737
f3bbb9ca57d6
added build option -D: include session directory and select its sessions;
wenzelm
parents:
48693
diff
changeset
|
444 |
|
61406 | 445 |
\<^medskip> |
66745 | 446 |
Option \<^verbatim>\<open>-S\<close> indicates a ``soft build'': the selection is restricted to |
447 |
those sessions that have changed sources (according to actually imported |
|
448 |
theories). The status of heap images is ignored. |
|
449 |
||
450 |
\<^medskip> |
|
61406 | 451 |
The build process depends on additional options |
61575 | 452 |
(\secref{sec:system-options}) that are passed to the prover eventually. The |
453 |
settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide |
|
73826
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73777
diff
changeset
|
454 |
additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf |
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73777
diff
changeset
|
455 |
threads=4"\<close>. Moreover, the environment of system build options may be |
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73777
diff
changeset
|
456 |
augmented on the command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>, |
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73777
diff
changeset
|
457 |
which abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean or string options. |
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73777
diff
changeset
|
458 |
Multiple occurrences of \<^verbatim>\<open>-o\<close> on the command-line are applied in the given |
72900f34dbb3
allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents:
73777
diff
changeset
|
459 |
order. |
48578 | 460 |
|
61406 | 461 |
\<^medskip> |
72648 | 462 |
Option \<^verbatim>\<open>-P\<close> enables PDF/HTML presentation in the given directory, where |
463 |
``\<^verbatim>\<open>-P:\<close>'' refers to the default @{setting_ref ISABELLE_BROWSER_INFO} (or |
|
73012
238ddf525da4
clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in applications;
wenzelm
parents:
72878
diff
changeset
|
464 |
@{setting_ref ISABELLE_BROWSER_INFO_SYSTEM}). This applies only to |
75161
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
465 |
explicitly selected sessions; note that option \<^verbatim>\<open>-R\<close> allows to select all |
73012
238ddf525da4
clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in applications;
wenzelm
parents:
72878
diff
changeset
|
466 |
requirements separately. |
72648 | 467 |
|
468 |
\<^medskip> |
|
61575 | 469 |
Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected |
470 |
sessions. By default, images are only saved for inner nodes of the hierarchy |
|
471 |
of sessions, as required for other sessions to continue later on. |
|
48578 | 472 |
|
61406 | 473 |
\<^medskip> |
68734
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68523
diff
changeset
|
474 |
Option \<^verbatim>\<open>-c\<close> cleans the selected sessions (all descendants wrt.\ the session |
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68523
diff
changeset
|
475 |
parent or import graph) before performing the specified build operation. |
48595 | 476 |
|
61406 | 477 |
\<^medskip> |
69811
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
478 |
Option \<^verbatim>\<open>-e\<close> executes the \isakeyword{export_files} directives from the ROOT |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
479 |
specification of all explicitly selected sessions: the status of the session |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
480 |
build database needs to be OK, but the session could have been built |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
481 |
earlier. Using \isakeyword{export_files}, a session may serve as abstract |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
482 |
interface for add-on build artefacts, but these are only materialized on |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
483 |
explicit request: without option \<^verbatim>\<open>-e\<close> there is no effect on the physical |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
484 |
file-system yet. |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
485 |
|
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69755
diff
changeset
|
486 |
\<^medskip> |
66841 | 487 |
Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their |
488 |
requirements. |
|
489 |
||
76926 | 490 |
\<^medskip> Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage |
491 |
(including optional cleanup). The overall return code always the status of |
|
492 |
the set of selected sessions. Add-on builds (like presentation) are run for |
|
493 |
successful sessions, i.e.\ already finished ones. |
|
48595 | 494 |
|
61406 | 495 |
\<^medskip> |
61575 | 496 |
Option \<^verbatim>\<open>-j\<close> specifies the maximum number of parallel build jobs (prover |
497 |
processes). Each prover process is subject to a separate limit of parallel |
|
79647 | 498 |
worker threads, cf.\ system option @{system_option_ref threads}. The default |
499 |
is 1 for a local build, and 0 for a cluster build (see option \<^verbatim>\<open>-H\<close> below). |
|
48578 | 500 |
|
61406 | 501 |
\<^medskip> |
64265 | 502 |
Option \<^verbatim>\<open>-N\<close> enables cyclic shuffling of NUMA CPU nodes. This may help |
503 |
performance tuning on Linux servers with separate CPU/memory modules. |
|
504 |
||
505 |
\<^medskip> |
|
75161
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
506 |
Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. |
59891
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59446
diff
changeset
|
507 |
|
61406 | 508 |
\<^medskip> |
75161
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
509 |
Option \<^verbatim>\<open>-l\<close> lists the source files that contribute to a session. |
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
510 |
|
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
511 |
\<^medskip> |
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
512 |
Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax. It is |
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
513 |
possible to use option \<^verbatim>\<open>-k\<close> repeatedly to check multiple keywords. The |
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
514 |
theory sources are checked for conflicts wrt.\ this hypothetical change of |
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
515 |
syntax, e.g.\ to reveal occurrences of identifiers that need to be quoted. |
78587 | 516 |
|
517 |
\<^medskip> |
|
518 |
Option \<^verbatim>\<open>-H\<close> augments the cluster hosts to be used in this build process. |
|
519 |
Each \<^verbatim>\<open>-H\<close> option accepts multiple host names (separated by commas), which |
|
520 |
all share the same (optional) parameters. Multiple \<^verbatim>\<open>-H\<close> options may be |
|
521 |
given to specify further hosts (with different parameters). For example: |
|
522 |
\<^verbatim>\<open>-H host1,host2:jobs=2,threads=4 -H host3:jobs=4,threads=6\<close>. |
|
523 |
||
524 |
The syntax for host parameters follows Isabelle outer syntax, notably with |
|
525 |
double-quoted string literals. On the command-line, this may require extra |
|
526 |
single quotes or escapes. For example: \<^verbatim>\<open>-H 'host4:dirs="..."'\<close>. |
|
527 |
||
79647 | 528 |
The local host only participates in cluster build, if an explicit option |
529 |
\<^verbatim>\<open>-j\<close> > 0 is given. The default is 0, which means that \<^verbatim>\<open>isabelle build -H\<close> |
|
530 |
will initialize the build queue and oversee remote workers, but not run any |
|
531 |
Isabelle sessions on its own account. |
|
532 |
||
78587 | 533 |
The presence of at least one \<^verbatim>\<open>-H\<close> option changes the mode of operation of |
534 |
\<^verbatim>\<open>isabelle build\<close> substantially. It uses a shared PostgreSQL database |
|
535 |
server, which needs to be accessible from each node via local system options |
|
536 |
such as @{system_option "build_database_server"}, @{system_option |
|
537 |
"build_database_host"}, or @{system_option "build_database_ssh_host"}. |
|
538 |
Remote host connections are managed via regular SSH configuration, see also |
|
78626
f926602640fe
more portable: it really is the Cygwin $HOME not the Windows $USER_HOME;
wenzelm
parents:
78587
diff
changeset
|
539 |
\<^verbatim>\<open>$HOME/.ssh/config\<close> on each node. |
61575 | 540 |
\<close> |
59891
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59446
diff
changeset
|
541 |
|
48578 | 542 |
|
58618 | 543 |
subsubsection \<open>Examples\<close> |
48578 | 544 |
|
58618 | 545 |
text \<open> |
48578 | 546 |
Build a specific logic image: |
75558 | 547 |
@{verbatim [display] \<open> isabelle build -b HOLCF\<close>} |
48578 | 548 |
|
61406 | 549 |
\<^smallskip> |
550 |
Build the main group of logic images: |
|
75558 | 551 |
@{verbatim [display] \<open> isabelle build -b -g main\<close>} |
48578 | 552 |
|
61406 | 553 |
\<^smallskip> |
66748 | 554 |
Build all descendants (and requirements) of \<^verbatim>\<open>FOL\<close> and \<^verbatim>\<open>ZF\<close>: |
75558 | 555 |
@{verbatim [display] \<open> isabelle build -B FOL -B ZF\<close>} |
66748 | 556 |
|
557 |
\<^smallskip> |
|
558 |
Build all sessions where sources have changed (ignoring heaps): |
|
75558 | 559 |
@{verbatim [display] \<open> isabelle build -a -S\<close>} |
66748 | 560 |
|
561 |
\<^smallskip> |
|
61575 | 562 |
Provide a general overview of the status of all Isabelle sessions, without |
563 |
building anything: |
|
75558 | 564 |
@{verbatim [display] \<open> isabelle build -a -n -v\<close>} |
48578 | 565 |
|
61406 | 566 |
\<^smallskip> |
61575 | 567 |
Build all sessions with HTML browser info and PDF document preparation: |
75558 | 568 |
@{verbatim [display] \<open> isabelle build -a -o browser_info -o document\<close>} |
48578 | 569 |
|
61406 | 570 |
\<^smallskip> |
61575 | 571 |
Build all sessions with a maximum of 8 parallel prover processes and 4 |
572 |
worker threads each (on a machine with many cores): |
|
75558 | 573 |
@{verbatim [display] \<open> isabelle build -a -j8 -o threads=4\<close>} |
48595 | 574 |
|
61406 | 575 |
\<^smallskip> |
61575 | 576 |
Build some session images with cleanup of their descendants, while retaining |
577 |
their ancestry: |
|
75558 | 578 |
@{verbatim [display] \<open> isabelle build -b -c HOL-Library HOL-Algebra\<close>} |
48595 | 579 |
|
61406 | 580 |
\<^smallskip> |
76203 | 581 |
HTML/PDF presentation for sessions that happen to be properly built already, |
582 |
without rebuilding anything except the missing browser info: |
|
583 |
@{verbatim [display] \<open> isabelle build -a -n -o browser_info\<close>} |
|
584 |
||
585 |
\<^smallskip> |
|
61406 | 586 |
Clean all sessions without building anything: |
75558 | 587 |
@{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
|
588 |
|
61406 | 589 |
\<^smallskip> |
61575 | 590 |
Build all sessions from some other directory hierarchy, according to the |
591 |
settings variable \<^verbatim>\<open>AFP\<close> that happens to be defined inside the Isabelle |
|
592 |
environment: |
|
75558 | 593 |
@{verbatim [display] \<open> isabelle build -D '$AFP'\<close>} |
49131 | 594 |
|
61406 | 595 |
\<^smallskip> |
61575 | 596 |
Inform about the status of all sessions required for AFP, without building |
597 |
anything yet: |
|
75558 | 598 |
@{verbatim [display] \<open> isabelle build -D '$AFP' -R -v -n\<close>} |
78587 | 599 |
|
600 |
\<^smallskip> |
|
601 |
Run a distributed build on 3 cluster hosts (local, \<^verbatim>\<open>host1\<close>, \<^verbatim>\<open>host2\<close>): |
|
602 |
@{verbatim [display] \<open> isabelle build -a -j2 -o threads=8 \ |
|
603 |
-H host1:jobs=2,threads=8 |
|
604 |
-H host2:jobs=4:threads=4,numa,shared\<close>} |
|
58618 | 605 |
\<close> |
48578 | 606 |
|
66671 | 607 |
|
77554
4465d9dff448
clarified terminology of "session build database", while "build database" is the one underlying Build_Process;
wenzelm
parents:
76987
diff
changeset
|
608 |
section \<open>Print messages from session build database \label{sec:tool-log}\<close> |
72876 | 609 |
|
610 |
text \<open> |
|
77572 | 611 |
The @{tool_def "build_log"} tool prints prover messages from the build |
72876 | 612 |
database of the given session. Its command-line usage is: |
613 |
||
614 |
@{verbatim [display] |
|
77563 | 615 |
\<open>Usage: isabelle build_log [OPTIONS] [SESSIONS ...] |
72876 | 616 |
|
617 |
Options are: |
|
76089 | 618 |
-H REGEX filter messages by matching against head |
619 |
-M REGEX filter messages by matching against body |
|
72876 | 620 |
-T NAME restrict to given theories (multiple options possible) |
621 |
-U output Unicode symbols |
|
622 |
-m MARGIN margin for pretty printing (default: 76.0) |
|
623 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
73837
f72335f6a9ed
clarified documentation: tracing messages are not shown here;
wenzelm
parents:
73826
diff
changeset
|
624 |
-v print all messages, including information etc. |
72876 | 625 |
|
77554
4465d9dff448
clarified terminology of "session build database", while "build database" is the one underlying Build_Process;
wenzelm
parents:
76987
diff
changeset
|
626 |
Print messages from the session build database of the given sessions, |
4465d9dff448
clarified terminology of "session build database", while "build database" is the one underlying Build_Process;
wenzelm
parents:
76987
diff
changeset
|
627 |
without any checks against current sources nor session structure: results |
4465d9dff448
clarified terminology of "session build database", while "build database" is the one underlying Build_Process;
wenzelm
parents:
76987
diff
changeset
|
628 |
from old sessions or failed builds can be printed as well. |
72876 | 629 |
|
76089 | 630 |
Multiple options -H and -M are conjunctive: all given patterns need to |
631 |
match. Patterns match any substring, but ^ or $ may be used to match the |
|
632 |
start or end explicitly.\<close>} |
|
633 |
||
634 |
The specified session databases are taken as is, with formal checking |
|
635 |
against current sources: There is \<^emph>\<open>no\<close> implicit build process involved, so |
|
636 |
it is possible to retrieve error messages from a failed session as well. The |
|
637 |
order of messages follows the source positions of source files; thus the |
|
638 |
result is mostly deterministic, independent of the somewhat erratic |
|
639 |
evaluation of parallel processing. |
|
72876 | 640 |
|
641 |
\<^medskip> Option \<^verbatim>\<open>-o\<close> allows to change system options, as in @{tool build} |
|
642 |
(\secref{sec:tool-build}). This may affect the storage space for the build |
|
643 |
database, notably via @{system_option system_heaps}, or @{system_option |
|
644 |
build_database_server} and its relatives. |
|
645 |
||
646 |
\<^medskip> Option \<^verbatim>\<open>-T\<close> restricts output to given theories: multiple entries are |
|
647 |
possible by repeating this option on the command-line. The default is to |
|
75161
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
648 |
refer to \<^emph>\<open>all\<close> theories used in the original session build process. |
72876 | 649 |
|
650 |
\<^medskip> Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-U\<close> modify pretty printing and output of Isabelle |
|
651 |
symbols. The default is for an old-fashioned ASCII terminal at 80 characters |
|
652 |
per line (76 + 4 characters to prefix warnings or errors). |
|
72878 | 653 |
|
73837
f72335f6a9ed
clarified documentation: tracing messages are not shown here;
wenzelm
parents:
73826
diff
changeset
|
654 |
\<^medskip> Option \<^verbatim>\<open>-v\<close> prints all messages from the session database that are |
f72335f6a9ed
clarified documentation: tracing messages are not shown here;
wenzelm
parents:
73826
diff
changeset
|
655 |
normally inlined into the source text, including information messages etc. |
76089 | 656 |
|
657 |
\<^medskip> Options \<^verbatim>\<open>-H\<close> and \<^verbatim>\<open>-M\<close> filter messages according to their header or body |
|
658 |
content, respectively. The header follows a very basic format that makes it |
|
659 |
easy to match message kinds (e.g. \<^verbatim>\<open>Warning\<close> or \<^verbatim>\<open>Error\<close>) and file names |
|
660 |
(e.g. \<^verbatim>\<open>src/HOL/Nat.thy\<close>). The body is usually pretty-printed, but for |
|
661 |
matching it is treated like one long line: blocks are ignored and breaks are |
|
662 |
turned into plain spaces (according to their formal width). |
|
663 |
||
664 |
The syntax for patters follows regular expressions of the Java |
|
79724 | 665 |
platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close> |
72876 | 666 |
\<close> |
667 |
||
668 |
subsubsection \<open>Examples\<close> |
|
669 |
||
670 |
text \<open> |
|
671 |
Print messages from theory \<^verbatim>\<open>HOL.Nat\<close> of session \<^verbatim>\<open>HOL\<close>, using Unicode |
|
672 |
rendering of Isabelle symbols and a margin of 100 characters: |
|
77563 | 673 |
@{verbatim [display] \<open> isabelle build_log -T HOL.Nat -U -m 100 HOL\<close>} |
76089 | 674 |
|
675 |
Print warnings about ambiguous input (inner syntax) of session |
|
676 |
\<^verbatim>\<open>HOL-Library\<close>, which is built beforehand: |
|
677 |
@{verbatim [display] \<open> isabelle build HOL-Library |
|
77563 | 678 |
isabelle build_log -H "Warning" -M "Ambiguous input" HOL-Library\<close>} |
76089 | 679 |
|
680 |
Print all errors from all sessions, e.g. from a partial build of |
|
681 |
Isabelle/AFP: |
|
77563 | 682 |
@{verbatim [display] \<open> isabelle build_log -H "Error" $(isabelle sessions -a -d AFP/thys)\<close>} |
72876 | 683 |
\<close> |
684 |
||
685 |
||
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68116
diff
changeset
|
686 |
section \<open>Retrieve theory exports \label{sec:tool-export}\<close> |
68116 | 687 |
|
688 |
text \<open> |
|
689 |
The @{tool_def "export"} tool retrieves theory exports from the session |
|
690 |
database. Its command-line usage is: @{verbatim [display] |
|
691 |
\<open>Usage: isabelle export [OPTIONS] SESSION |
|
692 |
||
693 |
Options are: |
|
68314
2acbf8129d8b
clarified option -O: avoid conflict with build/dump option -D;
wenzelm
parents:
68292
diff
changeset
|
694 |
-O DIR output directory for exported files (default: "export") |
68116 | 695 |
-d DIR include session directory |
696 |
-l list exports |
|
697 |
-n no build of session |
|
698 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
69671 | 699 |
-p NUM prune path of exported files by NUM elements |
75161
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
700 |
-x PATTERN extract files matching pattern (e.g. "*:**" for all) |
68116 | 701 |
|
702 |
List or export theory exports for SESSION: named blobs produced by |
|
68290 | 703 |
isabelle build. Option -l or -x is required; option -x may be repeated. |
68116 | 704 |
|
705 |
The PATTERN language resembles glob patterns in the shell, with ? and * |
|
706 |
(both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], |
|
707 |
and variants {pattern1,pattern2,pattern3}.\<close>} |
|
708 |
||
709 |
\<^medskip> |
|
710 |
The specified session is updated via @{tool build} |
|
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69811
diff
changeset
|
711 |
(\secref{sec:tool-build}), with the same options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>. The option |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69811
diff
changeset
|
712 |
\<^verbatim>\<open>-n\<close> suppresses the implicit build process: it means that a potentially |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69811
diff
changeset
|
713 |
outdated session database is used! |
68116 | 714 |
|
715 |
\<^medskip> |
|
716 |
Option \<^verbatim>\<open>-l\<close> lists all stored exports, with compound names |
|
717 |
\<open>theory\<close>\<^verbatim>\<open>:\<close>\<open>name\<close>. |
|
718 |
||
719 |
\<^medskip> |
|
720 |
Option \<^verbatim>\<open>-x\<close> extracts stored exports whose compound name matches the given |
|
721 |
pattern. Note that wild cards ``\<^verbatim>\<open>?\<close>'' and ``\<^verbatim>\<open>*\<close>'' do not match the |
|
722 |
separators ``\<^verbatim>\<open>:\<close>'' and ``\<^verbatim>\<open>/\<close>''; the wild card \<^verbatim>\<open>**\<close> matches over directory |
|
723 |
name hierarchies separated by ``\<^verbatim>\<open>/\<close>''. Thus the pattern ``\<^verbatim>\<open>*:**\<close>'' matches |
|
68290 | 724 |
\<^emph>\<open>all\<close> theory exports. Multiple options \<^verbatim>\<open>-x\<close> refer to the union of all |
725 |
specified patterns. |
|
68116 | 726 |
|
68314
2acbf8129d8b
clarified option -O: avoid conflict with build/dump option -D;
wenzelm
parents:
68292
diff
changeset
|
727 |
Option \<^verbatim>\<open>-O\<close> specifies an alternative output directory for option \<^verbatim>\<open>-x\<close>: the |
68116 | 728 |
default is \<^verbatim>\<open>export\<close> within the current directory. Each theory creates its |
729 |
own sub-directory hierarchy, using the session-qualified theory name. |
|
69671 | 730 |
|
731 |
Option \<^verbatim>\<open>-p\<close> specifies the number of elements that should be pruned from |
|
732 |
each name: it allows to reduce the resulting directory hierarchy at the |
|
733 |
danger of overwriting files due to loss of uniqueness. |
|
68116 | 734 |
\<close> |
735 |
||
68348 | 736 |
|
737 |
section \<open>Dump PIDE session database \label{sec:tool-dump}\<close> |
|
738 |
||
739 |
text \<open> |
|
740 |
The @{tool_def "dump"} tool dumps information from the cumulative PIDE |
|
741 |
session database (which is processed on the spot). Its command-line usage |
|
742 |
is: @{verbatim [display] |
|
743 |
\<open>Usage: isabelle dump [OPTIONS] [SESSIONS ...] |
|
744 |
||
745 |
Options are: |
|
746 |
-A NAMES dump named aspects (default: ...) |
|
747 |
-B NAME include session NAME and all descendants |
|
748 |
-D DIR include session directory and select its sessions |
|
749 |
-O DIR output directory for dumped files (default: "dump") |
|
71807 | 750 |
-R refer to requirements of selected sessions |
68348 | 751 |
-X NAME exclude sessions from group NAME and all descendants |
752 |
-a select all sessions |
|
70862 | 753 |
-b NAME base logic image (default "Pure") |
68348 | 754 |
-d DIR include session directory |
755 |
-g NAME select session group NAME |
|
756 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
757 |
-v verbose |
|
758 |
-x NAME exclude session NAME and all descendants |
|
759 |
||
760 |
Dump cumulative PIDE session database, with the following aspects: |
|
761 |
...\<close>} |
|
762 |
||
763 |
\<^medskip> 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> and the |
|
764 |
remaining command-line arguments specify sessions as in @{tool build} |
|
765 |
(\secref{sec:tool-build}): the cumulative PIDE database of all their loaded |
|
766 |
theories is dumped to the output directory of option \<^verbatim>\<open>-O\<close> (default: \<^verbatim>\<open>dump\<close> |
|
767 |
in the current directory). |
|
768 |
||
70859
6e6254bbce1f
split into standard partitions, for improved scalability;
wenzelm
parents:
70858
diff
changeset
|
769 |
\<^medskip> Option \<^verbatim>\<open>-b\<close> specifies an optional base logic image, for improved |
70862 | 770 |
scalability of the PIDE session. Its theories are only processed if it is |
771 |
included in the overall session selection. |
|
70859
6e6254bbce1f
split into standard partitions, for improved scalability;
wenzelm
parents:
70858
diff
changeset
|
772 |
|
68348 | 773 |
\<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build} |
774 |
(\secref{sec:tool-build}). |
|
775 |
||
776 |
\<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. |
|
777 |
||
778 |
\<^medskip> Option \<^verbatim>\<open>-A\<close> specifies named aspects of the dump, as a comma-separated |
|
779 |
list. The default is to dump all known aspects, as given in the command-line |
|
71893 | 780 |
usage of the tool. The underlying Isabelle/Scala operation |
781 |
\<^scala_method>\<open>isabelle.Dump.dump\<close> takes aspects as user-defined |
|
782 |
operations on the final PIDE state and document version. This allows to |
|
783 |
imitate Prover IDE rendering under program control. |
|
68348 | 784 |
\<close> |
785 |
||
786 |
||
787 |
subsubsection \<open>Examples\<close> |
|
788 |
||
789 |
text \<open> |
|
790 |
Dump all Isabelle/ZF sessions (which are rather small): |
|
75558 | 791 |
@{verbatim [display] \<open> isabelle dump -v -B ZF\<close>} |
68348 | 792 |
|
793 |
\<^smallskip> |
|
70862 | 794 |
Dump the quite substantial \<^verbatim>\<open>HOL-Analysis\<close> session, with full bootstrap |
795 |
from Isabelle/Pure: |
|
75558 | 796 |
@{verbatim [display] \<open> isabelle dump -v HOL-Analysis\<close>} |
68348 | 797 |
|
798 |
\<^smallskip> |
|
70862 | 799 |
Dump all sessions connected to HOL-Analysis, using main Isabelle/HOL as |
800 |
basis: |
|
75558 | 801 |
@{verbatim [display] \<open> isabelle dump -v -b HOL -B HOL-Analysis\<close>} |
68348 | 802 |
|
803 |
This results in uniform PIDE markup for everything, except for the |
|
804 |
Isabelle/Pure bootstrap process itself. Producing that on the spot requires |
|
805 |
several GB of heap space, both for the Isabelle/Scala and Isabelle/ML |
|
806 |
process (in 64bit mode). Here are some relevant settings (\secref{sec:boot}) |
|
807 |
for such ambitious applications: |
|
808 |
@{verbatim [display] |
|
75558 | 809 |
\<open> ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m" |
810 |
ML_OPTIONS="--minheap 4G --maxheap 32G" |
|
68348 | 811 |
\<close>} |
69599 | 812 |
\<close> |
68348 | 813 |
|
69599 | 814 |
|
815 |
section \<open>Update theory sources based on PIDE markup \label{sec:tool-update}\<close> |
|
816 |
||
817 |
text \<open> |
|
818 |
The @{tool_def "update"} tool updates theory sources based on markup that is |
|
76921 | 819 |
produced by the regular @{tool build} process \secref{sec:tool-build}). Its |
820 |
command-line usage is: @{verbatim [display] |
|
69599 | 821 |
\<open>Usage: isabelle update [OPTIONS] [SESSIONS ...] |
822 |
||
823 |
Options are: |
|
824 |
-B NAME include session NAME and all descendants |
|
825 |
-D DIR include session directory and select its sessions |
|
71807 | 826 |
-R refer to requirements of selected sessions |
69599 | 827 |
-X NAME exclude sessions from group NAME and all descendants |
828 |
-a select all sessions |
|
76926 | 829 |
-b build heap images |
830 |
-c clean build |
|
69599 | 831 |
-d DIR include session directory |
76926 | 832 |
-f fresh build |
69599 | 833 |
-g NAME select session group NAME |
76921 | 834 |
-j INT maximum number of parallel jobs (default 1) |
76925
47f1b099497c
tuned options --- avoid confusion with "isabelle build -b";
wenzelm
parents:
76921
diff
changeset
|
835 |
-l NAME additional base logic |
77554
4465d9dff448
clarified terminology of "session build database", while "build database" is the one underlying Build_Process;
wenzelm
parents:
76987
diff
changeset
|
836 |
-n no build -- take existing session build databases |
69599 | 837 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
76927
da13da82f6f9
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
wenzelm
parents:
76926
diff
changeset
|
838 |
-u OPT override "update" option for selected sessions |
69599 | 839 |
-v verbose |
840 |
-x NAME exclude session NAME and all descendants |
|
841 |
||
76926 | 842 |
Update theory sources based on PIDE markup produced by "isabelle build".\<close>} |
69599 | 843 |
|
76926 | 844 |
\<^medskip> Most options are the same as for @{tool build} (\secref{sec:tool-build}). |
76921 | 845 |
|
76925
47f1b099497c
tuned options --- avoid confusion with "isabelle build -b";
wenzelm
parents:
76921
diff
changeset
|
846 |
\<^medskip> Option \<^verbatim>\<open>-l\<close> specifies one or more base logics: these sessions and their |
76921 | 847 |
ancestors are \<^emph>\<open>excluded\<close> from the update. |
69599 | 848 |
|
76926 | 849 |
\<^medskip> Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close> options, by relying on naming |
850 |
convention: ``\<^verbatim>\<open>-u\<close>~\<open>OPT\<close>'' is a shortcut for ``\<^verbatim>\<open>-o\<close>~\<^verbatim>\<open>update_\<close>\<open>OPT\<close>''. |
|
69599 | 851 |
|
75161
95612f330c93
misc tuning based on comments by Heiko Eißfeldt;
wenzelm
parents:
74873
diff
changeset
|
852 |
\<^medskip> The following \<^verbatim>\<open>update\<close> options are supported: |
69599 | 853 |
|
76983 | 854 |
\<^item> @{system_option_ref update_inner_syntax_cartouches} to update inner |
855 |
syntax (types, terms, etc.)~to use cartouches, instead of double-quoted |
|
856 |
strings or atomic identifiers. For example, ``\<^theory_text>\<open>lemma \<doublequote>x = |
|
69610 | 857 |
x\<doublequote>\<close>'' is replaced by ``\<^theory_text>\<open>lemma \<open>x = x\<close>\<close>'', and ``\<^theory_text>\<open>assume |
858 |
A\<close>'' is replaced by ``\<^theory_text>\<open>assume \<open>A\<close>\<close>''. |
|
69599 | 859 |
|
860 |
\<^item> @{system_option update_mixfix_cartouches} to update mixfix templates to |
|
861 |
use cartouches instead of double-quoted strings. For example, ``\<^theory_text>\<open>(infixl |
|
862 |
\<doublequote>+\<doublequote> 65)\<close>'' is replaced by ``\<^theory_text>\<open>(infixl \<open>+\<close> |
|
863 |
65)\<close>''. |
|
864 |
||
76983 | 865 |
\<^item> @{system_option_ref update_control_cartouches} to update antiquotations |
866 |
to use the compact form with control symbol and cartouche argument. For |
|
69599 | 867 |
example, ``\<open>@{term \<doublequote>x + y\<doublequote>}\<close>'' is replaced by |
868 |
``\<open>\<^term>\<open>x + y\<close>\<close>'' (the control symbol is literally \<^verbatim>\<open>\<^term>\<close>.) |
|
869 |
||
76983 | 870 |
\<^item> @{system_option_ref update_path_cartouches} to update file-system paths |
871 |
to use cartouches: this depends on language markup provided by semantic |
|
69603 | 872 |
processing of parsed input. |
873 |
||
76983 | 874 |
\<^item> @{system_option_ref update_cite} to update {\LaTeX} \<^verbatim>\<open>\cite\<close> commands |
875 |
and old-style \<^verbatim>\<open>@{cite "name"}\<close> document antiquotations. |
|
76982 | 876 |
|
69599 | 877 |
It is also possible to produce custom updates in Isabelle/ML, by reporting |
878 |
\<^ML>\<open>Markup.update\<close> with the precise source position and a replacement |
|
879 |
text. This operation should be made conditional on specific system options, |
|
880 |
similar to the ones above. Searching the above option names in ML sources of |
|
881 |
\<^dir>\<open>$ISABELLE_HOME/src/Pure\<close> provides some examples. |
|
882 |
||
69602 | 883 |
Updates can be in conflict by producing nested or overlapping edits: this |
884 |
may require to run @{tool update} multiple times. |
|
69599 | 885 |
\<close> |
886 |
||
887 |
||
888 |
subsubsection \<open>Examples\<close> |
|
889 |
||
890 |
text \<open> |
|
891 |
Update some cartouche notation in all theory sources required for session |
|
70863
d1299774543d
clarified "isabelle update" options -- more like "isabelle dump";
wenzelm
parents:
70862
diff
changeset
|
892 |
\<^verbatim>\<open>HOL-Analysis\<close> (and ancestors): |
69599 | 893 |
|
75558 | 894 |
@{verbatim [display] \<open> isabelle update -u mixfix_cartouches HOL-Analysis\<close>} |
69599 | 895 |
|
76921 | 896 |
\<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close>, but |
897 |
do not change the underlying \<^verbatim>\<open>HOL\<close> (and \<^verbatim>\<open>Pure\<close>) session: |
|
69599 | 898 |
|
76925
47f1b099497c
tuned options --- avoid confusion with "isabelle build -b";
wenzelm
parents:
76921
diff
changeset
|
899 |
@{verbatim [display] \<open> isabelle update -u mixfix_cartouches -l HOL -B HOL-Analysis\<close>} |
69599 | 900 |
|
76921 | 901 |
\<^smallskip> Update all sessions that happen to be properly built beforehand: |
69599 | 902 |
|
76921 | 903 |
@{verbatim [display] \<open> isabelle update -u mixfix_cartouches -n -a\<close>} |
68348 | 904 |
\<close> |
905 |
||
71808 | 906 |
|
907 |
section \<open>Explore sessions structure\<close> |
|
908 |
||
909 |
text \<open> |
|
910 |
The @{tool_def "sessions"} tool explores the sessions structure. Its |
|
911 |
command-line usage is: |
|
912 |
@{verbatim [display] |
|
913 |
\<open>Usage: isabelle sessions [OPTIONS] [SESSIONS ...] |
|
914 |
||
915 |
Options are: |
|
916 |
-B NAME include session NAME and all descendants |
|
917 |
-D DIR include session directory and select its sessions |
|
918 |
-R refer to requirements of selected sessions |
|
919 |
-X NAME exclude sessions from group NAME and all descendants |
|
920 |
-a select all sessions |
|
76107 | 921 |
-b follow session build dependencies (default: source imports) |
71808 | 922 |
-d DIR include session directory |
923 |
-g NAME select session group NAME |
|
924 |
-x NAME exclude session NAME and all descendants |
|
925 |
||
926 |
Explore the structure of Isabelle sessions and print result names in |
|
927 |
topological order (on stdout).\<close>} |
|
928 |
||
929 |
Arguments and options for session selection resemble @{tool build} |
|
930 |
(\secref{sec:tool-build}). |
|
931 |
\<close> |
|
932 |
||
933 |
||
934 |
subsubsection \<open>Examples\<close> |
|
935 |
||
936 |
text \<open> |
|
937 |
All sessions of the Isabelle distribution: |
|
75558 | 938 |
@{verbatim [display] \<open> isabelle sessions -a\<close>} |
71808 | 939 |
|
940 |
\<^medskip> |
|
76107 | 941 |
Sessions that are imported by \<^verbatim>\<open>ZF\<close>: |
942 |
@{verbatim [display] \<open> isabelle sessions ZF\<close>} |
|
943 |
||
944 |
\<^medskip> |
|
945 |
Sessions that are required to build \<^verbatim>\<open>ZF\<close>: |
|
946 |
@{verbatim [display] \<open> isabelle sessions -b ZF\<close>} |
|
947 |
||
948 |
\<^medskip> |
|
949 |
Sessions that are based on \<^verbatim>\<open>ZF\<close> (and imported by it): |
|
75558 | 950 |
@{verbatim [display] \<open> isabelle sessions -B ZF\<close>} |
71808 | 951 |
|
952 |
\<^medskip> |
|
953 |
All sessions of Isabelle/AFP (based in directory \<^path>\<open>AFP\<close>): |
|
75558 | 954 |
@{verbatim [display] \<open> isabelle sessions -D AFP/thys\<close>} |
71808 | 955 |
|
956 |
\<^medskip> |
|
957 |
Sessions required by Isabelle/AFP (based in directory \<^path>\<open>AFP\<close>): |
|
75558 | 958 |
@{verbatim [display] \<open> isabelle sessions -R -D AFP/thys\<close>} |
71808 | 959 |
\<close> |
960 |
||
75556 | 961 |
|
962 |
section \<open>Synchronize source repositories and session images for Isabelle and AFP\<close> |
|
963 |
||
964 |
text \<open> |
|
75557 | 965 |
The @{tool_def sync} tool synchronizes a local Isabelle and AFP source |
966 |
repository, possibly with prebuilt \<^verbatim>\<open>.jar\<close> files and session images. Its |
|
967 |
command-line usage is: @{verbatim [display] |
|
75556 | 968 |
\<open>Usage: isabelle sync [OPTIONS] TARGET |
969 |
||
970 |
Options are: |
|
971 |
-A ROOT include AFP with given root directory (":" for $AFP_BASE) |
|
972 |
-H purge heaps directory on target |
|
973 |
-I NAME include session heap image and build database |
|
974 |
(based on accidental local state) |
|
975 |
-J preserve *.jar files |
|
976 |
-T thorough treatment of file content and directory times |
|
977 |
-a REV explicit AFP revision (default: state of working directory) |
|
77783
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77647
diff
changeset
|
978 |
-s HOST SSH host name for remote target (default: local) |
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77647
diff
changeset
|
979 |
-u USER explicit SSH user name |
75556 | 980 |
-n no changes: dry-run |
77783
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77647
diff
changeset
|
981 |
-p PORT explicit SSH port |
75556 | 982 |
-r REV explicit revision (default: state of working directory) |
983 |
-v verbose |
|
984 |
||
985 |
Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".\<close>} |
|
986 |
||
75557 | 987 |
The approach is to apply @{tool hg_sync} (see \secref{sec:tool-hg-sync}) on |
988 |
the underlying Isabelle repository, and an optional AFP repository. |
|
989 |
Consequently, the Isabelle installation needs to be a Mercurial repository |
|
75556 | 990 |
clone: a regular download of the Isabelle distribution is not sufficient! |
991 |
||
992 |
On the target side, AFP is placed into @{setting ISABELLE_HOME} as immediate |
|
993 |
sub-directory with the literal name \<^verbatim>\<open>AFP\<close>; thus it can be easily included |
|
994 |
elsewhere, e.g. @{tool build}~\<^verbatim>\<open>-d\<close>~\<^verbatim>\<open>'~~/AFP'\<close> on the remote side. |
|
995 |
||
77792
b81b2c50fc7c
use "rsync --secluded-args" by default, discontinue obsolete option -P of sync tools;
wenzelm
parents:
77783
diff
changeset
|
996 |
\<^medskip> Options \<^verbatim>\<open>-T\<close>, \<^verbatim>\<open>-n\<close>, \<^verbatim>\<open>-p\<close>, \<^verbatim>\<open>-s\<close>, \<^verbatim>\<open>-u\<close>, \<^verbatim>\<open>-v\<close> are the same as |
77783
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77647
diff
changeset
|
997 |
the underlying @{tool hg_sync}. |
75556 | 998 |
|
999 |
\<^medskip> Options \<^verbatim>\<open>-r\<close> and \<^verbatim>\<open>-a\<close> are the same as option \<^verbatim>\<open>-r\<close> for @{tool hg_sync}, |
|
1000 |
but for the Isabelle and AFP repositories, respectively. The AFP version is |
|
1001 |
only used if a corresponding repository is given via option \<^verbatim>\<open>-A\<close>, either |
|
1002 |
with explicit root directory, or as \<^verbatim>\<open>-A:\<close> to refer to \<^verbatim>\<open>$AFP_BASE\<close> (this |
|
75557 | 1003 |
assumes AFP as component of the local Isabelle installation). If no AFP |
1004 |
repository is given, an existing \<^verbatim>\<open>AFP\<close> directory on the target remains |
|
1005 |
unchanged. |
|
75556 | 1006 |
|
75557 | 1007 |
\<^medskip> Option \<^verbatim>\<open>-J\<close> uploads existing \<^verbatim>\<open>.jar\<close> files from the working directory, |
1008 |
which are usually Isabelle/Scala/Java modules under control of @{tool |
|
1009 |
scala_build} via \<^verbatim>\<open>etc/build.props\<close> (see also \secref{sec:scala-build}). |
|
1010 |
Thus the dependency management is accurate: bad uploads will be rebuilt |
|
1011 |
eventually (or ignored). This might fail for very old Isabelle versions, |
|
1012 |
when going into the past via option \<^verbatim>\<open>-r\<close>: here it is better to omit option |
|
1013 |
\<^verbatim>\<open>-J\<close> and thus purge \<^verbatim>\<open>.jar\<close> files on the target (because they do not belong |
|
1014 |
to the repository). |
|
75556 | 1015 |
|
1016 |
\<^medskip> Option \<^verbatim>\<open>-I\<close> uploads a collection of session images. The set of \<^verbatim>\<open>-I\<close> |
|
1017 |
options specifies the end-points in the session build graph, including all |
|
1018 |
required ancestors. The result collection is uploaded using the underlying |
|
75557 | 1019 |
\<^verbatim>\<open>rsync\<close> policies, so unchanged images are not sent again. Session images |
1020 |
are assembled within the target \<^verbatim>\<open>heaps\<close> directory: this scheme fits |
|
1021 |
together with @{tool build}~\<^verbatim>\<open>-o system_heaps\<close>. Images are taken as-is from |
|
1022 |
the local Isabelle installation, regardless of option \<^verbatim>\<open>-r\<close>. Upload of bad |
|
1023 |
images could waste time and space, but running e.g. @{tool build} on the |
|
1024 |
target will check dependencies accurately and rebuild outdated images on |
|
1025 |
demand. |
|
75556 | 1026 |
|
1027 |
\<^medskip> Option \<^verbatim>\<open>-H\<close> tells the underlying \<^verbatim>\<open>rsync\<close> process to purge the \<^verbatim>\<open>heaps\<close> |
|
75557 | 1028 |
directory on the target, before uploading new images via option \<^verbatim>\<open>-I\<close>. The |
75556 | 1029 |
default is to work monotonically: old material that is not overwritten |
75557 | 1030 |
remains unchanged. Over time, this may lead to unused garbage, due to |
1031 |
changes in session names or the Poly/ML version. Option \<^verbatim>\<open>-H\<close> helps to avoid |
|
1032 |
wasting file-system space. |
|
75556 | 1033 |
\<close> |
1034 |
||
1035 |
subsubsection \<open>Examples\<close> |
|
1036 |
||
1037 |
text \<open> |
|
75557 | 1038 |
For quick testing of Isabelle + AFP on a remote machine, upload changed |
1039 |
sources, jars, and local sessions images for \<^verbatim>\<open>HOL\<close>: |
|
1040 |
||
77783
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77647
diff
changeset
|
1041 |
@{verbatim [display] \<open> isabelle sync -A: -I HOL -J -s testmachine test/isabelle_afp\<close>} |
75556 | 1042 |
Assuming that the local \<^verbatim>\<open>HOL\<close> hierarchy has been up-to-date, and the local |
1043 |
and remote ML platforms coincide, a remote @{tool build} will proceed |
|
1044 |
without building \<^verbatim>\<open>HOL\<close> again. |
|
1045 |
||
75557 | 1046 |
\<^medskip> Here is a variation for extra-clean testing of Isabelle + AFP: no option |
1047 |
\<^verbatim>\<open>-J\<close>, but option \<^verbatim>\<open>-T\<close> to disable the default ``quick check'' of \<^verbatim>\<open>rsync\<close> |
|
1048 |
(which only inspects file sizes and date stamps); existing heaps are |
|
1049 |
deleted: |
|
77783
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77647
diff
changeset
|
1050 |
@{verbatim [display] \<open> isabelle sync -A: -T -H -s testmachine test/isabelle_afp\<close>} |
75556 | 1051 |
\<close> |
1052 |
||
48578 | 1053 |
end |