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