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