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