author wenzelm
Fri Aug 17 21:15:36 2012 +0200 (2012-08-17)
changeset 48854 f7cbf24b5f41
parent 48853 ec82c33c75f8
child 48855 a7d0b9e349ec
permissions -rw-r--r--
Backed out changeset ec82c33c75f8;
     1 Important notes on Mercurial repository access for Isabelle
     2 ===========================================================
     4 Introduction
     5 ------------
     7 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 for an introduction to the main ideas.  The
    12 Mercurial book explains many more details.
    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.
    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.
    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.
    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 history browsers such as "hg view" and TortoiseHg.  Unlike
    36 the default web view, some of these tools help to inspect the semantic
    37 content of non-trivial merge nodes.
    40 Initial configuration
    41 ---------------------
    43 The official Isabelle repository can be cloned like this:
    45   hg clone
    47 This will create a local directory "isabelle", unless an alternative
    48 name is specified.  The full repository meta-data and history of
    49 changes is in isabelle/.hg; local configuration for this clone can be
    50 added to isabelle/.hg/hgrc, but note that hgrc files are never copied
    51 by another clone operation.
    54 There is also $HOME/.hgrc for per-user Mercurial configuration.  The
    55 initial configuration requires at least an entry to identify yourself
    56 as follows:
    58   [ui]
    59   username = XXX
    61 Isabelle contributors are free to choose either a short "login name"
    62 (for accounts at TU Munich) or a "full name" -- with or without mail
    63 address.  It is important to stick to this choice once and for all.
    64 The machine default that Mercurial produces for unspecified
    65 [ui]username is not appropriate.
    67 Such configuration can be given in $HOME/.hgrc (for each home
    68 directory on each machine) or in .hg/hgrc (for each repository clone).
    71 Here are some further examples for hgrc.  This is how to provide
    72 default options for common commands:
    74   [defaults]
    75   log = -l 10
    77 This is how to configure some extension, which is called "graphlog"
    78 and provides the "glog" command:
    80   [extensions]
    81   hgext.graphlog =
    84 Shared pull/push access
    85 -----------------------
    87 The entry point is world
    88 readable, both via plain web browsing and the hg client as described
    89 above.  Anybody can produce a clone, change it locally, and then use
    90 regular mechanisms of Mercurial to report changes upstream, say via
    91 mail to someone with write access to that file space.  It is also
    92 quite easy to publish changed clones again on the web, using the
    93 ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
    94 that are included in the Mercurial distribution, and send a "pull
    95 request" to someone else.  There are also public hosting services for
    96 Mercurial repositories.
    98 The downstream/upstream mode of operation is quite common in the
    99 distributed version control community, and works well for occasional
   100 changes produced by anybody out there.  Of course, upstream
   101 maintainers need to review and moderate changes being proposed, before
   102 pushing anything onto the official Isabelle repository at TUM.  Direct
   103 pushes are also reviewed routinely in a post-hoc fashion; everybody
   104 hooked on the main repository is called to keep an eye on incoming
   105 changes.  In any case, changesets need to be understandable, at the
   106 time of writing and many years later.
   108 Push access to the Isabelle repository requires an account at TUM,
   109 with properly configured ssh to the local machines (e.g. macbroy20 ..
   110 macbroy29).  You also need to be a member of the "isabelle" Unix
   111 group.
   113 Sharing a locally modified clone then works as follows, using your
   114 user name instead of "wenzelm":
   116   hg out ssh://wenzelm@macbroy20//home/isabelle-repository/repos/isabelle
   118 In fact, the "out" or "outgoing" command performs only a dry run: it
   119 displays the changesets that would get published.  An actual "push",
   120 with a lasting effect on the Isabelle repository, works like this:
   122   hg push ssh://wenzelm@macbroy20//home/isabelle-repository/repos/isabelle
   125 Default paths for push and pull can be configured in
   126 isabelle/.hg/hgrc, for example:
   128   [paths]
   129   default = ssh://wenzelm@macbroy20//home/isabelle-repository/repos/isabelle
   131 Now "hg pull" or "hg push" will use that shared file space, unless a
   132 different URL is specified explicitly.
   134 When cloning a repository, the default path is set to the initial
   135 source URL.  So we could have cloned via that ssh URL in the first
   136 place, to get exactly to the same point:
   138   hg clone ssh://wenzelm@macbroy20//home/isabelle-repository/repos/isabelle
   141 Simple merges
   142 -------------
   144 The main idea of Mercurial is to let individual users produce
   145 independent branches of development first, but merge with others
   146 frequently.  The basic hg merge operation is more general than
   147 required for the mode of operation with a shared pull/push area.  The
   148 "fetch" extension accommodates this case nicely, automating trivial
   149 merges and requiring manual intervention for actual conflicts only.
   151 The fetch extension can be configured via $HOME/.hgrc like this:
   153   [extensions]
   154   hgext.fetch =
   156   [defaults]
   157   fetch = -m "merged"
   159 To keep merges semantically trivial and prevent genuine merge
   160 conflicts or lost updates, it is essential to observe to following
   161 general discipline wrt. the public Isabelle push area:
   163   * Before editing, pull or fetch the latest version.
   165   * Accumulate private commits for a maximum of 1-3 days.
   167   * Start publishing again by pull or fetch, which normally produces
   168     local merges.
   170   * Test the merged result as usual and push back in real time.
   172 Piling private changes and public merges longer than 0.5-2 hours is
   173 apt to produce some mess when pushing eventually!
   176 Content discipline
   177 ------------------
   179 The following principles should be kept in mind when producing
   180 changesets that are meant to be published at some point.
   182   * The author of changes needs to be properly identified, using
   183     [ui]username configuration as described above.
   185     While Mercurial also provides means for signed changesets, we want
   186     to keep things simple and trust that users specify their identity
   187     correctly (and uniquely).
   189   * The history of sources is an integral part of the sources
   190     themselves.  This means that private experiments and branches
   191     should not be published by accident.  Named branches are not
   192     allowed on the public version.  Note that old SVN-style branching
   193     is replaced by regular repository clones in Mercurial.
   195     Exchanging local experiments with some other users can be done
   196     directly on peer-to-peer basis, without affecting the central
   197     pull/push area.
   199   * Log messages are an integral part of the history of sources.
   200     Other people will have to inspect them routinely, to understand
   201     why things have been done in a certain way at some point.
   203     Authors of log entries should be aware that published changes are
   204     actually read.  The main point is not to announce novelties, but
   205     to describe faithfully what has been done, and provide some clues
   206     about the motivation behind it.  The main recipient is someone who
   207     needs to understand the change in the distant future to isolate
   208     problems.  Sometimes it is helpful to reference past changes via
   209     changeset ids in the log entry.
   211   * The standard changelog entry format of the Isabelle repository
   212     admits several (vaguely related) items to be rolled into one
   213     changeset.  Each item is then described on a separate line that
   214     may become longer as screen line and is terminated by punctuation.
   215     These lines are roughly ordered by importance.
   217     This format conforms to established Isabelle tradition.  In
   218     contrast, the default of Mercurial prefers a single headline
   219     followed by a long body text.  The reason for that is a somewhat
   220     different development model of typical "distributed" projects,
   221     where external changes pass through a hierarchy of reviewers and
   222     maintainers, until they end up in some authoritative repository.
   223     Isabelle changesets can be more spontaneous, growing from the
   224     bottom-up.
   226     The web style of
   227     accommodates the Isabelle changelog format.  Note that multiple
   228     lines will sometimes display as a single paragraph in HTML, so
   229     some terminating punctuation is required.  Do not squeeze multiple
   230     items on the same line in the original text!
   233 Building a repository version of Isabelle
   234 -----------------------------------------
   236 The regular "isabelle build" tool allows to build session images as
   237 usual, but this first requires to resolve add-on components first,
   238 including the ML system.  Some extra configuration is required to
   239 approximate some of the system integration of official Isabelle
   240 releases from a bare-bones repository snapshot.  The special directory
   241 Admin/ -- which is absent in official releases -- might provide some
   242 further clues.
   244 Here is a reasonably easy way to include important Isabelle components
   245 on the spot:
   247   (1) The bash script ISABELLE_HOME_USER/etc/settings is augmented by
   248   some shell function invocations like this:
   250       init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
   251       init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional"
   253   This uses some central place "$HOME/.isabelle/contrib" to keep
   254   component directories that are shared by all Isabelle versions.
   256   (2) Missing components are resolved on the command line like this:
   258       isabelle components -a
   260   This will saturate the "$HOME/.isabelle/contrib" directory structure
   261   from according to $ISABELLE_COMPONENT_REPOSITORY.
   263 Since the given component catalogs in $ISABELLE_HOME/Admin/components
   264 are subject to the Mercurial history, it is possible to bisect over a
   265 range of Isabelle versions while references to the contributing
   266 components change accordingly.