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