|
1 Important notes on Mercurial repository access for Isabelle |
|
2 =========================================================== |
|
3 |
|
4 Preamble |
|
5 -------- |
|
6 |
|
7 Mercurial http://www.selenic.com/mercurial belongs to a new generation |
|
8 of source code management systems, following the paradigm of |
|
9 "distributed version control". Compared to the old centralized model |
|
10 of CVS/SVN, this gives considerable more power and freedom in |
|
11 organizing the flow of changes, both between individual developers and |
|
12 designated pull/push areas that are shared with others. |
|
13 |
|
14 More power for the user also means more responsibility! Due to its |
|
15 decentralized nature, changesets that have been published once, |
|
16 e.g. via push to a shared repository that is visible on the net, |
|
17 cannot be easily retracted from the public again. Regular Mercurial |
|
18 operations are strictly monotonic, where changset transactions are |
|
19 only added, but never deleted. There are special tools to "repair" |
|
20 individual repositories via non-monotonic actions, but this does not |
|
21 yet retrieve unwanted changesets that have escaped into the public. |
|
22 |
|
23 Only global operations like pull/push, unbundle/bundle etc. fall into |
|
24 this critical category; incoming/outgoing or in/out may help to |
|
25 inspect changesets before exchanging them globally. Anything else in |
|
26 Mercurial is local to the user's repository clone (including |
|
27 commit/update/merge etc.) and is in fact much simpler and safer to use |
|
28 than the corresponding operations of CVS or SVN. |
|
29 |
|
30 |
|
31 Initial configuration |
|
32 ===================== |
|
33 |
|
34 Never use any Mercurial version before 1.0! At the moment, versions |
|
35 1.0, 1.0.1 and 1.0.2 all work equally well. |
|
36 |
|
37 |
|
38 The public pull area of the Isabelle repository can be cloned like |
|
39 this: |
|
40 |
|
41 hg clone http://isabelle.in.tum.de/repos/isabelle |
|
42 |
|
43 This will create a local directory "isabelle", unless an alternative |
|
44 name is specified. The full repository meta-data and history of |
|
45 changes is in isabelle/.hg; local configuration for this clone can be |
|
46 added to isabelle/.hg/hgrc, but note that hgrc files are never copied |
|
47 by another clone operation! |
|
48 |
|
49 There is also ~/.hgrc for per-user Mercurial configuration. The |
|
50 initial configuration should include at least an entry to identify |
|
51 yourself. For example, something like this in /home/wenzelm/.hgrc: |
|
52 |
|
53 [ui] |
|
54 username = wenzelm |
|
55 |
|
56 Failing to configure the username correctly makes the system invent |
|
57 funny machine names that may persist eternally in the flow of |
|
58 changesets. |
|
59 |
|
60 In principle, user names can be chosen freely, but for longterm |
|
61 committers of the Isabelle repository the obvious choice is to keep |
|
62 with the old CVS naming scheme. |
|
63 |
|
64 |
|
65 There are other useful configuration to go into ~/.hgrc, e.g. defaults |
|
66 for common commands: |
|
67 |
|
68 [defaults] |
|
69 log = -l 10 |
|
70 |
|
71 The next example shows how to install some Mercurial extension: |
|
72 |
|
73 [extensions] |
|
74 hgext.graphlog = |
|
75 |
|
76 Now the additional glog command will be available. |
|
77 |
|
78 |
|
79 See also the fine documentation for further details, especially the |
|
80 book http://hgbook.red-bean.com/ |
|
81 |
|
82 |
|
83 Shared pull/push access |
|
84 ======================= |
|
85 |
|
86 The entry point http://isabelle.in.tum.de/repos/isabelle is world |
|
87 readable, both via plain web browsing and the hg client as described |
|
88 above. Anybody can produce a clone, change it arbitrarily, and then |
|
89 use regular mechanisms of Mercurial to report changes "upstream", say |
|
90 via e-mail to someone with write access to that file space. It is |
|
91 also quite easy to publish changed clones again on the web, using hg |
|
92 serve, or the hgweb.cgi or hgwebdir.cgi scripts that are included in |
|
93 the Mercurial distribution. |
|
94 |
|
95 This downstream/upstream mode of operation is quite common in the |
|
96 distributed version control community, and works well for occasional |
|
97 changes produced by anybody out there. Of course, upstream |
|
98 maintainers need to review and moderate changes being proposed, before |
|
99 pushing anything onto the official Isabelle repository at TUM. |
|
100 |
|
101 |
|
102 Direct pull/push access requires an account at TUM, with properly |
|
103 configured ssh access to the local machines (e.g. macbroy20, |
|
104 atbroy100). |
|
105 |
|
106 The simple wrapper script /home/isabelle/mercurial/bin/hg provides a |
|
107 uniform view on the different Linux installations on the local |
|
108 network. Thus it is advisable to add that directory to the shell PATH |
|
109 of the account at TUM: |
|
110 |
|
111 PATH="/home/isabelle/mercurial/bin:$PATH" |
|
112 |
|
113 Now a clone of the shared push/pull area can be produced like this, |
|
114 using your user name instead of "wenzelm": |
|
115 |
|
116 hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle |
|
117 |
|
118 In fact, the only difference to the previous clone of |
|
119 http://isabelle.in.tum.de/repos/isabelle will be a different default |
|
120 pull/push path in isabelle/.hg/hgrc: |
|
121 |
|
122 [paths] |
|
123 default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle |
|
124 |
|
125 This means an earlier pull-only clone can be changed into a pull/push |
|
126 version by editing this single line of the internal repository |
|
127 configuration. |
|
128 |
|
129 |
|
130 Content discipline |
|
131 ================== |
|
132 |
|
133 Old-style centralized version control is occasionally compared with a |
|
134 "library where everybody scribbles into the books". Or seen the other |
|
135 way round, the centralized model discourages individual |
|
136 experimentation (with local branches etc.), because everything is |
|
137 forced to happen on a shared file space. With Mercurial, arbitrary |
|
138 variations on local clones are no problem, but care is required again |
|
139 when publishing changes eventually. |
|
140 |
|
141 The following principles should be kept in mind when producing |
|
142 changesets that might become public at some point. |
|
143 |
|
144 * The author of changes should be properly identified, using |
|
145 ui/username configuration as described above. |
|
146 |
|
147 While Mercurial also provides means for signed changesets, we want |
|
148 to keep things simple and trust that users specify their identity |
|
149 correctly. |
|
150 |
|
151 * The history of sources is an integral part of the sources |
|
152 themselves. This means that private experiments and branches |
|
153 should not be published, unless they are really meant to become |
|
154 universally available. |
|
155 |
|
156 Note that exchanging local experiments with some other users can |
|
157 be done directly on peer-to-peer basis, without affecting the |
|
158 central pull/push area. |
|
159 |
|
160 * Log messages are an integral part of the history of sources. |
|
161 Other users will have to look there eventually, to understand why |
|
162 things have been done in a certain way at some point. |
|
163 |
|
164 Mercurial provides nice web presentation of incoming changes with |
|
165 a digest of log entries; this also includes Atom/RSS news feeds. |
|
166 Users should be aware that others will actually read what is |
|
167 written into log messages. |
|
168 |
|
169 The usual changelog presentation style for the Isabelle repository |
|
170 admits log entries that consist of several lines, but without the |
|
171 special head line that is used in Mercurial projects elsewhere. |
|
172 Since some display styles strip newlines from text, it is |
|
173 advisable to separate lines via punctuation, and not rely on |
|
174 two-dimensional presentation too much. |
|
175 |
|
176 |
|
177 Makarius 29-Nov-2008 |