author | wenzelm |
Thu, 02 Apr 2020 12:49:53 +0200 | |
changeset 71656 | 3e121f999120 |
parent 71583 | 200ec7c4c1a5 |
child 73188 | 6e7ac8cefe57 |
permissions | -rw-r--r-- |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
1 |
Important notes on Mercurial repository access for Isabelle |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
2 |
=========================================================== |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
3 |
|
54963 | 4 |
Quick start in 30min |
49348 | 5 |
-------------------- |
6 |
||
63490
9416333a17c2
prefer curl: presumably more portable and versatile;
wenzelm
parents:
54963
diff
changeset
|
7 |
1a. Linux and Mac OS X: ensure that Mercurial is installed |
68378 | 8 |
(see also https://www.mercurial-scm.org) |
49348 | 9 |
|
66763
0b3fa8e22f22
prefer Cygwin64, although some components still require update;
wenzelm
parents:
66753
diff
changeset
|
10 |
1b. Windows: ensure that Cygwin64 with curl and Mercurial is installed |
68378 | 11 |
(see also https://www.cygwin.com) |
49348 | 12 |
|
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
50617
diff
changeset
|
13 |
2. Clone repository (bash shell commands): |
49348 | 14 |
|
67744 | 15 |
hg clone https://isabelle.in.tum.de/repos/isabelle |
49348 | 16 |
|
50575 | 17 |
cd isabelle |
49348 | 18 |
|
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
50617
diff
changeset
|
19 |
./bin/isabelle components -I |
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
50617
diff
changeset
|
20 |
|
50575 | 21 |
./bin/isabelle components -a |
49348 | 22 |
|
50575 | 23 |
./bin/isabelle jedit -l HOL |
49348 | 24 |
|
51502 | 25 |
./bin/isabelle build -b HOL #optional: build session image manually |
26 |
||
50653
5c85f8b80b95
simplified quick start via "isabelle components -I";
wenzelm
parents:
50617
diff
changeset
|
27 |
3. Update repository (bash shell commands): |
50281
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
28 |
|
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
29 |
cd isabelle |
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
30 |
|
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
31 |
hg pull -u |
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
32 |
|
50575 | 33 |
./bin/isabelle components -a |
34 |
||
35 |
./bin/isabelle jedit -l HOL |
|
36 |
||
51502 | 37 |
4. Access documentation (bash shell commands): |
38 |
||
53359 | 39 |
./bin/isabelle build_doc -a |
51502 | 40 |
|
41 |
./bin/isabelle doc system |
|
42 |
||
49348 | 43 |
|
40601 | 44 |
Introduction |
45 |
------------ |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
46 |
|
68378 | 47 |
Mercurial https://www.mercurial-scm.org belongs to source code |
63985 | 48 |
management systems that follow the so-called paradigm of "distributed |
71583 | 49 |
version control". This means plain versioning without the legacy of |
50 |
SVN and the extra complexity of GIT. See also |
|
51 |
https://www.mercurial-scm.org/learn |
|
40601 | 52 |
|
63985 | 53 |
Mercurial offers some flexibility in organizing the flow of changes, |
40601 | 54 |
both between individual developers and designated pull/push areas that |
63985 | 55 |
are shared with others. This additional freedom demands additional |
40601 | 56 |
responsibility to maintain a certain development process that fits to |
57 |
a particular project. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
58 |
|
40601 | 59 |
Regular Mercurial operations are strictly monotonic, where changeset |
51502 | 60 |
transactions are only added, but never deleted or mutated. There are |
61 |
special tools to manipulate repositories via non-monotonic actions |
|
62 |
(such as "rollback" or "strip"), but recovering from gross mistakes |
|
63 |
that have escaped into the public can be hard and embarrassing. It is |
|
64 |
much easier to inspect and amend changesets routinely before pushing. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
65 |
|
40601 | 66 |
The effect of the critical "pull" / "push" operations can be tested in |
67 |
a dry run via "incoming" / "outgoing". The "fetch" extension includes |
|
51502 | 68 |
useful sanity checks beyond raw "pull" / "update" / "merge", although |
69 |
it has lost popularity in recent years. Most other operations are |
|
70 |
local to the user's repository clone. This gives some freedom for |
|
71 |
experimentation without affecting anybody else. |
|
40601 | 72 |
|
73 |
Mercurial provides nice web presentation of incoming changes with a |
|
74 |
digest of log entries; this also includes RSS/Atom news feeds. There |
|
47449 | 75 |
are add-on history browsers such as "hg view" and TortoiseHg. Unlike |
76 |
the default web view, some of these tools help to inspect the semantic |
|
77 |
content of non-trivial merge nodes. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
78 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
79 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
80 |
Initial configuration |
29481 | 81 |
--------------------- |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
82 |
|
51502 | 83 |
The main Isabelle repository can be cloned like this: |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
84 |
|
67744 | 85 |
hg clone https://isabelle.in.tum.de/repos/isabelle |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
86 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
87 |
This will create a local directory "isabelle", unless an alternative |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
88 |
name is specified. The full repository meta-data and history of |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
89 |
changes is in isabelle/.hg; local configuration for this clone can be |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
90 |
added to isabelle/.hg/hgrc, but note that hgrc files are never copied |
40601 | 91 |
by another clone operation. |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
92 |
|
28917 | 93 |
|
28913 | 94 |
There is also $HOME/.hgrc for per-user Mercurial configuration. The |
40601 | 95 |
initial configuration requires at least an entry to identify yourself |
96 |
as follows: |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
97 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
98 |
[ui] |
71583 | 99 |
username = ABC |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
100 |
|
40601 | 101 |
Isabelle contributors are free to choose either a short "login name" |
102 |
(for accounts at TU Munich) or a "full name" -- with or without mail |
|
103 |
address. It is important to stick to this choice once and for all. |
|
104 |
The machine default that Mercurial produces for unspecified |
|
105 |
[ui]username is not appropriate. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
106 |
|
40601 | 107 |
Such configuration can be given in $HOME/.hgrc (for each home |
108 |
directory on each machine) or in .hg/hgrc (for each repository clone). |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
109 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
110 |
|
40601 | 111 |
Here are some further examples for hgrc. This is how to provide |
112 |
default options for common commands: |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
113 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
114 |
[defaults] |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
115 |
log = -l 10 |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
116 |
|
40601 | 117 |
This is how to configure some extension, which is called "graphlog" |
118 |
and provides the "glog" command: |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
119 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
120 |
[extensions] |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
121 |
hgext.graphlog = |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
122 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
123 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
124 |
Shared pull/push access |
29481 | 125 |
----------------------- |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
126 |
|
67744 | 127 |
The entry point https://isabelle.in.tum.de/repos/isabelle is world |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
128 |
readable, both via plain web browsing and the hg client as described |
40601 | 129 |
above. Anybody can produce a clone, change it locally, and then use |
130 |
regular mechanisms of Mercurial to report changes upstream, say via |
|
131 |
mail to someone with write access to that file space. It is also |
|
132 |
quite easy to publish changed clones again on the web, using the |
|
133 |
ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts |
|
134 |
that are included in the Mercurial distribution, and send a "pull |
|
71583 | 135 |
request" to someone else. |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
136 |
|
28913 | 137 |
The downstream/upstream mode of operation is quite common in the |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
138 |
distributed version control community, and works well for occasional |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
139 |
changes produced by anybody out there. Of course, upstream |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
140 |
maintainers need to review and moderate changes being proposed, before |
40601 | 141 |
pushing anything onto the official Isabelle repository at TUM. Direct |
142 |
pushes are also reviewed routinely in a post-hoc fashion; everybody |
|
143 |
hooked on the main repository is called to keep an eye on incoming |
|
51502 | 144 |
changes. In any case, changesets need to be understandable, both at |
145 |
the time of writing and many years later. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
146 |
|
40601 | 147 |
Push access to the Isabelle repository requires an account at TUM, |
51072 | 148 |
with properly configured ssh to isabelle-server.in.tum.de. You also |
149 |
need to be a member of the "isabelle" Unix group. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
150 |
|
28913 | 151 |
Sharing a locally modified clone then works as follows, using your |
152 |
user name instead of "wenzelm": |
|
153 |
||
51072 | 154 |
hg out ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
155 |
|
28913 | 156 |
In fact, the "out" or "outgoing" command performs only a dry run: it |
157 |
displays the changesets that would get published. An actual "push", |
|
158 |
with a lasting effect on the Isabelle repository, works like this: |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
159 |
|
51072 | 160 |
hg push ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle |
28913 | 161 |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
162 |
|
40601 | 163 |
Default paths for push and pull can be configured in |
164 |
isabelle/.hg/hgrc, for example: |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
165 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
166 |
[paths] |
51072 | 167 |
default = ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
168 |
|
28913 | 169 |
Now "hg pull" or "hg push" will use that shared file space, unless a |
170 |
different URL is specified explicitly. |
|
171 |
||
172 |
When cloning a repository, the default path is set to the initial |
|
173 |
source URL. So we could have cloned via that ssh URL in the first |
|
174 |
place, to get exactly to the same point: |
|
175 |
||
51072 | 176 |
hg clone ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
177 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
178 |
|
40601 | 179 |
Simple merges |
180 |
------------- |
|
30182 | 181 |
|
182 |
The main idea of Mercurial is to let individual users produce |
|
183 |
independent branches of development first, but merge with others |
|
184 |
frequently. The basic hg merge operation is more general than |
|
185 |
required for the mode of operation with a shared pull/push area. The |
|
40601 | 186 |
"fetch" extension accommodates this case nicely, automating trivial |
30182 | 187 |
merges and requiring manual intervention for actual conflicts only. |
188 |
||
40601 | 189 |
The fetch extension can be configured via $HOME/.hgrc like this: |
30182 | 190 |
|
191 |
[extensions] |
|
192 |
hgext.fetch = |
|
193 |
||
194 |
[defaults] |
|
195 |
fetch = -m "merged" |
|
196 |
||
40601 | 197 |
To keep merges semantically trivial and prevent genuine merge |
198 |
conflicts or lost updates, it is essential to observe to following |
|
199 |
general discipline wrt. the public Isabelle push area: |
|
200 |
||
201 |
* Before editing, pull or fetch the latest version. |
|
202 |
||
203 |
* Accumulate private commits for a maximum of 1-3 days. |
|
204 |
||
205 |
* Start publishing again by pull or fetch, which normally produces |
|
206 |
local merges. |
|
207 |
||
50281
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
208 |
* Test the merged result, e.g. like this: |
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
209 |
|
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
210 |
isabelle build -a |
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
211 |
|
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
212 |
* Push back in real time. |
40601 | 213 |
|
214 |
Piling private changes and public merges longer than 0.5-2 hours is |
|
215 |
apt to produce some mess when pushing eventually! |
|
30182 | 216 |
|
50281
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
217 |
The pull-test-push cycle should not be repeated too fast, to avoid |
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
218 |
delaying others from doing the same concurrently. |
cbba16084784
further update and clarification of the all-important README_REPOSITORY;
wenzelm
parents:
49443
diff
changeset
|
219 |
|
30182 | 220 |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
221 |
Content discipline |
29481 | 222 |
------------------ |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
223 |
|
40601 | 224 |
The following principles should be kept in mind when producing |
225 |
changesets that are meant to be published at some point. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
226 |
|
40601 | 227 |
* The author of changes needs to be properly identified, using |
228 |
[ui]username configuration as described above. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
229 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
230 |
While Mercurial also provides means for signed changesets, we want |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
231 |
to keep things simple and trust that users specify their identity |
40601 | 232 |
correctly (and uniquely). |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
233 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
234 |
* The history of sources is an integral part of the sources |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
235 |
themselves. This means that private experiments and branches |
40601 | 236 |
should not be published by accident. Named branches are not |
237 |
allowed on the public version. Note that old SVN-style branching |
|
238 |
is replaced by regular repository clones in Mercurial. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
239 |
|
40601 | 240 |
Exchanging local experiments with some other users can be done |
241 |
directly on peer-to-peer basis, without affecting the central |
|
242 |
pull/push area. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
243 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
244 |
* Log messages are an integral part of the history of sources. |
40601 | 245 |
Other people will have to inspect them routinely, to understand |
246 |
why things have been done in a certain way at some point. |
|
247 |
||
248 |
Authors of log entries should be aware that published changes are |
|
249 |
actually read. The main point is not to announce novelties, but |
|
250 |
to describe faithfully what has been done, and provide some clues |
|
251 |
about the motivation behind it. The main recipient is someone who |
|
252 |
needs to understand the change in the distant future to isolate |
|
51502 | 253 |
problems. Sometimes it is helpful to reference past changes |
254 |
formally via changeset ids in the log entry. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
255 |
|
40601 | 256 |
* The standard changelog entry format of the Isabelle repository |
51502 | 257 |
admits several (somehow related) items to be rolled into one |
40601 | 258 |
changeset. Each item is then described on a separate line that |
259 |
may become longer as screen line and is terminated by punctuation. |
|
260 |
These lines are roughly ordered by importance. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
261 |
|
40601 | 262 |
This format conforms to established Isabelle tradition. In |
263 |
contrast, the default of Mercurial prefers a single headline |
|
264 |
followed by a long body text. The reason for that is a somewhat |
|
265 |
different development model of typical "distributed" projects, |
|
266 |
where external changes pass through a hierarchy of reviewers and |
|
267 |
maintainers, until they end up in some authoritative repository. |
|
268 |
Isabelle changesets can be more spontaneous, growing from the |
|
269 |
bottom-up. |
|
270 |
||
67744 | 271 |
The web style of https://isabelle.in.tum.de/repos/isabelle |
40601 | 272 |
accommodates the Isabelle changelog format. Note that multiple |
273 |
lines will sometimes display as a single paragraph in HTML, so |
|
274 |
some terminating punctuation is required. Do not squeeze multiple |
|
275 |
items on the same line in the original text! |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
276 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
277 |
|
51502 | 278 |
Testing of changes (before push) |
279 |
-------------------------------- |
|
48497
ba61aceaa18a
some updates on "Building a repository version of Isabelle";
wenzelm
parents:
47449
diff
changeset
|
280 |
|
51502 | 281 |
The integrity of the standard pull/push area of Isabelle needs the be |
282 |
preserved at all time. This means that a complete test with default |
|
283 |
configuration needs to be finished successfully before push. If the |
|
284 |
preparation of the push involves a pull/merge phase, its result needs |
|
285 |
to covered by the test as well. |
|
28908 | 286 |
|
51502 | 287 |
There are several possibilities to perform the test, e.g. using the |
288 |
Isabelle testboard at TUM. In contrast, the subsequent command-line |
|
289 |
examples are for tests on the local machine: |
|
48844 | 290 |
|
51502 | 291 |
./bin/isabelle build -a #regular test |
48844 | 292 |
|
63985 | 293 |
./bin/isabelle build -a -o document=pdf #test with document preparation (optional) |
48844 | 294 |
|
51502 | 295 |
./bin/isabelle build -a -j2 -o threads=4 #test on multiple cores (example) |
48497
ba61aceaa18a
some updates on "Building a repository version of Isabelle";
wenzelm
parents:
47449
diff
changeset
|
296 |
|
51502 | 297 |
See also the chapter on Isabelle sessions and build management in the |
66753 | 298 |
"system" manual. The build option -S is particularly useful for quick |
299 |
tests of individual commits, e.g. for each step of a longer chain of |
|
300 |
changes, but the final push always requires a full test as above! |
|
48986
037d32448e29
update on "isabelle build" and "isabelle build_doc";
wenzelm
parents:
48855
diff
changeset
|
301 |
|
51502 | 302 |
Note that implicit dependencies on Isabelle components are specified |
303 |
via catalog files in $ISABELLE_HOME/Admin/components/ as part of the |
|
304 |
Mercurial history. This allows to bisect over a range of Isabelle |
|
305 |
versions while references to the contributing components change |
|
306 |
accordingly. Recall that "isabelle components -a" updates the local |
|
307 |
component store monotonically according to that information, and thus |
|
308 |
resolves missing components. |