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