README_REPOSITORY
author wenzelm
Sat Nov 29 19:01:28 2008 +0100 (2008-11-29)
changeset 28910 5c712e46988f
parent 28908 4571302e1594
child 28913 86ed1c86e0ef
permissions -rw-r--r--
tuned;
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@28907
    10
of CVS/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@28907
    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@28907
    19
only added, but never deleted.  There are special tools to "repair"
wenzelm@28907
    20
individual repositories via non-monotonic actions, but this does not
wenzelm@28907
    21
yet retrieve unwanted changesets that have escaped into the public.
wenzelm@28907
    22
wenzelm@28907
    23
Only global operations like pull/push, unbundle/bundle etc. fall into
wenzelm@28907
    24
this critical category; incoming/outgoing or in/out may help to
wenzelm@28907
    25
inspect changesets before exchanging them globally.  Anything else in
wenzelm@28907
    26
Mercurial is local to the user's repository clone (including
wenzelm@28907
    27
commit/update/merge etc.) and is in fact much simpler and safer to use
wenzelm@28907
    28
than the corresponding operations of CVS or SVN.
wenzelm@28907
    29
wenzelm@28907
    30
wenzelm@28907
    31
Initial configuration
wenzelm@28907
    32
=====================
wenzelm@28907
    33
wenzelm@28907
    34
Never use any Mercurial version before 1.0!  At the moment, versions
wenzelm@28907
    35
1.0, 1.0.1 and 1.0.2 all work equally well.
wenzelm@28907
    36
wenzelm@28907
    37
wenzelm@28907
    38
The public pull area of the Isabelle repository can be cloned like
wenzelm@28907
    39
this:
wenzelm@28907
    40
wenzelm@28907
    41
  hg clone http://isabelle.in.tum.de/repos/isabelle
wenzelm@28907
    42
wenzelm@28907
    43
This will create a local directory "isabelle", unless an alternative
wenzelm@28907
    44
name is specified.  The full repository meta-data and history of
wenzelm@28907
    45
changes is in isabelle/.hg; local configuration for this clone can be
wenzelm@28907
    46
added to isabelle/.hg/hgrc, but note that hgrc files are never copied
wenzelm@28907
    47
by another clone operation!
wenzelm@28907
    48
wenzelm@28907
    49
There is also ~/.hgrc for per-user Mercurial configuration.  The
wenzelm@28907
    50
initial configuration should include at least an entry to identify
wenzelm@28907
    51
yourself.  For example, something like this in /home/wenzelm/.hgrc:
wenzelm@28907
    52
wenzelm@28907
    53
  [ui]
wenzelm@28907
    54
  username = wenzelm
wenzelm@28907
    55
wenzelm@28907
    56
Failing to configure the username correctly makes the system invent
wenzelm@28907
    57
funny machine names that may persist eternally in the flow of
wenzelm@28907
    58
changesets.
wenzelm@28907
    59
wenzelm@28907
    60
In principle, user names can be chosen freely, but for longterm
wenzelm@28907
    61
committers of the Isabelle repository the obvious choice is to keep
wenzelm@28907
    62
with the old CVS naming scheme.
wenzelm@28907
    63
wenzelm@28907
    64
wenzelm@28907
    65
There are other useful configuration to go into ~/.hgrc, e.g. defaults
wenzelm@28907
    66
for common commands:
wenzelm@28907
    67
wenzelm@28907
    68
  [defaults]
wenzelm@28907
    69
  log = -l 10
wenzelm@28907
    70
wenzelm@28907
    71
The next example shows how to install some Mercurial extension:
wenzelm@28907
    72
wenzelm@28907
    73
  [extensions]
wenzelm@28907
    74
  hgext.graphlog =
wenzelm@28907
    75
wenzelm@28907
    76
Now the additional glog command will be available.
wenzelm@28907
    77
wenzelm@28907
    78
wenzelm@28907
    79
See also the fine documentation for further details, especially the
wenzelm@28907
    80
book http://hgbook.red-bean.com/
wenzelm@28907
    81
wenzelm@28907
    82
wenzelm@28907
    83
Shared pull/push access
wenzelm@28907
    84
=======================
wenzelm@28907
    85
wenzelm@28907
    86
The entry point http://isabelle.in.tum.de/repos/isabelle is world
wenzelm@28907
    87
readable, both via plain web browsing and the hg client as described
wenzelm@28907
    88
above.  Anybody can produce a clone, change it arbitrarily, and then
wenzelm@28907
    89
use regular mechanisms of Mercurial to report changes "upstream", say
wenzelm@28907
    90
via e-mail to someone with write access to that file space.  It is
wenzelm@28907
    91
also quite easy to publish changed clones again on the web, using hg
wenzelm@28907
    92
serve, or the hgweb.cgi or hgwebdir.cgi scripts that are included in
wenzelm@28907
    93
the Mercurial distribution.
wenzelm@28907
    94
wenzelm@28907
    95
This downstream/upstream mode of operation is quite common in the
wenzelm@28907
    96
distributed version control community, and works well for occasional
wenzelm@28907
    97
changes produced by anybody out there.  Of course, upstream
wenzelm@28907
    98
maintainers need to review and moderate changes being proposed, before
wenzelm@28907
    99
pushing anything onto the official Isabelle repository at TUM.
wenzelm@28907
   100
