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