README_REPOSITORY
changeset 28907 1a470f95ef18
child 28908 4571302e1594
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/README_REPOSITORY	Sat Nov 29 17:09:28 2008 +0100
     1.3 @@ -0,0 +1,177 @@
     1.4 +Important notes on Mercurial repository access for Isabelle
     1.5 +===========================================================
     1.6 +
     1.7 +Preamble
     1.8 +--------
     1.9 +
    1.10 +Mercurial http://www.selenic.com/mercurial belongs to a new generation
    1.11 +of source code management systems, following the paradigm of
    1.12 +"distributed version control".  Compared to the old centralized model
    1.13 +of CVS/SVN, this gives considerable more power and freedom in
    1.14 +organizing the flow of changes, both between individual developers and
    1.15 +designated pull/push areas that are shared with others.
    1.16 +
    1.17 +More power for the user also means more responsibility!  Due to its
    1.18 +decentralized nature, changesets that have been published once,
    1.19 +e.g. via push to a shared repository that is visible on the net,
    1.20 +cannot be easily retracted from the public again.  Regular Mercurial
    1.21 +operations are strictly monotonic, where changset transactions are
    1.22 +only added, but never deleted.  There are special tools to "repair"
    1.23 +individual repositories via non-monotonic actions, but this does not
    1.24 +yet retrieve unwanted changesets that have escaped into the public.
    1.25 +
    1.26 +Only global operations like pull/push, unbundle/bundle etc. fall into
    1.27 +this critical category; incoming/outgoing or in/out may help to
    1.28 +inspect changesets before exchanging them globally.  Anything else in
    1.29 +Mercurial is local to the user's repository clone (including
    1.30 +commit/update/merge etc.) and is in fact much simpler and safer to use
    1.31 +than the corresponding operations of CVS or SVN.
    1.32 +
    1.33 +
    1.34 +Initial configuration
    1.35 +=====================
    1.36 +
    1.37 +Never use any Mercurial version before 1.0!  At the moment, versions
    1.38 +1.0, 1.0.1 and 1.0.2 all work equally well.
    1.39 +
    1.40 +
    1.41 +The public pull area of the Isabelle repository can be cloned like
    1.42 +this:
    1.43 +
    1.44 +  hg clone http://isabelle.in.tum.de/repos/isabelle
    1.45 +
    1.46 +This will create a local directory "isabelle", unless an alternative
    1.47 +name is specified.  The full repository meta-data and history of
    1.48 +changes is in isabelle/.hg; local configuration for this clone can be
    1.49 +added to isabelle/.hg/hgrc, but note that hgrc files are never copied
    1.50 +by another clone operation!
    1.51 +
    1.52 +There is also ~/.hgrc for per-user Mercurial configuration.  The
    1.53 +initial configuration should include at least an entry to identify
    1.54 +yourself.  For example, something like this in /home/wenzelm/.hgrc:
    1.55 +
    1.56 +  [ui]
    1.57 +  username = wenzelm
    1.58 +
    1.59 +Failing to configure the username correctly makes the system invent
    1.60 +funny machine names that may persist eternally in the flow of
    1.61 +changesets.
    1.62 +
    1.63 +In principle, user names can be chosen freely, but for longterm
    1.64 +committers of the Isabelle repository the obvious choice is to keep
    1.65 +with the old CVS naming scheme.
    1.66 +
    1.67 +
    1.68 +There are other useful configuration to go into ~/.hgrc, e.g. defaults
    1.69 +for common commands:
    1.70 +
    1.71 +  [defaults]
    1.72 +  log = -l 10
    1.73 +
    1.74 +The next example shows how to install some Mercurial extension:
    1.75 +
    1.76 +  [extensions]
    1.77 +  hgext.graphlog =
    1.78 +
    1.79 +Now the additional glog command will be available.
    1.80 +
    1.81 +
    1.82 +See also the fine documentation for further details, especially the
    1.83 +book http://hgbook.red-bean.com/
    1.84 +
    1.85 +
    1.86 +Shared pull/push access
    1.87 +=======================
    1.88 +
    1.89 +The entry point http://isabelle.in.tum.de/repos/isabelle is world
    1.90 +readable, both via plain web browsing and the hg client as described
    1.91 +above.  Anybody can produce a clone, change it arbitrarily, and then
    1.92 +use regular mechanisms of Mercurial to report changes "upstream", say
    1.93 +via e-mail to someone with write access to that file space.  It is
    1.94 +also quite easy to publish changed clones again on the web, using hg
    1.95 +serve, or the hgweb.cgi or hgwebdir.cgi scripts that are included in
    1.96 +the Mercurial distribution.
    1.97 +
    1.98 +This downstream/upstream mode of operation is quite common in the
    1.99 +distributed version control community, and works well for occasional
   1.100 +changes produced by anybody out there.  Of course, upstream
   1.101 +maintainers need to review and moderate changes being proposed, before
   1.102 +pushing anything onto the official Isabelle repository at TUM.
   1.103 +
   1.104 +
   1.105 +Direct pull/push access requires an account at TUM, with properly
   1.106 +configured ssh access to the local machines (e.g. macbroy20,
   1.107 +atbroy100).
   1.108 +
   1.109 +The simple wrapper script /home/isabelle/mercurial/bin/hg provides a
   1.110 +uniform view on the different Linux installations on the local
   1.111 +network.  Thus it is advisable to add that directory to the shell PATH
   1.112 +of the account at TUM:
   1.113 +
   1.114 +  PATH="/home/isabelle/mercurial/bin:$PATH"
   1.115 +
   1.116 +Now a clone of the shared push/pull area can be produced like this,
   1.117 +using your user name instead of "wenzelm":
   1.118 +
   1.119 +  hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   1.120 +
   1.121 +In fact, the only difference to the previous clone of
   1.122 +http://isabelle.in.tum.de/repos/isabelle will be a different default
   1.123 +pull/push path in isabelle/.hg/hgrc:
   1.124 +
   1.125 +  [paths]
   1.126 +  default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   1.127 +
   1.128 +This means an earlier pull-only clone can be changed into a pull/push
   1.129 +version by editing this single line of the internal repository
   1.130 +configuration.
   1.131 +
   1.132 +
   1.133 +Content discipline
   1.134 +==================
   1.135 +
   1.136 +Old-style centralized version control is occasionally compared with a
   1.137 +"library where everybody scribbles into the books".  Or seen the other
   1.138 +way round, the centralized model discourages individual
   1.139 +experimentation (with local branches etc.), because everything is
   1.140 +forced to happen on a shared file space.  With Mercurial, arbitrary
   1.141 +variations on local clones are no problem, but care is required again
   1.142 +when publishing changes eventually.
   1.143 +
   1.144 +The following principles should be kept in mind when producing
   1.145 +changesets that might become public at some point.
   1.146 +
   1.147 +  * The author of changes should be properly identified, using
   1.148 +    ui/username configuration as described above.
   1.149 +
   1.150 +    While Mercurial also provides means for signed changesets, we want
   1.151 +    to keep things simple and trust that users specify their identity
   1.152 +    correctly.
   1.153 +
   1.154 +  * The history of sources is an integral part of the sources
   1.155 +    themselves.  This means that private experiments and branches
   1.156 +    should not be published, unless they are really meant to become
   1.157 +    universally available.
   1.158 +
   1.159 +    Note that exchanging local experiments with some other users can
   1.160 +    be done directly on peer-to-peer basis, without affecting the
   1.161 +    central pull/push area.
   1.162 +
   1.163 +  * Log messages are an integral part of the history of sources.
   1.164 +    Other users will have to look there eventually, to understand why
   1.165 +    things have been done in a certain way at some point.
   1.166 +
   1.167 +    Mercurial provides nice web presentation of incoming changes with
   1.168 +    a digest of log entries; this also includes Atom/RSS news feeds.
   1.169 +    Users should be aware that others will actually read what is
   1.170 +    written into log messages.
   1.171 +
   1.172 +    The usual changelog presentation style for the Isabelle repository
   1.173 +    admits log entries that consist of several lines, but without the
   1.174 +    special head line that is used in Mercurial projects elsewhere.
   1.175 +    Since some display styles strip newlines from text, it is
   1.176 +    advisable to separate lines via punctuation, and not rely on
   1.177 +    two-dimensional presentation too much.
   1.178 +
   1.179 +
   1.180 +Makarius 29-Nov-2008