Important notes on Mercurial repository access for Isabelle===========================================================Preamble--------Mercurial http://www.selenic.com/mercurial belongs to a new generationof source code management systems, following the paradigm of"distributed version control". Compared to the old centralized modelof CVS or SVN, this gives considerable more power and freedom inorganizing the flow of changes, both between individual developers anddesignated pull/push areas that are shared with others.More power for the user also means more responsibility! Due to itsdecentralized 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 Mercurialoperations are strictly monotonic, where changset transactions areonly added, but never deleted. There are special tools to manipulateindividual repositories via non-monotonic actions, but this does notyet retrieve any changesets that have escaped into the public byaccident.Only global operations like "pull" and "push" fall into this criticalcategory. Note that "incoming" / "outgoing" allow to inspectchangesets before exchanging them globally. Anything else inMercurial is local to the user's repository clone (including "commit","update", "merge" etc.) and is in fact much simpler and safer to usethan the corresponding operations of CVS or SVN.Initial configuration---------------------Always use Mercurial version 1.0 or later, such as 1.0.1 or 1.0.2.The old 0.9.x versions do not work in a multi-user environment withshared file spaces.The official Isabelle repository can be cloned like this: hg clone http://isabelle.in.tum.de/repos/isabelleThis will create a local directory "isabelle", unless an alternativename is specified. The full repository meta-data and history ofchanges is in isabelle/.hg; local configuration for this clone can beadded to isabelle/.hg/hgrc, but note that hgrc files are never copiedby another clone operation!There is also $HOME/.hgrc for per-user Mercurial configuration. Theinitial configuration should include at least an entry to identifyyourself. For example, something like this in /home/wenzelm/.hgrc: [ui] username = wenzelmOf course, the user identity can be also configured inisabelle/.hg/hgrc on per-repository basis. Failing to specify theusername correctly makes the system invent funny machine names thatmay persist indefinitely in the public flow of changesets.In principle, user names can be chosen freely, but for longtermcommitters of the Isabelle repository the obvious choice is to keepwith the old CVS naming scheme.There are other useful configuration to go into $HOME/.hgrc,e.g. defaults for common commands: [defaults] log = -l 10The 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 thebook http://hgbook.red-bean.com/Shared pull/push access-----------------------The entry point http://isabelle.in.tum.de/repos/isabelle is worldreadable, both via plain web browsing and the hg client as describedabove. Anybody can produce a clone, change it arbitrarily, and thenuse regular mechanisms of Mercurial to report changes upstream, sayvia e-mail to someone with write access to that file space. It isalso quite easy to publish changed clones again on the web, using theadhoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scriptsthat are included in the Mercurial distribution.The downstream/upstream mode of operation is quite common in thedistributed version control community, and works well for occasionalchanges produced by anybody out there. Of course, upstreammaintainers need to review and moderate changes being proposed, beforepushing anything onto the official Isabelle repository at TUM.Write access to the Isabelle repository requires an account at TUM,with properly configured ssh access to the local machines(e.g. macbroy20, atbroy100). You also need to be a member of the"isabelle" Unix group.Sharing a locally modified clone then works as follows, using youruser name instead of "wenzelm": hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelleIn fact, the "out" or "outgoing" command performs only a dry run: itdisplays the changesets that would get published. An actual "push",with a lasting effect on the Isabelle repository, works like this: hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelleDefault paths for push and pull can be configure in isabelle/.hg/hgrc,for example: [paths] default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelleNow "hg pull" or "hg push" will use that shared file space, unless adifferent URL is specified explicitly.When cloning a repository, the default path is set to the initialsource URL. So we could have cloned via that ssh URL in the firstplace, to get exactly to the same point: hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelleContent discipline------------------Old-style centralized version control is occasionally compared to "alibrary where everybody scribbles into the books". Or seen the otherway round, the centralized model discourages individualexperimentation (with local branches etc.), because everything isforced to happen on a shared file space. With Mercurial, arbitraryvariations on local clones are no problem, but care is required againwhen publishing changes eventually.The following principles should be kept in mind when producingchangesets 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 headline 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, arepository version of Isabelle lacks textual version identifiers insome sources and scripts, and various components produced byAdmin/build are missing. After applying that script with suitablearguments, the regular user instructions for building and runningIsabelle from sources apply.Needless to say, the results from the build process must not be addedto the repository!Makarius 30-Nov-2008