README_REPOSITORY
author wenzelm
Mon Nov 23 22:47:08 2009 +0100 (2009-11-23)
changeset 33873 e9120a7b2779
parent 32361 141e5151b918
child 35567 309e75c58af2
permissions -rw-r--r--
more tuning for release;
wenzelm@28907
     1
Important notes on Mercurial repository access for Isabelle
wenzelm@28907
     2
===========================================================
wenzelm@28907
     3
wenzelm@28907
     4
Preamble
wenzelm@28907
     5
--------
wenzelm@28907
     6
wenzelm@28907
     7
Mercurial http://www.selenic.com/mercurial belongs to a new generation
wenzelm@28907
     8
of source code management systems, following the paradigm of
wenzelm@28907
     9
"distributed version control".  Compared to the old centralized model
wenzelm@28913
    10
of CVS or SVN, this gives considerable more power and freedom in
wenzelm@28907
    11
organizing the flow of changes, both between individual developers and
wenzelm@28907
    12
designated pull/push areas that are shared with others.
wenzelm@28907
    13
wenzelm@28907
    14
More power for the user also means more responsibility!  Due to its
wenzelm@28907
    15
decentralized nature, changesets that have been published once,
wenzelm@28913
    16
e.g. via "push" to a shared repository that is visible on the net,
wenzelm@28907
    17
cannot be easily retracted from the public again.  Regular Mercurial
wenzelm@28907
    18
operations are strictly monotonic, where changset transactions are
wenzelm@28913
    19
only added, but never deleted.  There are special tools to manipulate
wenzelm@28907
    20
individual repositories via non-monotonic actions, but this does not
wenzelm@28913
    21
yet retrieve any changesets that have escaped into the public by
wenzelm@28913
    22
accident.
wenzelm@28907
    23
wenzelm@28918
    24
Only global operations like "pull" and "push" fall into this critical
wenzelm@28918
    25
category.  Note that "incoming" / "outgoing" allow to inspect
wenzelm@28918
    26
changesets before exchanging them globally.  Anything else in
wenzelm@28918
    27
Mercurial is local to the user's repository clone (including "commit",
wenzelm@28918
    28
"update", "merge" etc.) and is in fact much simpler and safer to use
wenzelm@28918
    29
than the corresponding operations of CVS or SVN.
wenzelm@28907
    30
wenzelm@28907
    31
wenzelm@28907
    32
Initial configuration
wenzelm@29481
    33
---------------------
wenzelm@28907
    34
wenzelm@30182
    35
Always use Mercurial versions from the 1.0 or 1.1 branch, or later.
wenzelm@28913
    36
The old 0.9.x versions do not work in a multi-user environment with
wenzelm@30182
    37
shared file spaces!
wenzelm@28907
    38
wenzelm@28907
    39
wenzelm@28913
    40
The official Isabelle repository can be cloned like this:
wenzelm@28907
    41
wenzelm@28907
    42
  hg clone http://isabelle.in.tum.de/repos/isabelle
wenzelm@28907
    43
wenzelm@28907
    44
This will create a local directory "isabelle", unless an alternative
wenzelm@28907
    45
name is specified.  The full repository meta-data and history of
wenzelm@28907
    46
changes is in isabelle/.hg; local configuration for this clone can be
wenzelm@28907
    47
added to isabelle/.hg/hgrc, but note that hgrc files are never copied
wenzelm@28907
    48
by another clone operation!
wenzelm@28907
    49
wenzelm@28917
    50
wenzelm@28913
    51
There is also $HOME/.hgrc for per-user Mercurial configuration.  The
wenzelm@28907
    52
initial configuration should include at least an entry to identify
wenzelm@28907
    53
yourself.  For example, something like this in /home/wenzelm/.hgrc:
wenzelm@28907
    54
wenzelm@28907
    55
  [ui]
wenzelm@28907
    56
  username = wenzelm
wenzelm@28907
    57
wenzelm@28917
    58
Of course, the user identity can be also configured in
wenzelm@28918
    59
isabelle/.hg/hgrc on per-repository basis.  Failing to specify the
wenzelm@28917
    60
username correctly makes the system invent funny machine names that
wenzelm@28917
    61
may persist indefinitely in the public flow of changesets.
wenzelm@28907
    62
wenzelm@28907
    63
In principle, user names can be chosen freely, but for longterm
wenzelm@28907
    64
committers of the Isabelle repository the obvious choice is to keep
wenzelm@30182
    65
with the old CVS naming scheme.  Others should use their regular "full
wenzelm@30182
    66
