1 Important notes on Mercurial repository access for Isabelle
2 ===========================================================
7 1a. Linux and Mac OS X: ensure that Mercurial is installed
8 (see also http://www.selenic.com/mercurial)
10 1b. Windows: ensure that Cygwin64 with curl and Mercurial is installed
11 (see also http://www.cygwin.com)
13 2. Clone repository (bash shell commands):
15 hg clone http://isabelle.in.tum.de/repos/isabelle
19 ./bin/isabelle components -I
21 ./bin/isabelle components -a
23 ./bin/isabelle jedit -l HOL
25 ./bin/isabelle build -b HOL #optional: build session image manually
27 3. Update repository (bash shell commands):
33 ./bin/isabelle components -a
35 ./bin/isabelle jedit -l HOL
37 ./bin/isabelle jedit -b -f #optional: force fresh build of Isabelle/Scala
39 4. Access documentation (bash shell commands):
41 ./bin/isabelle build_doc -a
43 ./bin/isabelle doc system
49 Mercurial http://www.selenic.com/mercurial belongs to source code
50 management systems that follow the so-called paradigm of "distributed
51 version control". This means plain revision control without the
52 legacy of CVS or SVN (and without the extra complexity introduced by
53 git). See also http://hginit.com/ for an introduction to the main
54 ideas. The Mercurial book http://hgbook.red-bean.com/ explains many
57 Mercurial offers some flexibility in organizing the flow of changes,
58 both between individual developers and designated pull/push areas that
59 are shared with others. This additional freedom demands additional
60 responsibility to maintain a certain development process that fits to
63 Regular Mercurial operations are strictly monotonic, where changeset
64 transactions are only added, but never deleted or mutated. There are
65 special tools to manipulate repositories via non-monotonic actions
66 (such as "rollback" or "strip"), but recovering from gross mistakes
67 that have escaped into the public can be hard and embarrassing. It is
68 much easier to inspect and amend changesets routinely before pushing.
70 The effect of the critical "pull" / "push" operations can be tested in
71 a dry run via "incoming" / "outgoing". The "fetch" extension includes
72 useful sanity checks beyond raw "pull" / "update" / "merge", although
73 it has lost popularity in recent years. Most other operations are
74 local to the user's repository clone. This gives some freedom for
75 experimentation without affecting anybody else.
77 Mercurial provides nice web presentation of incoming changes with a
78 digest of log entries; this also includes RSS/Atom news feeds. There
79 are add-on history browsers such as "hg view" and TortoiseHg. Unlike
80 the default web view, some of these tools help to inspect the semantic
81 content of non-trivial merge nodes.
87 The main Isabelle repository can be cloned like this:
89 hg clone http://isabelle.in.tum.de/repos/isabelle
91 This will create a local directory "isabelle", unless an alternative
92 name is specified. The full repository meta-data and history of
93 changes is in isabelle/.hg; local configuration for this clone can be
94 added to isabelle/.hg/hgrc, but note that hgrc files are never copied
95 by another clone operation.
98 There is also $HOME/.hgrc for per-user Mercurial configuration. The
99 initial configuration requires at least an entry to identify yourself
105 Isabelle contributors are free to choose either a short "login name"
106 (for accounts at TU Munich) or a "full name" -- with or without mail
107 address. It is important to stick to this choice once and for all.
108 The machine default that Mercurial produces for unspecified
109 [ui]username is not appropriate.
111 Such configuration can be given in $HOME/.hgrc (for each home
112 directory on each machine) or in .hg/hgrc (for each repository clone).
115 Here are some further examples for hgrc. This is how to provide
116 default options for common commands:
121 This is how to configure some extension, which is called "graphlog"
122 and provides the "glog" command:
128 Shared pull/push access
129 -----------------------
131 The entry point http://isabelle.in.tum.de/repos/isabelle is world
132 readable, both via plain web browsing and the hg client as described
133 above. Anybody can produce a clone, change it locally, and then use
134 regular mechanisms of Mercurial to report changes upstream, say via
135 mail to someone with write access to that file space. It is also
136 quite easy to publish changed clones again on the web, using the
137 ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
138 that are included in the Mercurial distribution, and send a "pull
139 request" to someone else. There are also public hosting services for
140 Mercurial repositories, notably Bitbucket.
142 The downstream/upstream mode of operation is quite common in the
143 distributed version control community, and works well for occasional
144 changes produced by anybody out there. Of course, upstream
145 maintainers need to review and moderate changes being proposed, before
146 pushing anything onto the official Isabelle repository at TUM. Direct
147 pushes are also reviewed routinely in a post-hoc fashion; everybody
148 hooked on the main repository is called to keep an eye on incoming
149 changes. In any case, changesets need to be understandable, both at
150 the time of writing and many years later.
152 Push access to the Isabelle repository requires an account at TUM,
153 with properly configured ssh to isabelle-server.in.tum.de. You also
154 need to be a member of the "isabelle" Unix group.
156 Sharing a locally modified clone then works as follows, using your
157 user name instead of "wenzelm":
159 hg out ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
161 In fact, the "out" or "outgoing" command performs only a dry run: it
162 displays the changesets that would get published. An actual "push",
163 with a lasting effect on the Isabelle repository, works like this:
165 hg push ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
168 Default paths for push and pull can be configured in
169 isabelle/.hg/hgrc, for example:
172 default = ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
174 Now "hg pull" or "hg push" will use that shared file space, unless a
175 different URL is specified explicitly.
177 When cloning a repository, the default path is set to the initial
178 source URL. So we could have cloned via that ssh URL in the first
179 place, to get exactly to the same point:
181 hg clone ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
187 The main idea of Mercurial is to let individual users produce
188 independent branches of development first, but merge with others
189 frequently. The basic hg merge operation is more general than
190 required for the mode of operation with a shared pull/push area. The
191 "fetch" extension accommodates this case nicely, automating trivial
192 merges and requiring manual intervention for actual conflicts only.
194 The fetch extension can be configured via $HOME/.hgrc like this:
202 To keep merges semantically trivial and prevent genuine merge
203 conflicts or lost updates, it is essential to observe to following
204 general discipline wrt. the public Isabelle push area:
206 * Before editing, pull or fetch the latest version.
208 * Accumulate private commits for a maximum of 1-3 days.
210 * Start publishing again by pull or fetch, which normally produces
213 * Test the merged result, e.g. like this:
217 * Push back in real time.
219 Piling private changes and public merges longer than 0.5-2 hours is
220 apt to produce some mess when pushing eventually!
222 The pull-test-push cycle should not be repeated too fast, to avoid
223 delaying others from doing the same concurrently.
229 The following principles should be kept in mind when producing
230 changesets that are meant to be published at some point.
232 * The author of changes needs to be properly identified, using
233 [ui]username configuration as described above.
235 While Mercurial also provides means for signed changesets, we want
236 to keep things simple and trust that users specify their identity
237 correctly (and uniquely).
239 * The history of sources is an integral part of the sources
240 themselves. This means that private experiments and branches
241 should not be published by accident. Named branches are not
242 allowed on the public version. Note that old SVN-style branching
243 is replaced by regular repository clones in Mercurial.
245 Exchanging local experiments with some other users can be done
246 directly on peer-to-peer basis, without affecting the central
249 * Log messages are an integral part of the history of sources.
250 Other people will have to inspect them routinely, to understand
251 why things have been done in a certain way at some point.
253 Authors of log entries should be aware that published changes are
254 actually read. The main point is not to announce novelties, but
255 to describe faithfully what has been done, and provide some clues
256 about the motivation behind it. The main recipient is someone who
257 needs to understand the change in the distant future to isolate
258 problems. Sometimes it is helpful to reference past changes
259 formally via changeset ids in the log entry.
261 * The standard changelog entry format of the Isabelle repository
262 admits several (somehow related) items to be rolled into one
263 changeset. Each item is then described on a separate line that
264 may become longer as screen line and is terminated by punctuation.
265 These lines are roughly ordered by importance.
267 This format conforms to established Isabelle tradition. In
268 contrast, the default of Mercurial prefers a single headline
269 followed by a long body text. The reason for that is a somewhat
270 different development model of typical "distributed" projects,
271 where external changes pass through a hierarchy of reviewers and
272 maintainers, until they end up in some authoritative repository.
273 Isabelle changesets can be more spontaneous, growing from the
276 The web style of http://isabelle.in.tum.de/repos/isabelle/
277 accommodates the Isabelle changelog format. Note that multiple
278 lines will sometimes display as a single paragraph in HTML, so
279 some terminating punctuation is required. Do not squeeze multiple
280 items on the same line in the original text!
283 Testing of changes (before push)
284 --------------------------------
286 The integrity of the standard pull/push area of Isabelle needs the be
287 preserved at all time. This means that a complete test with default
288 configuration needs to be finished successfully before push. If the
289 preparation of the push involves a pull/merge phase, its result needs
290 to covered by the test as well.
292 There are several possibilities to perform the test, e.g. using the
293 Isabelle testboard at TUM. In contrast, the subsequent command-line
294 examples are for tests on the local machine:
296 ./bin/isabelle build -a #regular test
298 ./bin/isabelle build -a -o document=pdf #test with document preparation (optional)
300 ./bin/isabelle build -a -j2 -o threads=4 #test on multiple cores (example)
302 See also the chapter on Isabelle sessions and build management in the
303 "system" manual. The build option -S is particularly useful for quick
304 tests of individual commits, e.g. for each step of a longer chain of
305 changes, but the final push always requires a full test as above!
307 Note that implicit dependencies on Isabelle components are specified
308 via catalog files in $ISABELLE_HOME/Admin/components/ as part of the
309 Mercurial history. This allows to bisect over a range of Isabelle
310 versions while references to the contributing components change
311 accordingly. Recall that "isabelle components -a" updates the local
312 component store monotonically according to that information, and thus
313 resolves missing components.