README_REPOSITORY
author wenzelm
Sun Nov 30 12:25:54 2008 +0100 (2008-11-30)
changeset 28913 86ed1c86e0ef
parent 28910 5c712e46988f
child 28917 20f43e0e0958
permissions -rw-r--r--
misc tuning and clarification;
     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 or 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 manipulate
    20 individual repositories via non-monotonic actions, but this does not
    21 yet retrieve any changesets that have escaped into the public by
    22 accident.
    23 
    24 Only global operations like "pull" / "push", "unbundle" / "bundle"
    25 etc. fall into this critical category.  Note that "incoming" /
    26 "outgoing" allow to inspect changesets before exchanging them
    27 globally.  Anything else in Mercurial is local to the user's
    28 repository clone (including "commit", "update", "merge" etc.) and is
    29 in fact much simpler and safer to use than the corresponding
    30 operations of CVS or SVN.
    31 
    32 
    33 Initial configuration
    34 =====================
    35 
    36 Always use Mercurial version 1.0 or later, such as 1.0.1 or 1.0.2.
    37 The old 0.9.x versions do not work in a multi-user environment with
    38 shared file spaces.
    39 
    40 
    41 The official Isabelle repository can be cloned like this:
    42 
    43   hg clone http://isabelle.in.tum.de/repos/isabelle
    44 
    45 This will create a local directory "isabelle", unless an alternative
    46 name is specified.  The full repository meta-data and history of
    47 changes is in isabelle/.hg; local configuration for this clone can be
    48 added to isabelle/.hg/hgrc, but note that hgrc files are never copied
    49 by another clone operation!
    50 
    51 There is also $HOME/.hgrc for per-user Mercurial configuration.  The
    52 initial configuration should include at least an entry to identify
    53 yourself.  For example, something like this in /home/wenzelm/.hgrc:
    54 
    55   [ui]
    56   username = wenzelm
    57 
    58 Failing to configure the username correctly makes the system invent
    59 funny machine names that may persist indefinitely in the public flow
    60 of changesets.
    61 
    62 In principle, user names can be chosen freely, but for longterm
    63 committers of the Isabelle repository the obvious choice is to keep
    64 with the old CVS naming scheme.
    65 
    66 
    67 There are other useful configuration to go into $HOME/.hgrc,
    68 e.g. defaults for common commands:
    69 
    70   [defaults]
    71   log = -l 10
    72 
    73 The next example shows how to install some Mercurial extension:
    74 
    75   [extensions]
    76   hgext.graphlog =
    77 
    78 Now the additional glog command will be available.
    79 
    80 
    81 See also the fine documentation for further details, especially the
    82 book http://hgbook.red-bean.com/
    83 
    84 
    85 Shared pull/push access
    86 =======================
    87 
    88 The entry point http://isabelle.in.tum.de/repos/isabelle is world
    89 readable, both via plain web browsing and the hg client as described
    90 above.  Anybody can produce a clone, change it arbitrarily, and then
    91 use regular mechanisms of Mercurial to report changes upstream, say
    92 via e-mail to someone with write access to that file space.  It is
    93 also quite easy to publish changed clones again on the web, using the
    94 adhoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
    95 that are included in the Mercurial distribution.
    96 
    97 The downstream/upstream mode of operation is quite common in the
    98 distributed version control community, and works well for occasional
    99 changes produced by anybody out there.  Of course, upstream
   100 maintainers need to review and moderate changes being proposed, before
   101 pushing anything onto the official Isabelle repository at TUM.
   102 
   103 
   104 Write access to the Isabelle repository requires an account at TUM,
   105 with properly configured ssh access to the local machines
   106 (e.g. macbroy20, atbroy100).  You also need to be a member of the
   107 "isabelle" Unix group.
   108 
   109 Sharing a locally modified clone then works as follows, using your
   110 user name instead of "wenzelm":
   111 
   112   hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   113 
   114 In fact, the "out" or "outgoing" command performs only a dry run: it
   115 displays the changesets that would get published.  An actual "push",
   116 with a lasting effect on the Isabelle repository, works like this:
   117 
   118   hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   119 
   120 
   121 Default paths for push and pull can be configure in isabelle/.hg/hgrc,
   122 for example:
   123 
   124   [paths]
   125   default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   126 
   127 Now "hg pull" or "hg push" will use that shared file space, unless a
   128 different URL is specified explicitly.
   129 
   130 When cloning a repository, the default path is set to the initial
   131 source URL.  So we could have cloned via that ssh URL in the first
   132 place, to get exactly to the same point:
   133 
   134   hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   135 
   136 
   137 Content discipline
   138 ==================
   139 
   140 Old-style centralized version control is occasionally compared to "a
   141 library where everybody scribbles into the books".  Or seen the other
   142 way round, the centralized model discourages individual
   143 experimentation (with local branches etc.), because everything is
   144 forced to happen on a shared file space.  With Mercurial, arbitrary
   145 variations on local clones are no problem, but care is required again
   146 when publishing changes eventually.
   147 
   148 The following principles should be kept in mind when producing
   149 changesets that might become public at some point.
   150 
   151   * The author of changes should be properly identified, using
   152     ui/username configuration as described above.
   153 
   154     While Mercurial also provides means for signed changesets, we want
   155     to keep things simple and trust that users specify their identity
   156     correctly.
   157 
   158   * The history of sources is an integral part of the sources
   159     themselves.  This means that private experiments and branches
   160     should not be published, unless they are really meant to become
   161     universally available.
   162 
   163     Note that exchanging local experiments with some other users can
   164     be done directly on peer-to-peer basis, without affecting the
   165     central pull/push area.
   166 
   167   * Log messages are an integral part of the history of sources.
   168     Other users will have to look there eventually, to understand why
   169     things have been done in a certain way at some point.
   170 
   171     Mercurial provides nice web presentation of incoming changes with
   172     a digest of log entries; this also includes RSS/Atom news feeds.
   173     Users should be aware that others will actually read what is
   174     written into log messages.
   175 
   176     The usual changelog presentation style for the Isabelle repository
   177     admits log entries that consist of several lines, but without the
   178     special headline that is used in Mercurial projects elsewhere.
   179     Since some display styles strip newlines from text, it is
   180     advisable to separate lines via punctuation, and not rely on
   181     two-dimensional presentation too much.
   182 
   183 
   184 Building Isabelle from the repository version
   185 =============================================
   186 
   187 Compared to a proper distribution or development snapshot, a
   188 repository version of Isabelle lacks textual version identifiers in
   189 some sources and scripts, and various components produced by
   190 Admin/build are missing.  After applying that script with suitable
   191 arguments, the regular user instructions for building and running
   192 Isabelle from sources apply.
   193 
   194 Needless to say, the results from the build process must not be added
   195 to the repository!
   196 
   197 
   198 Makarius 30-Nov-2008