--- /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