name"; including an email address is optional.
wenzelm@28907
    67
wenzelm@28907
    68
wenzelm@28913
    69
There are other useful configuration to go into $HOME/.hgrc,
wenzelm@28913
    70
e.g. defaults for common commands:
wenzelm@28907
    71
wenzelm@28907
    72
  [defaults]
wenzelm@28907
    73
  log = -l 10
wenzelm@28907
    74
wenzelm@28907
    75
The next example shows how to install some Mercurial extension:
wenzelm@28907
    76
wenzelm@28907
    77
  [extensions]
wenzelm@28907
    78
  hgext.graphlog =
wenzelm@28907
    79
wenzelm@28907
    80
Now the additional glog command will be available.
wenzelm@28907
    81
wenzelm@28907
    82
wenzelm@28907
    83
See also the fine documentation for further details, especially the
wenzelm@28907
    84
book http://hgbook.red-bean.com/
wenzelm@28907
    85
wenzelm@28907
    86
wenzelm@28907
    87
Shared pull/push access
wenzelm@29481
    88
-----------------------
wenzelm@28907
    89
wenzelm@28907
    90
The entry point http://isabelle.in.tum.de/repos/isabelle is world
wenzelm@28907
    91
readable, both via plain web browsing and the hg client as described
wenzelm@28907
    92
above.  Anybody can produce a clone, change it arbitrarily, and then
wenzelm@28913
    93
use regular mechanisms of Mercurial to report changes upstream, say
wenzelm@28907
    94
via e-mail to someone with write access to that file space.  It is
wenzelm@28913
    95
also quite easy to publish changed clones again on the web, using the
wenzelm@28913
    96
adhoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
wenzelm@28913
    97
that are included in the Mercurial distribution.
wenzelm@28907
    98
wenzelm@28913
    99
The downstream/upstream mode of operation is quite common in the
wenzelm@28907
   100
distributed version control community, and works well for occasional
wenzelm@28907
   101
changes produced by anybody out there.  Of course, upstream
wenzelm@28907
   102
maintainers need to review and moderate changes being proposed, before
wenzelm@28907
   103
pushing anything onto the official Isabelle repository at TUM.
wenzelm@28907
   104
wenzelm@28907
   105
wenzelm@28913
   106
Write access to the Isabelle repository requires an account at TUM,
wenzelm@28913
   107
with properly configured ssh access to the local machines
wenzelm@28913
   108
(e.g. macbroy20, atbroy100).  You also need to be a member of the
wenzelm@28913
   109
"isabelle" Unix group.
wenzelm@28907
   110
wenzelm@28913
   111
Sharing a locally modified clone then works as follows, using your
wenzelm@28913
   112
user name instead of "wenzelm":
wenzelm@28913
   113
wenzelm@28913
   114
  hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
wenzelm@28907
   115
wenzelm@28913
   116
In fact, the "out" or "outgoing" command performs only a dry run: it
wenzelm@28913
   117
displays the changesets that would get published.  An actual "push",
wenzelm@28913
   118
with a lasting effect on the Isabelle repository, works like this:
wenzelm@28907
   119
wenzelm@28913
   120
  hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
wenzelm@28913
   121
wenzelm@28907
   122
wenzelm@28913
   123
Default paths for push and pull can be configure in isabelle/.hg/hgrc,
wenzelm@28913
   124
for example:
wenzelm@28907
   125
wenzelm@28907
   126
  [paths]
wenzelm@28907
   127
  default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
wenzelm@28907
   128
wenzelm@28913
   129
Now "hg pull" or "hg push" will use that shared file space, unless a
wenzelm@28913
   130
different URL is specified explicitly.
wenzelm@28913
   131
wenzelm@28913
   132
When cloning a repository, the default path is set to the initial
wenzelm@28913
   133
source URL.  So we could have cloned via that ssh URL in the first
wenzelm@28913
   134
place, to get exactly to the same point:
wenzelm@28913
   135
wenzelm@28913
   136
  hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
wenzelm@28907
   137
wenzelm@28907
   138
wenzelm@30182
   139
Simplified merges
wenzelm@30182
   140
-----------------
wenzelm@30182
   141
wenzelm@30182
   142
The main idea of Mercurial is to let individual users produce
wenzelm@30182
   143
independent branches of development first, but merge with others
wenzelm@30182
   144
frequently.  The basic hg merge operation is more general than
wenzelm@30182
   145
required for the mode of operation with a shared pull/push area.  The
wenzelm@30182
   146
hg fetch extension accommodates this case nicely, automating trivial
wenzelm@30182
   147
