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