README_REPOSITORY
author Thomas Sewell <tsewell@nicta.com.au>
Fri, 25 Sep 2009 19:04:18 +1000
changeset 32754 4e0256f7d219
parent 32361 141e5151b918
child 35567 309e75c58af2
permissions -rw-r--r--
Avoid record-inner constants in polymorphic definitions in Bali The Bali package needs to insert a record extension into a type class and define an associated polymorphic constant. There is no elegant way to do this. The existing approach was to insert every record extension into the type class, defining the polymorphic constant at each layer using inner operations created by the record package. Some of those operations have been removed. They can be replaced by use of record_name.extend if necessary, but we can also sidestep this altogether. The simpler approach here is to use defs(overloaded) once to provide a single definition for the composition of all the type constructors, which seems to be permitted. This gets us exactly the fact we need, with the cost that some types that were admitted to the type class have no definition for the constant at all.
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
32361
141e5151b918 clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
wenzelm
parents: 30182
diff changeset
   211
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
   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!