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