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