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