wenzelm@28907
   101
wenzelm@28907
   102
Direct pull/push access requires an account at TUM, with properly
wenzelm@28907
   103
configured ssh access to the local machines (e.g. macbroy20,
wenzelm@28907
   104
atbroy100).
wenzelm@28907
   105
wenzelm@28907
   106
The simple wrapper script /home/isabelle/mercurial/bin/hg provides a
wenzelm@28907
   107
uniform view on the different Linux installations on the local
wenzelm@28907
   108
network.  Thus it is advisable to add that directory to the shell PATH
wenzelm@28907
   109
of the account at TUM:
wenzelm@28907
   110
wenzelm@28907
   111
  PATH="/home/isabelle/mercurial/bin:$PATH"
wenzelm@28907
   112
wenzelm@28907
   113
Now a clone of the shared push/pull area can be produced like this,
wenzelm@28907
   114
using your user name instead of "wenzelm":
wenzelm@28907
   115
wenzelm@28907
   116
  hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
wenzelm@28907
   117
wenzelm@28907
   118
In fact, the only difference to the previous clone of
wenzelm@28908
   119
http://isabelle.in.tum.de/repos/isabelle is a different default
wenzelm@28907
   120
pull/push path in isabelle/.hg/hgrc:
wenzelm@28907
   121
wenzelm@28907
   122
  [paths]
wenzelm@28907
   123
  default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
wenzelm@28907
   124
wenzelm@28907
   125
This means an earlier pull-only clone can be changed into a pull/push
wenzelm@28907
   126
version by editing this single line of the internal repository
wenzelm@28907
   127
configuration.
wenzelm@28907
   128
wenzelm@28907
   129
wenzelm@28907
   130
Content discipline
wenzelm@28907
   131
==================
wenzelm@28907
   132
wenzelm@28907
   133
Old-style centralized version control is occasionally compared with a
wenzelm@28907
   134
"library where everybody scribbles into the books".  Or seen the other
wenzelm@28907
   135
way round, the centralized model discourages individual
wenzelm@28907
   136
experimentation (with local branches etc.), because everything is
wenzelm@28907
   137
forced to happen on a shared file space.  With Mercurial, arbitrary
wenzelm@28907
   138
variations on local clones are no problem, but care is required again
wenzelm@28907
   139
when publishing changes eventually.
wenzelm@28907
   140
wenzelm@28907
   141
The following principles should be kept in mind when producing
wenzelm@28907
   142
changesets that might become public at some point.
wenzelm@28907
   143
wenzelm@28907
   144
  * The author of changes should be properly identified, using
wenzelm@28907
   145
    ui/username configuration as described above.
wenzelm@28907
   146
wenzelm@28907
   147
    While Mercurial also provides means for signed changesets, we want
wenzelm@28907
   148
    to keep things simple and trust that users specify their identity
wenzelm@28907
   149
    correctly.
wenzelm@28907
   150
wenzelm@28907
   151
  * The history of sources is an integral part of the sources
wenzelm@28907
   152
    themselves.  This means that private experiments and branches
wenzelm@28907
   153
    should not be published, unless they are really meant to become
wenzelm@28907
   154
    universally available.
wenzelm@28907
   155
wenzelm@28907
   156
    Note that exchanging local experiments with some other users can
wenzelm@28907
   157
    be done directly on peer-to-peer basis, without affecting the
wenzelm@28907
   158
    central pull/push area.
wenzelm@28907
   159
wenzelm@28907
   160
  * Log messages are an integral part of the history of sources.
wenzelm@28907
   161
    Other users will have to look there eventually, to understand why
wenzelm@28907
   162
    things have been done in a certain way at some point.
wenzelm@28907
   163
wenzelm@28907
   164
    Mercurial provides nice web presentation of incoming changes with
wenzelm@28908
   165
    a digest of log entries; this also includes RSS/Atom news feeds.
wenzelm@28907
   166
    Users should be aware that others will actually read what is
wenzelm@28907
   167
    written into log messages.
wenzelm@28907
   168
wenzelm@28907
   169
    The usual changelog presentation style for the Isabelle repository
wenzelm@28907
   170
    admits log entries that consist of several lines, but without the
wenzelm@28907
   171
    special head line that is used in Mercurial projects elsewhere.
wenzelm@28907
   172
    Since some display styles strip newlines from text, it is
wenzelm@28907
   173
    advisable to separate lines via punctuation, and not rely on
wenzelm@28907
   174
    two-dimensional presentation too much.
wenzelm@28907
   175
wenzelm@28907
   176
wenzelm@28908
   177
Building Isabelle from the repository version
wenzelm@28908
   178
=============================================
wenzelm@28908
   179
wenzelm@28910
   180
Compared to a proper distribution or development snapshot, a
wenzelm@28908
   181
repository version of Isabelle lacks proper version identifiers in
wenzelm@28910
   182
various places, and some components produced by Admin/build.  After
wenzelm@28908
   183
applying that script with suitable options, the regular user
wenzelm@28908
   184
instructions for building and running Isabelle from sources apply.
wenzelm@28908
   185
wenzelm@28908
   186
Needless to say, the results from the build process must not be
wenzelm@28908
   187
committed back into the repository!
wenzelm@28908
   188
wenzelm@28908
   189
wenzelm@28907
   190
Makarius 29-Nov-2008