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