README_REPOSITORY
author wenzelm
Sat Nov 29 17:09:28 2008 +0100 (2008-11-29)
changeset 28907 1a470f95ef18
child 28908 4571302e1594
permissions -rw-r--r--
Important notes on Mercurial repository access for Isabelle.
     1 Important notes on Mercurial repository access for Isabelle
     2 ===========================================================
     3 
     4 Preamble
     5 --------
     6 
     7 Mercurial http://www.selenic.com/mercurial belongs to a new generation
     8 of source code management systems, following the paradigm of
     9 "distributed version control".  Compared to the old centralized model
    10 of CVS/SVN, this gives considerable more power and freedom in
    11 organizing the flow of changes, both between individual developers and
    12 designated pull/push areas that are shared with others.
    13 
    14 More power for the user also means more responsibility!  Due to its
    15 decentralized nature, changesets that have been published once,
    16 e.g. via push to a shared repository that is visible on the net,
    17 cannot be easily retracted from the public again.  Regular Mercurial
    18 operations are strictly monotonic, where changset transactions are
    19 only added, but never deleted.  There are special tools to "repair"
    20 individual repositories via non-monotonic actions, but this does not
    21 yet retrieve unwanted changesets that have escaped into the public.
    22 
    23 Only global operations like pull/push, unbundle/bundle etc. fall into
    24 this critical category; incoming/outgoing or in/out may help to
    25 inspect changesets before exchanging them globally.  Anything else in
    26 Mercurial is local to the user's repository clone (including
    27 commit/update/merge etc.) and is in fact much simpler and safer to use
    28 than the corresponding operations of CVS or SVN.
    29 
    30 
    31 Initial configuration
    32 =====================
    33 
    34 Never use any Mercurial version before 1.0!  At the moment, versions
    35 1.0, 1.0.1 and 1.0.2 all work equally well.
    36 
    37 
    38 The public pull area of the Isabelle repository can be cloned like
    39 this:
    40 
    41   hg clone http://isabelle.in.tum.de/repos/isabelle
    42 
    43 This will create a local directory "isabelle", unless an alternative
    44 name is specified.  The full repository meta-data and history of
    45 changes is in isabelle/.hg; local configuration for this clone can be
    46 added to isabelle/.hg/hgrc, but note that hgrc files are never copied
    47 by another clone operation!
    48 
    49 There is also ~/.hgrc for per-user Mercurial configuration.  The
    50 initial configuration should include at least an entry to identify
    51 yourself.  For example, something like this in /home/wenzelm/.hgrc:
    52 
    53   [ui]
    54   username = wenzelm
    55 
    56 Failing to configure the username correctly makes the system invent
    57 funny machine names that may persist eternally in the flow of
    58 changesets.
    59 
    60 In principle, user names can be chosen freely, but for longterm
    61 committers of the Isabelle repository the obvious choice is to keep
    62 with the old CVS naming scheme.
    63 
    64 
    65 There are other useful configuration to go into ~/.hgrc, e.g. defaults
    66 for common commands:
    67 
    68   [defaults]
    69   log = -l 10
    70 
    71 The next example shows how to install some Mercurial extension:
    72 
    73   [extensions]
    74   hgext.graphlog =
    75 
    76 Now the additional glog command will be available.
    77 
    78 
    79 See also the fine documentation for further details, especially the
    80 book http://hgbook.red-bean.com/
    81 
    82 
    83 Shared pull/push access
    84 =======================
    85 
    86 The entry point http://isabelle.in.tum.de/repos/isabelle is world
    87 readable, both via plain web browsing and the hg client as described
    88 above.  Anybody can produce a clone, change it arbitrarily, and then
    89 use regular mechanisms of Mercurial to report changes "upstream", say
    90 via e-mail to someone with write access to that file space.  It is
    91 also quite easy to publish changed clones again on the web, using hg
    92 serve, or the hgweb.cgi or hgwebdir.cgi scripts that are included in
    93 the Mercurial distribution.
    94 
    95 This downstream/upstream mode of operation is quite common in the
    96 distributed version control community, and works well for occasional
    97 changes produced by anybody out there.  Of course, upstream
    98 maintainers need to review and moderate changes being proposed, before
    99 pushing anything onto the official Isabelle repository at TUM.
   100 
   101 
   102 Direct pull/push access requires an account at TUM, with properly
   103 configured ssh access to the local machines (e.g. macbroy20,
   104 atbroy100).
   105 
   106 The simple wrapper script /home/isabelle/mercurial/bin/hg provides a
   107 uniform view on the different Linux installations on the local
   108 network.  Thus it is advisable to add that directory to the shell PATH
   109 of the account at TUM:
   110 
   111   PATH="/home/isabelle/mercurial/bin:$PATH"
   112 
   113 Now a clone of the shared push/pull area can be produced like this,
   114 using your user name instead of "wenzelm":
   115 
   116   hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   117 
   118 In fact, the only difference to the previous clone of
   119 http://isabelle.in.tum.de/repos/isabelle will be a different default
   120 pull/push path in isabelle/.hg/hgrc:
   121 
   122   [paths]
   123   default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   124 
   125 This means an earlier pull-only clone can be changed into a pull/push
   126 version by editing this single line of the internal repository
   127 configuration.
   128 
   129 
   130 Content discipline
   131 ==================
   132 
   133 Old-style centralized version control is occasionally compared with a
   134 "library where everybody scribbles into the books".  Or seen the other
   135 way round, the centralized model discourages individual
   136 experimentation (with local branches etc.), because everything is
   137 forced to happen on a shared file space.  With Mercurial, arbitrary
   138 variations on local clones are no problem, but care is required again
   139 when publishing changes eventually.
   140 
   141 The following principles should be kept in mind when producing
   142 changesets that might become public at some point.
   143 
   144   * The author of changes should be properly identified, using
   145     ui/username configuration as described above.
   146 
   147     While Mercurial also provides means for signed changesets, we want
   148     to keep things simple and trust that users specify their identity
   149     correctly.
   150 
   151   * The history of sources is an integral part of the sources
   152     themselves.  This means that private experiments and branches
   153     should not be published, unless they are really meant to become
   154     universally available.
   155 
   156     Note that exchanging local experiments with some other users can
   157     be done directly on peer-to-peer basis, without affecting the
   158     central pull/push area.
   159 
   160   * Log messages are an integral part of the history of sources.
   161     Other users will have to look there eventually, to understand why
   162     things have been done in a certain way at some point.
   163 
   164     Mercurial provides nice web presentation of incoming changes with
   165     a digest of log entries; this also includes Atom/RSS news feeds.
   166     Users should be aware that others will actually read what is
   167     written into log messages.
   168 
   169     The usual changelog presentation style for the Isabelle repository
   170     admits log entries that consist of several lines, but without the
   171     special head line that is used in Mercurial projects elsewhere.
   172     Since some display styles strip newlines from text, it is
   173     advisable to separate lines via punctuation, and not rely on
   174     two-dimensional presentation too much.
   175 
   176 
   177 Makarius 29-Nov-2008