Important notes on Mercurial repository access for Isabelle

===========================================================

Preamble

--------

Mercurial http://www.selenic.com/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

this:

  hg clone http://isabelle.in.tum.de/repos/isabelle

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

changesets.

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

book http://hgbook.red-bean.com/

Shared pull/push access

=======================

The entry point http://isabelle.in.tum.de/repos/isabelle 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,

atbroy100).

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

http://isabelle.in.tum.de/repos/isabelle is 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

configuration.

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 RSS/Atom 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.

Building Isabelle from the repository version

=============================================

Compared to a proper distribution or development snapshot, a

repository version of Isabelle lacks proper version identifiers in

various places, and some components produced by Admin/build.  After

applying that script with suitable options, the regular user

instructions for building and running Isabelle from sources apply.

Needless to say, the results from the build process must not be

committed back into the repository!

Makarius 29-Nov-2008