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