1 Important notes on Mercurial repository access for Isabelle
2 ===========================================================
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 or 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.
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 manipulate
20 individual repositories via non-monotonic actions, but this does not
21 yet retrieve any changesets that have escaped into the public by
24 Only global operations like "pull" and "push" fall into this critical
25 category. Note that "incoming" / "outgoing" allow to inspect
26 changesets before exchanging them globally. Anything else in
27 Mercurial is local to the user's repository clone (including "commit",
28 "update", "merge" etc.) and is in fact much simpler and safer to use
29 than the corresponding operations of CVS or SVN.
35 Always use Mercurial versions from the 1.0 or 1.1 branch, or later.
36 The old 0.9.x versions do not work in a multi-user environment with
40 The official Isabelle repository can be cloned like this:
42 hg clone http://isabelle.in.tum.de/repos/isabelle
44 This will create a local directory "isabelle", unless an alternative
45 name is specified. The full repository meta-data and history of
46 changes is in isabelle/.hg; local configuration for this clone can be
47 added to isabelle/.hg/hgrc, but note that hgrc files are never copied
48 by another clone operation!
51 There is also $HOME/.hgrc for per-user Mercurial configuration. The
52 initial configuration should include at least an entry to identify
53 yourself. For example, something like this in /home/wenzelm/.hgrc:
58 Of course, the user identity can be also configured in
59 isabelle/.hg/hgrc on per-repository basis. Failing to specify the
60 username correctly makes the system invent funny machine names that
61 may persist indefinitely in the public flow of changesets.
63 In principle, user names can be chosen freely, but for longterm
64 committers of the Isabelle repository the obvious choice is to keep
65 with the old CVS naming scheme. Others should use their regular "full
66 name"; including an email address is optional.
69 There are other useful configuration to go into $HOME/.hgrc,
70 e.g. defaults for common commands:
75 The next example shows how to install some Mercurial extension:
80 Now the additional glog command will be available.
83 See also the fine documentation for further details, especially the
84 book http://hgbook.red-bean.com/
86 There is also a nice tutorial at http://hginit.com/
89 Shared pull/push access
90 -----------------------
92 The entry point http://isabelle.in.tum.de/repos/isabelle is world
93 readable, both via plain web browsing and the hg client as described
94 above. Anybody can produce a clone, change it arbitrarily, and then
95 use regular mechanisms of Mercurial to report changes upstream, say
96 via e-mail to someone with write access to that file space. It is
97 also quite easy to publish changed clones again on the web, using the
98 adhoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
99 that are included in the Mercurial distribution.
101 The downstream/upstream mode of operation is quite common in the
102 distributed version control community, and works well for occasional
103 changes produced by anybody out there. Of course, upstream
104 maintainers need to review and moderate changes being proposed, before
105 pushing anything onto the official Isabelle repository at TUM.
108 Write access to the Isabelle repository requires an account at TUM,
109 with properly configured ssh access to the local machines
110 (e.g. macbroy20, atbroy100). You also need to be a member of the
111 "isabelle" Unix group.
113 Sharing a locally modified clone then works as follows, using your
114 user name instead of "wenzelm":
116 hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
118 In fact, the "out" or "outgoing" command performs only a dry run: it
119 displays the changesets that would get published. An actual "push",
120 with a lasting effect on the Isabelle repository, works like this:
122 hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
125 Default paths for push and pull can be configure in isabelle/.hg/hgrc,
129 default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
131 Now "hg pull" or "hg push" will use that shared file space, unless a
132 different URL is specified explicitly.
134 When cloning a repository, the default path is set to the initial
135 source URL. So we could have cloned via that ssh URL in the first
136 place, to get exactly to the same point:
138 hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
144 The main idea of Mercurial is to let individual users produce
145 independent branches of development first, but merge with others
146 frequently. The basic hg merge operation is more general than
147 required for the mode of operation with a shared pull/push area. The
148 hg fetch extension accommodates this case nicely, automating trivial
149 merges and requiring manual intervention for actual conflicts only.
151 The fetch extension can be configured via the user's ~/.hgrc like
160 Note that the potential for merge conflicts can be greatly reduced by
161 doing "hg fetch" before any starting local changes!
167 Old-style centralized version control is occasionally compared to "a
168 library where everybody scribbles into the books". Or seen the other
169 way round, the centralized model discourages individual
170 experimentation (with local branches etc.), because everything is
171 forced to happen on a shared file space. With Mercurial, arbitrary
172 variations on local clones are no problem, but care is required again
173 when publishing changes eventually.
175 The following principles should be kept in mind when producing
176 changesets that might become public at some point.
178 * The author of changes should be properly identified, using
179 ui/username configuration as described above.
181 While Mercurial also provides means for signed changesets, we want
182 to keep things simple and trust that users specify their identity
185 * The history of sources is an integral part of the sources
186 themselves. This means that private experiments and branches
187 should not be published, unless they are really meant to become
188 universally available.
190 Note that exchanging local experiments with some other users can
191 be done directly on peer-to-peer basis, without affecting the
192 central pull/push area.
194 * Log messages are an integral part of the history of sources.
195 Other users will have to look there eventually, to understand why
196 things have been done in a certain way at some point.
198 Mercurial provides nice web presentation of incoming changes with
199 a digest of log entries; this also includes RSS/Atom news feeds.
200 Users should be aware that others will actually read what is
201 written into log messages. There are also add-on browsers,
202 notably hgtk that is part of the TortoiseHg distribution and works
203 for generic Python/GTk platforms.
205 The usual changelog presentation style for the Isabelle repository
206 admits log entries that consist of several lines, but without the
207 special headline that is used in Mercurial projects elsewhere.
208 Since some display styles strip newlines from text, it is
209 advisable to separate lines via punctuation, and not rely on
210 two-dimensional presentation too much.
213 Building a repository version of Isabelle
214 -----------------------------------------
216 Compared to a proper distribution or development snapshot, a
217 repository version of Isabelle lacks textual version identifiers in
218 some sources and scripts, and various components produced by
219 Admin/build are missing. After applying that script with suitable
220 arguments, the regular user instructions for building and running
221 Isabelle from sources apply.
223 Needless to say, the results from the build process must not be added