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