Important notes on Mercurial repository access for Isabelle.
Sat, 29 Nov 2008 17:09:28 +0100
changeset 28907 1a470f95ef18
parent 28906 5f568bfc58d7
child 28908 4571302e1594
Important notes on Mercurial repository access for Isabelle.
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/README_REPOSITORY	Sat Nov 29 17:09:28 2008 +0100
@@ -0,0 +1,177 @@
+Important notes on Mercurial repository access for Isabelle
+Mercurial belongs to a new generation
+of source code management systems, following the paradigm of
+"distributed version control".  Compared to the old centralized model
+of CVS/SVN, this gives considerable more power and freedom in
+organizing the flow of changes, both between individual developers and
+designated pull/push areas that are shared with others.
+More power for the user also means more responsibility!  Due to its
+decentralized nature, changesets that have been published once,
+e.g. via push to a shared repository that is visible on the net,
+cannot be easily retracted from the public again.  Regular Mercurial
+operations are strictly monotonic, where changset transactions are
+only added, but never deleted.  There are special tools to "repair"
+individual repositories via non-monotonic actions, but this does not
+yet retrieve unwanted changesets that have escaped into the public.
+Only global operations like pull/push, unbundle/bundle etc. fall into
+this critical category; incoming/outgoing or in/out may help to
+inspect changesets before exchanging them globally.  Anything else in
+Mercurial is local to the user's repository clone (including
+commit/update/merge etc.) and is in fact much simpler and safer to use
+than the corresponding operations of CVS or SVN.
+Initial configuration
+Never use any Mercurial version before 1.0!  At the moment, versions
+1.0, 1.0.1 and 1.0.2 all work equally well.
+The public pull area of the Isabelle repository can be cloned like
+  hg clone
+This will create a local directory "isabelle", unless an alternative
+name is specified.  The full repository meta-data and history of
+changes is in isabelle/.hg; local configuration for this clone can be
+added to isabelle/.hg/hgrc, but note that hgrc files are never copied
+by another clone operation!
+There is also ~/.hgrc for per-user Mercurial configuration.  The
+initial configuration should include at least an entry to identify
+yourself.  For example, something like this in /home/wenzelm/.hgrc:
+  [ui]
+  username = wenzelm
+Failing to configure the username correctly makes the system invent
+funny machine names that may persist eternally in the flow of
+In principle, user names can be chosen freely, but for longterm
+committers of the Isabelle repository the obvious choice is to keep
+with the old CVS naming scheme.
+There are other useful configuration to go into ~/.hgrc, e.g. defaults
+for common commands:
+  [defaults]
+  log = -l 10
+The next example shows how to install some Mercurial extension:
+  [extensions]
+  hgext.graphlog =
+Now the additional glog command will be available.
+See also the fine documentation for further details, especially the
+Shared pull/push access
+The entry point is world
+readable, both via plain web browsing and the hg client as described
+above.  Anybody can produce a clone, change it arbitrarily, and then
+use regular mechanisms of Mercurial to report changes "upstream", say
+via e-mail to someone with write access to that file space.  It is
+also quite easy to publish changed clones again on the web, using hg
+serve, or the hgweb.cgi or hgwebdir.cgi scripts that are included in
+the Mercurial distribution.
+This downstream/upstream mode of operation is quite common in the
+distributed version control community, and works well for occasional
+changes produced by anybody out there.  Of course, upstream
+maintainers need to review and moderate changes being proposed, before
+pushing anything onto the official Isabelle repository at TUM.
+Direct pull/push access requires an account at TUM, with properly
+configured ssh access to the local machines (e.g. macbroy20,
+The simple wrapper script /home/isabelle/mercurial/bin/hg provides a
+uniform view on the different Linux installations on the local
+network.  Thus it is advisable to add that directory to the shell PATH
+of the account at TUM:
+  PATH="/home/isabelle/mercurial/bin:$PATH"
+Now a clone of the shared push/pull area can be produced like this,
+using your user name instead of "wenzelm":
+  hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
+In fact, the only difference to the previous clone of
+ will be a different default
+pull/push path in isabelle/.hg/hgrc:
+  [paths]
+  default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
+This means an earlier pull-only clone can be changed into a pull/push
+version by editing this single line of the internal repository
+Content discipline
+Old-style centralized version control is occasionally compared with a
+"library where everybody scribbles into the books".  Or seen the other
+way round, the centralized model discourages individual
+experimentation (with local branches etc.), because everything is
+forced to happen on a shared file space.  With Mercurial, arbitrary
+variations on local clones are no problem, but care is required again
+when publishing changes eventually.
+The following principles should be kept in mind when producing
+changesets that might become public at some point.
+  * The author of changes should be properly identified, using
+    ui/username configuration as described above.
+    While Mercurial also provides means for signed changesets, we want
+    to keep things simple and trust that users specify their identity
+    correctly.
+  * The history of sources is an integral part of the sources
+    themselves.  This means that private experiments and branches
+    should not be published, unless they are really meant to become
+    universally available.
+    Note that exchanging local experiments with some other users can
+    be done directly on peer-to-peer basis, without affecting the
+    central pull/push area.
+  * Log messages are an integral part of the history of sources.
+    Other users will have to look there eventually, to understand why
+    things have been done in a certain way at some point.
+    Mercurial provides nice web presentation of incoming changes with
+    a digest of log entries; this also includes Atom/RSS news feeds.
+    Users should be aware that others will actually read what is
+    written into log messages.
+    The usual changelog presentation style for the Isabelle repository
+    admits log entries that consist of several lines, but without the
+    special head line that is used in Mercurial projects elsewhere.
+    Since some display styles strip newlines from text, it is
+    advisable to separate lines via punctuation, and not rely on
+    two-dimensional presentation too much.
+Makarius 29-Nov-2008