author | huffman |
Thu, 23 Dec 2010 11:52:26 -0800 | |
changeset 41400 | 1a7557cc686a |
parent 40601 | 021278fdd0a8 |
child 47449 | 5e1482296b12 |
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 |
|
40601 | 4 |
Introduction |
5 |
------------ |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
6 |
|
40601 | 7 |
Mercurial http://www.selenic.com/mercurial belongs to the current |
8 |
generation of source code management systems that follow the so-called |
|
9 |
paradigm of "distributed version control". This is a terrific name |
|
10 |
for plain revision control without the legacy of CVS or SVN. See also |
|
11 |
http://hginit.com/ for an introduction to the main ideas. The |
|
12 |
Mercurial book http://hgbook.red-bean.com/ explains many more details. |
|
13 |
||
14 |
Mercurial offers great flexibility in organizing the flow of changes, |
|
15 |
both between individual developers and designated pull/push areas that |
|
16 |
are shared with others. This additional power demands some additional |
|
17 |
responsibility to maintain a certain development process that fits to |
|
18 |
a particular project. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
19 |
|
40601 | 20 |
Regular Mercurial operations are strictly monotonic, where changeset |
21 |
transactions are only added, but never deleted. There are special |
|
22 |
tools to manipulate repositories via non-monotonic actions (such as |
|
23 |
"rollback" or "strip"), but recovering from gross mistakes that have |
|
24 |
escaped into the public can be hard and embarrassing. It is much |
|
25 |
easier to inspect and amend changesets routinely before pushing. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
26 |
|
40601 | 27 |
The effect of the critical "pull" / "push" operations can be tested in |
28 |
a dry run via "incoming" / "outgoing". The "fetch" extension includes |
|
29 |
useful sanity checks beyond raw "pull" / "update" / "merge". Most |
|
30 |
other operations are local to the user's repository clone. This gives |
|
31 |
some freedom for experimentation without affecting anybody else. |
|
32 |
||
33 |
Mercurial provides nice web presentation of incoming changes with a |
|
34 |
digest of log entries; this also includes RSS/Atom news feeds. There |
|
35 |
are add-on browsers, notably hgtk that is part of the TortoiseHg |
|
36 |
distribution and works for generic Python/GTk platforms. The |
|
37 |
alternative "view" utility helps to inspect the semantic content of |
|
38 |
merge nodes. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
39 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
40 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
41 |
Initial configuration |
29481 | 42 |
--------------------- |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
43 |
|
28913 | 44 |
The official Isabelle repository can be cloned like this: |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
45 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
46 |
hg clone http://isabelle.in.tum.de/repos/isabelle |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
47 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
48 |
This will create a local directory "isabelle", unless an alternative |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
49 |
name is specified. The full repository meta-data and history of |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
50 |
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
|
51 |
added to isabelle/.hg/hgrc, but note that hgrc files are never copied |
40601 | 52 |
by another clone operation. |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
53 |
|
28917 | 54 |
|
28913 | 55 |
There is also $HOME/.hgrc for per-user Mercurial configuration. The |
40601 | 56 |
initial configuration requires at least an entry to identify yourself |
57 |
as follows: |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
58 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
59 |
[ui] |
40601 | 60 |
username = XXX |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
61 |
|
40601 | 62 |
Isabelle contributors are free to choose either a short "login name" |
63 |
(for accounts at TU Munich) or a "full name" -- with or without mail |
|
64 |
address. It is important to stick to this choice once and for all. |
|
65 |
The machine default that Mercurial produces for unspecified |
|
66 |
[ui]username is not appropriate. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
67 |
|
40601 | 68 |
Such configuration can be given in $HOME/.hgrc (for each home |
69 |
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
|
70 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
71 |
|
40601 | 72 |
Here are some further examples for hgrc. This is how to provide |
73 |
default options for common commands: |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
74 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
75 |
[defaults] |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
76 |
log = -l 10 |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
77 |
|
40601 | 78 |
This is how to configure some extension, which is called "graphlog" |
79 |
and provides the "glog" command: |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
80 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
81 |
[extensions] |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
82 |
hgext.graphlog = |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
83 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
84 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
85 |
Shared pull/push access |
29481 | 86 |
----------------------- |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
87 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
88 |
The entry point http://isabelle.in.tum.de/repos/isabelle is world |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
89 |
readable, both via plain web browsing and the hg client as described |
40601 | 90 |
above. Anybody can produce a clone, change it locally, and then use |
91 |
regular mechanisms of Mercurial to report changes upstream, say via |
|
92 |
mail to someone with write access to that file space. It is also |
|
93 |
quite easy to publish changed clones again on the web, using the |
|
94 |
ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts |
|
95 |
that are included in the Mercurial distribution, and send a "pull |
|
96 |
request" to someone else. There are also public hosting services for |
|
97 |
Mercurial repositories. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
98 |
|
28913 | 99 |
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
|
100 |
distributed version control community, and works well for occasional |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
101 |
changes produced by anybody out there. Of course, upstream |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
102 |
maintainers need to review and moderate changes being proposed, before |
40601 | 103 |
pushing anything onto the official Isabelle repository at TUM. Direct |
104 |
pushes are also reviewed routinely in a post-hoc fashion; everybody |
|
105 |
hooked on the main repository is called to keep an eye on incoming |
|
106 |
changes. In any case, changesets need to be understandable, at the |
|
107 |
time of writing and many years later. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
108 |
|
40601 | 109 |
Push access to the Isabelle repository requires an account at TUM, |
110 |
with properly configured ssh to the local machines (e.g. macbroy20, |
|
111 |
atbroy100). You also need to be a member of the "isabelle" Unix |
|
112 |
group. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
113 |
|
28913 | 114 |
Sharing a locally modified clone then works as follows, using your |
115 |
user name instead of "wenzelm": |
|
116 |
||
117 |
hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
118 |
|
28913 | 119 |
In fact, the "out" or "outgoing" command performs only a dry run: it |
120 |
displays the changesets that would get published. An actual "push", |
|
121 |
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
|
122 |
|
28913 | 123 |
hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle |
124 |
||
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
125 |
|
40601 | 126 |
Default paths for push and pull can be configured in |
127 |
isabelle/.hg/hgrc, for example: |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
128 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
129 |
[paths] |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
130 |
default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
131 |
|
28913 | 132 |
Now "hg pull" or "hg push" will use that shared file space, unless a |
133 |
different URL is specified explicitly. |
|
134 |
||
135 |
When cloning a repository, the default path is set to the initial |
|
136 |
source URL. So we could have cloned via that ssh URL in the first |
|
137 |
place, to get exactly to the same point: |
|
138 |
||
139 |
hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
140 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
141 |
|
40601 | 142 |
Simple merges |
143 |
------------- |
|
30182 | 144 |
|
145 |
The main idea of Mercurial is to let individual users produce |
|
146 |
independent branches of development first, but merge with others |
|
147 |
frequently. The basic hg merge operation is more general than |
|
148 |
required for the mode of operation with a shared pull/push area. The |
|
40601 | 149 |
"fetch" extension accommodates this case nicely, automating trivial |
30182 | 150 |
merges and requiring manual intervention for actual conflicts only. |
151 |
||
40601 | 152 |
The fetch extension can be configured via $HOME/.hgrc like this: |
30182 | 153 |
|
154 |
[extensions] |
|
155 |
hgext.fetch = |
|
156 |
||
157 |
[defaults] |
|
158 |
fetch = -m "merged" |
|
159 |
||
40601 | 160 |
To keep merges semantically trivial and prevent genuine merge |
161 |
conflicts or lost updates, it is essential to observe to following |
|
162 |
general discipline wrt. the public Isabelle push area: |
|
163 |
||
164 |
* Before editing, pull or fetch the latest version. |
|
165 |
||
166 |
* Accumulate private commits for a maximum of 1-3 days. |
|
167 |
||
168 |
* Start publishing again by pull or fetch, which normally produces |
|
169 |
local merges. |
|
170 |
||
171 |
* Test the merged result as usual and push back in real time. |
|
172 |
||
173 |
Piling private changes and public merges longer than 0.5-2 hours is |
|
174 |
apt to produce some mess when pushing eventually! |
|
30182 | 175 |
|
176 |
||
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
177 |
Content discipline |
29481 | 178 |
------------------ |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
179 |
|
40601 | 180 |
The following principles should be kept in mind when producing |
181 |
changesets that are meant to be published at some point. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
182 |
|
40601 | 183 |
* The author of changes needs to be properly identified, using |
184 |
[ui]username configuration as described above. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
185 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
186 |
While Mercurial also provides means for signed changesets, we want |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
187 |
to keep things simple and trust that users specify their identity |
40601 | 188 |
correctly (and uniquely). |
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
189 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
190 |
* The history of sources is an integral part of the sources |
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
191 |
themselves. This means that private experiments and branches |
40601 | 192 |
should not be published by accident. Named branches are not |
193 |
allowed on the public version. Note that old SVN-style branching |
|
194 |
is replaced by regular repository clones in Mercurial. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
195 |
|
40601 | 196 |
Exchanging local experiments with some other users can be done |
197 |
directly on peer-to-peer basis, without affecting the central |
|
198 |
pull/push area. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
199 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
200 |
* Log messages are an integral part of the history of sources. |
40601 | 201 |
Other people will have to inspect them routinely, to understand |
202 |
why things have been done in a certain way at some point. |
|
203 |
||
204 |
Authors of log entries should be aware that published changes are |
|
205 |
actually read. The main point is not to announce novelties, but |
|
206 |
to describe faithfully what has been done, and provide some clues |
|
207 |
about the motivation behind it. The main recipient is someone who |
|
208 |
needs to understand the change in the distant future to isolate |
|
209 |
problems. Sometimes it is helpful to reference past changes via |
|
210 |
changeset ids in the log entry. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
211 |
|
40601 | 212 |
* The standard changelog entry format of the Isabelle repository |
213 |
admits several (vaguely related) items to be rolled into one |
|
214 |
changeset. Each item is then described on a separate line that |
|
215 |
may become longer as screen line and is terminated by punctuation. |
|
216 |
These lines are roughly ordered by importance. |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
217 |
|
40601 | 218 |
This format conforms to established Isabelle tradition. In |
219 |
contrast, the default of Mercurial prefers a single headline |
|
220 |
followed by a long body text. The reason for that is a somewhat |
|
221 |
different development model of typical "distributed" projects, |
|
222 |
where external changes pass through a hierarchy of reviewers and |
|
223 |
maintainers, until they end up in some authoritative repository. |
|
224 |
Isabelle changesets can be more spontaneous, growing from the |
|
225 |
bottom-up. |
|
226 |
||
227 |
The web style of http://isabelle.in.tum.de/repos/isabelle/ |
|
228 |
accommodates the Isabelle changelog format. Note that multiple |
|
229 |
lines will sometimes display as a single paragraph in HTML, so |
|
230 |
some terminating punctuation is required. Do not squeeze multiple |
|
231 |
items on the same line in the original text! |
|
28907
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
232 |
|
1a470f95ef18
Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff
changeset
|
233 |
|
32361
141e5151b918
clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
wenzelm
parents:
30182
diff
changeset
|
234 |
Building a repository version of Isabelle |
141e5151b918
clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
wenzelm
parents:
30182
diff
changeset
|
235 |
----------------------------------------- |
28908 | 236 |
|
40601 | 237 |
Compared to a proper distribution or development snapshot, it is |
238 |
relatively hard to build from the raw repository version. Essential |
|
239 |
contributing components are missing and need to be reconstructed by |
|
240 |
running the Admin/build script by hand. Afterwards the main Isabelle |
|
241 |
system and logic images can be compiled via the toplevel ./build |
|
242 |
script. Note that the repository lacks some textual version |
|
243 |
identifiers in the sources and scripts; this implies some changed |
|
244 |
behavior when processing settings etc. |
|
28908 | 245 |
|
40601 | 246 |
There is no guarantee that the NEWS file is up to date at an arbitrary |
247 |
point in history. |