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