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