# HG changeset patch # User wenzelm # Date 1227974968 -3600 # Node ID 1a470f95ef18f4cbcf4cdc9267f0fca76b4fd0a0 # Parent 5f568bfc58d71e654eb46edbc0d50a8acd9ae443 Important notes on Mercurial repository access for Isabelle. diff -r 5f568bfc58d7 -r 1a470f95ef18 README_REPOSITORY --- /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 +=========================================================== + +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 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 +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 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