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