README_REPOSITORY
author wenzelm
Sun Sep 18 15:59:38 2011 +0200 (2011-09-18)
changeset 44975 f80d918f8ac0
parent 40601 021278fdd0a8
child 47449 5e1482296b12
permissions -rw-r--r--
tentative announcement based on current NEWS;
     1 Important notes on Mercurial repository access for Isabelle
     2 ===========================================================
     3 
     4 Introduction
     5 ------------
     6 
     7 Mercurial http://www.selenic.com/mercurial belongs to the current
     8 generation of source code management systems that follow the so-called
     9 paradigm of "distributed version control".  This is a terrific name
    10 for plain revision control without the legacy of CVS or SVN.  See also
    11 http://hginit.com/ for an introduction to the main ideas.  The
    12 Mercurial book http://hgbook.red-bean.com/ explains many more details.
    13 
    14 Mercurial offers great flexibility in organizing the flow of changes,
    15 both between individual developers and designated pull/push areas that
    16 are shared with others.  This additional power demands some additional
    17 responsibility to maintain a certain development process that fits to
    18 a particular project.
    19 
    20 Regular Mercurial operations are strictly monotonic, where changeset
    21 transactions are only added, but never deleted.  There are special
    22 tools to manipulate repositories via non-monotonic actions (such as
    23 "rollback" or "strip"), but recovering from gross mistakes that have
    24 escaped into the public can be hard and embarrassing.  It is much
    25 easier to inspect and amend changesets routinely before pushing.
    26 
    27 The effect of the critical "pull" / "push" operations can be tested in
    28 a dry run via "incoming" / "outgoing".  The "fetch" extension includes
    29 useful sanity checks beyond raw "pull" / "update" / "merge".  Most
    30 other operations are local to the user's repository clone.  This gives
    31 some freedom for experimentation without affecting anybody else.
    32 
    33 Mercurial provides nice web presentation of incoming changes with a
    34 digest of log entries; this also includes RSS/Atom news feeds.  There
    35 are add-on browsers, notably hgtk that is part of the TortoiseHg
    36 distribution and works for generic Python/GTk platforms.  The
    37 alternative "view" utility helps to inspect the semantic content of
    38 merge nodes.
    39 
    40 
    41 Initial configuration
    42 ---------------------
    43 
    44 The official Isabelle repository can be cloned like this:
    45 
    46   hg clone http://isabelle.in.tum.de/repos/isabelle
    47 
    48 This will create a local directory "isabelle", unless an alternative
    49 name is specified.  The full repository meta-data and history of
    50 changes is in isabelle/.hg; local configuration for this clone can be
    51 added to isabelle/.hg/hgrc, but note that hgrc files are never copied
    52 by another clone operation.
    53 
    54 
    55 There is also $HOME/.hgrc for per-user Mercurial configuration.  The
    56 initial configuration requires at least an entry to identify yourself
    57 as follows:
    58 
    59   [ui]
    60   username = XXX
    61 
    62 Isabelle contributors are free to choose either a short "login name"
    63 (for accounts at TU Munich) or a "full name" -- with or without mail
    64 address.  It is important to stick to this choice once and for all.
    65 The machine default that Mercurial produces for unspecified
    66 [ui]username is not appropriate.
    67 
    68 Such configuration can be given in $HOME/.hgrc (for each home
    69 directory on each machine) or in .hg/hgrc (for each repository clone).
    70 
    71 
    72 Here are some further examples for hgrc.  This is how to provide
    73 default options for common commands:
    74 
    75   [defaults]
    76   log = -l 10
    77 
    78 This is how to configure some extension, which is called "graphlog"
    79 and provides the "glog" command:
    80 
    81   [extensions]
    82   hgext.graphlog =
    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 locally, and then use
    91 regular mechanisms of Mercurial to report changes upstream, say via
    92 mail to someone with write access to that file space.  It is also
    93 quite easy to publish changed clones again on the web, using the
    94 ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
    95 that are included in the Mercurial distribution, and send a "pull
    96 request" to someone else.  There are also public hosting services for
    97 Mercurial repositories.
    98 
    99 The downstream/upstream mode of operation is quite common in the
   100 distributed version control community, and works well for occasional
   101 changes produced by anybody out there.  Of course, upstream
   102 maintainers need to review and moderate changes being proposed, before
   103 pushing anything onto the official Isabelle repository at TUM.  Direct
   104 pushes are also reviewed routinely in a post-hoc fashion; everybody
   105 hooked on the main repository is called to keep an eye on incoming
   106 changes.  In any case, changesets need to be understandable, at the
   107 time of writing and many years later.
   108 
   109 Push access to the Isabelle repository requires an account at TUM,
   110 with properly configured ssh to the local machines (e.g. macbroy20,
   111 atbroy100).  You also need to be a member of the "isabelle" Unix
   112 group.
   113 
   114 Sharing a locally modified clone then works as follows, using your
   115 user name instead of "wenzelm":
   116 
   117   hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   118 
   119 In fact, the "out" or "outgoing" command performs only a dry run: it
   120 displays the changesets that would get published.  An actual "push",
   121 with a lasting effect on the Isabelle repository, works like this:
   122 
   123   hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   124 
   125 
   126 Default paths for push and pull can be configured in
   127 isabelle/.hg/hgrc, for example:
   128 
   129   [paths]
   130   default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   131 
   132 Now "hg pull" or "hg push" will use that shared file space, unless a
   133 different URL is specified explicitly.
   134 
   135 When cloning a repository, the default path is set to the initial
   136 source URL.  So we could have cloned via that ssh URL in the first
   137 place, to get exactly to the same point:
   138 
   139   hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   140 
   141 
   142 Simple merges
   143 -------------
   144 
   145 The main idea of Mercurial is to let individual users produce
   146 independent branches of development first, but merge with others
   147 frequently.  The basic hg merge operation is more general than
   148 required for the mode of operation with a shared pull/push area.  The
   149 "fetch" extension accommodates this case nicely, automating trivial
   150 merges and requiring manual intervention for actual conflicts only.
   151 
   152 The fetch extension can be configured via $HOME/.hgrc like this:
   153 
   154   [extensions]
   155   hgext.fetch =
   156 
   157   [defaults]
   158   fetch = -m "merged"
   159 
   160 To keep merges semantically trivial and prevent genuine merge
   161 conflicts or lost updates, it is essential to observe to following
   162 general discipline wrt. the public Isabelle push area:
   163 
   164   * Before editing, pull or fetch the latest version.
   165 
   166   * Accumulate private commits for a maximum of 1-3 days.
   167 
   168   * Start publishing again by pull or fetch, which normally produces
   169     local merges.
   170 
   171   * Test the merged result as usual and push back in real time.
   172 
   173 Piling private changes and public merges longer than 0.5-2 hours is
   174 apt to produce some mess when pushing eventually!
   175 
   176 
   177 Content discipline
   178 ------------------
   179 
   180 The following principles should be kept in mind when producing
   181 changesets that are meant to be published at some point.
   182 
   183   * The author of changes needs to be properly identified, using
   184     [ui]username configuration as described above.
   185 
   186     While Mercurial also provides means for signed changesets, we want
   187     to keep things simple and trust that users specify their identity
   188     correctly (and uniquely).
   189 
   190   * The history of sources is an integral part of the sources
   191     themselves.  This means that private experiments and branches
   192     should not be published by accident.  Named branches are not
   193     allowed on the public version.  Note that old SVN-style branching
   194     is replaced by regular repository clones in Mercurial.
   195 
   196     Exchanging local experiments with some other users can be done
   197     directly on peer-to-peer basis, without affecting the central
   198     pull/push area.
   199 
   200   * Log messages are an integral part of the history of sources.
   201     Other people will have to inspect them routinely, to understand
   202     why things have been done in a certain way at some point.
   203 
   204     Authors of log entries should be aware that published changes are
   205     actually read.  The main point is not to announce novelties, but
   206     to describe faithfully what has been done, and provide some clues
   207     about the motivation behind it.  The main recipient is someone who
   208     needs to understand the change in the distant future to isolate
   209     problems.  Sometimes it is helpful to reference past changes via
   210     changeset ids in the log entry.
   211 
   212   * The standard changelog entry format of the Isabelle repository
   213     admits several (vaguely related) items to be rolled into one
   214     changeset.  Each item is then described on a separate line that
   215     may become longer as screen line and is terminated by punctuation.
   216     These lines are roughly ordered by importance.
   217 
   218     This format conforms to established Isabelle tradition.  In
   219     contrast, the default of Mercurial prefers a single headline
   220     followed by a long body text.  The reason for that is a somewhat
   221     different development model of typical "distributed" projects,
   222     where external changes pass through a hierarchy of reviewers and
   223     maintainers, until they end up in some authoritative repository.
   224     Isabelle changesets can be more spontaneous, growing from the
   225     bottom-up.
   226 
   227     The web style of http://isabelle.in.tum.de/repos/isabelle/
   228     accommodates the Isabelle changelog format.  Note that multiple
   229     lines will sometimes display as a single paragraph in HTML, so
   230     some terminating punctuation is required.  Do not squeeze multiple
   231     items on the same line in the original text!
   232 
   233 
   234 Building a repository version of Isabelle
   235 -----------------------------------------
   236 
   237 Compared to a proper distribution or development snapshot, it is
   238 relatively hard to build from the raw repository version.  Essential
   239 contributing components are missing and need to be reconstructed by
   240 running the Admin/build script by hand.  Afterwards the main Isabelle
   241 system and logic images can be compiled via the toplevel ./build
   242 script.  Note that the repository lacks some textual version
   243 identifiers in the sources and scripts; this implies some changed
   244 behavior when processing settings etc.
   245 
   246 There is no guarantee that the NEWS file is up to date at an arbitrary
   247 point in history.