merges and requiring manual intervention for actual conflicts only.
wenzelm@30182
   148
wenzelm@30182
   149
The fetch extension can be configured via the user's ~/.hgrc like
wenzelm@30182
   150
this:
wenzelm@30182
   151
wenzelm@30182
   152
  [extensions]
wenzelm@30182
   153
  hgext.fetch =
wenzelm@30182
   154
wenzelm@30182
   155
  [defaults]
wenzelm@30182
   156
  fetch = -m "merged"
wenzelm@30182
   157
wenzelm@30182
   158
Note that the potential for merge conflicts can be greatly reduced by
wenzelm@30182
   159
doing "hg fetch" before any starting local changes!
wenzelm@30182
   160
wenzelm@30182
   161
wenzelm@28907
   162
Content discipline
wenzelm@29481
   163
------------------
wenzelm@28907
   164
wenzelm@28913
   165
Old-style centralized version control is occasionally compared to "a
wenzelm@28913
   166
library where everybody scribbles into the books".  Or seen the other
wenzelm@28907
   167
way round, the centralized model discourages individual
wenzelm@28907
   168
experimentation (with local branches etc.), because everything is
wenzelm@28907
   169
forced to happen on a shared file space.  With Mercurial, arbitrary
wenzelm@28907
   170
variations on local clones are no problem, but care is required again
wenzelm@28907
   171
when publishing changes eventually.
wenzelm@28907
   172
wenzelm@28907
   173
The following principles should be kept in mind when producing
wenzelm@28907
   174
changesets that might become public at some point.
wenzelm@28907
   175
wenzelm@28907
   176
  * The author of changes should be properly identified, using
wenzelm@28907
   177
    ui/username configuration as described above.
wenzelm@28907
   178
wenzelm@28907
   179
    While Mercurial also provides means for signed changesets, we want
wenzelm@28907
   180
    to keep things simple and trust that users specify their identity
wenzelm@28907
   181
    correctly.
wenzelm@28907
   182
wenzelm@28907
   183
  * The history of sources is an integral part of the sources
wenzelm@28907
   184
    themselves.  This means that private experiments and branches
wenzelm@28907
   185
    should not be published, unless they are really meant to become
wenzelm@28907
   186
    universally available.
wenzelm@28907
   187
wenzelm@28907
   188
    Note that exchanging local experiments with some other users can
wenzelm@28907
   189
    be done directly on peer-to-peer basis, without affecting the
wenzelm@28907
   190
    central pull/push area.
wenzelm@28907
   191
wenzelm@28907
   192
  * Log messages are an integral part of the history of sources.
wenzelm@28907
   193
    Other users will have to look there eventually, to understand why
wenzelm@28907
   194
    things have been done in a certain way at some point.
wenzelm@28907
   195
wenzelm@28907
   196
    Mercurial provides nice web presentation of incoming changes with
wenzelm@28908
   197
    a digest of log entries; this also includes RSS/Atom news feeds.
wenzelm@28907
   198
    Users should be aware that others will actually read what is
wenzelm@30182
   199
    written into log messages.  There are also add-on browsers,
wenzelm@30182
   200
    notably hgtk that is part of the TortoiseHg distribution and works
wenzelm@30182
   201
    for generic Python/GTk platforms.
wenzelm@28907
   202
wenzelm@28907
   203
    The usual changelog presentation style for the Isabelle repository
wenzelm@28907
   204
    admits log entries that consist of several lines, but without the
wenzelm@28913
   205
    special headline that is used in Mercurial projects elsewhere.
wenzelm@28907
   206
    Since some display styles strip newlines from text, it is
wenzelm@28907
   207
    advisable to separate lines via punctuation, and not rely on
wenzelm@28907
   208
    two-dimensional presentation too much.
wenzelm@28907
   209
wenzelm@28907
   210
wenzelm@32361
   211
Building a repository version of Isabelle
wenzelm@32361
   212
-----------------------------------------
wenzelm@28908
   213
wenzelm@28910
   214
Compared to a proper distribution or development snapshot, a
wenzelm@28913
   215
repository version of Isabelle lacks textual version identifiers in
wenzelm@28913
   216
some sources and scripts, and various components produced by
wenzelm@28913
   217
Admin/build are missing.  After applying that script with suitable
wenzelm@28913
   218
arguments, the regular user instructions for building and running
wenzelm@28913
   219
Isabelle from sources apply.
wenzelm@28908
   220
wenzelm@28913
   221
Needless to say, the results from the build process must not be added
wenzelm@28913
   222
to the repository!