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