README_REPOSITORY
author wenzelm
Tue, 19 Apr 2011 15:58:05 +0200
changeset 42403 38b29c9fc742
parent 40601 021278fdd0a8
child 47449 5e1482296b12
permissions -rw-r--r--
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
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
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
     4
Introduction
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
     5
------------
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
     6
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
     7
Mercurial http://www.selenic.com/mercurial belongs to the current
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
     8
generation of source code management systems that follow the so-called
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
     9
paradigm of "distributed version control".  This is a terrific name
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    10
for plain revision control without the legacy of CVS or SVN.  See also
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    11
http://hginit.com/ for an introduction to the main ideas.  The
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    12
Mercurial book http://hgbook.red-bean.com/ explains many more details.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    13
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    14
Mercurial offers great flexibility in organizing the flow of changes,
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    15
both between individual developers and designated pull/push areas that
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    16
are shared with others.  This additional power demands some additional
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    17
responsibility to maintain a certain development process that fits to
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    18
a particular project.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    19
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    20
Regular Mercurial operations are strictly monotonic, where changeset
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    21
transactions are only added, but never deleted.  There are special
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    22
tools to manipulate repositories via non-monotonic actions (such as
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    23
"rollback" or "strip"), but recovering from gross mistakes that have
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    24
escaped into the public can be hard and embarrassing.  It is much
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    25
easier to inspect and amend changesets routinely before pushing.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    26
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    27
The effect of the critical "pull" / "push" operations can be tested in
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    28
a dry run via "incoming" / "outgoing".  The "fetch" extension includes
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    29
useful sanity checks beyond raw "pull" / "update" / "merge".  Most
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    30
other operations are local to the user's repository clone.  This gives
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    31
some freedom for experimentation without affecting anybody else.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    32
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    33
Mercurial provides nice web presentation of incoming changes with a
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    34
digest of log entries; this also includes RSS/Atom news feeds.  There
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    35
are add-on browsers, notably hgtk that is part of the TortoiseHg
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    36
distribution and works for generic Python/GTk platforms.  The
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    37
alternative "view" utility helps to inspect the semantic content of
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    38
merge nodes.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    39
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    40
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    41
Initial configuration
29481
3e8420c1124a tuned ASCII art;
wenzelm
parents: 28918
diff changeset
    42
---------------------
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    43
28913
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
    44
The official Isabelle repository can be cloned like this:
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    45
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    46
  hg clone http://isabelle.in.tum.de/repos/isabelle
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    47
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    48
This will create a local directory "isabelle", unless an alternative
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    49
name is specified.  The full repository meta-data and history of
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    50
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
    51
added to isabelle/.hg/hgrc, but note that hgrc files are never copied
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    52
by another clone operation.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    53
28917
wenzelm
parents: 28913
diff changeset
    54
28913
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
    55
There is also $HOME/.hgrc for per-user Mercurial configuration.  The
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    56
initial configuration requires at least an entry to identify yourself
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    57
as follows:
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    58
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    59
  [ui]
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    60
  username = XXX
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    61
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    62
Isabelle contributors are free to choose either a short "login name"
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    63
(for accounts at TU Munich) or a "full name" -- with or without mail
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    64
address.  It is important to stick to this choice once and for all.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    65
The machine default that Mercurial produces for unspecified
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    66
[ui]username is not appropriate.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    67
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    68
Such configuration can be given in $HOME/.hgrc (for each home
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    69
directory on each machine) or in .hg/hgrc (for each repository clone).
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    70
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    71
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    72
Here are some further examples for hgrc.  This is how to provide
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    73
default options for common commands:
28907
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
  [defaults]
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    76
  log = -l 10
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    77
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    78
This is how to configure some extension, which is called "graphlog"
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    79
and provides the "glog" command:
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    80
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    81
  [extensions]
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    82
  hgext.graphlog =
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
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    85
Shared pull/push access
29481
3e8420c1124a tuned ASCII art;
wenzelm
parents: 28918
diff changeset
    86
-----------------------
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    87
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
    88
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
    89
readable, both via plain web browsing and the hg client as described
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    90
above.  Anybody can produce a clone, change it locally, and then use
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    91
regular mechanisms of Mercurial to report changes upstream, say via
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    92
mail to someone with write access to that file space.  It is also
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    93
quite easy to publish changed clones again on the web, using the
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    94
ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    95
that are included in the Mercurial distribution, and send a "pull
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    96
request" to someone else.  There are also public hosting services for
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
    97
Mercurial repositories.
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
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   103
pushing anything onto the official Isabelle repository at TUM.  Direct
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   104
pushes are also reviewed routinely in a post-hoc fashion; everybody
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   105
hooked on the main repository is called to keep an eye on incoming
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   106
changes.  In any case, changesets need to be understandable, at the
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   107
time of writing and many years later.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   108
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   109
Push access to the Isabelle repository requires an account at TUM,
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   110
with properly configured ssh to the local machines (e.g. macbroy20,
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   111
atbroy100).  You also need to be a member of the "isabelle" Unix
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   112
group.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   113
28913
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   114
Sharing a locally modified clone then works as follows, using your
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   115
user name instead of "wenzelm":
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   116
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   117
  hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   118
28913
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   119
In fact, the "out" or "outgoing" command performs only a dry run: it
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   120
displays the changesets that would get published.  An actual "push",
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   121
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
   122
28913
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   123
  hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   124
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   125
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   126
Default paths for push and pull can be configured in
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   127
isabelle/.hg/hgrc, for example:
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   128
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   129
  [paths]
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   130
  default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   131
28913
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   132
Now "hg pull" or "hg push" will use that shared file space, unless a
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   133
different URL is specified explicitly.
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   134
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   135
When cloning a repository, the default path is set to the initial
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   136
source URL.  So we could have cloned via that ssh URL in the first
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   137
place, to get exactly to the same point:
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   138
86ed1c86e0ef misc tuning and clarification;
wenzelm
parents: 28910
diff changeset
   139
  hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   140
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   141
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   142
Simple merges
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   143
-------------
30182
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   144
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   145
The main idea of Mercurial is to let individual users produce
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   146
independent branches of development first, but merge with others
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   147
frequently.  The basic hg merge operation is more general than
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   148
required for the mode of operation with a shared pull/push area.  The
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   149
"fetch" extension accommodates this case nicely, automating trivial
30182
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   150
merges and requiring manual intervention for actual conflicts only.
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   151
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   152
The fetch extension can be configured via $HOME/.hgrc like this:
30182
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   153
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   154
  [extensions]
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   155
  hgext.fetch =
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   156
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   157
  [defaults]
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   158
  fetch = -m "merged"
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   159
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   160
To keep merges semantically trivial and prevent genuine merge
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   161
conflicts or lost updates, it is essential to observe to following
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   162
general discipline wrt. the public Isabelle push area:
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   163
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   164
  * Before editing, pull or fetch the latest version.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   165
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   166
  * Accumulate private commits for a maximum of 1-3 days.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   167
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   168
  * Start publishing again by pull or fetch, which normally produces
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   169
    local merges.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   170
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   171
  * Test the merged result as usual and push back in real time.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   172
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   173
Piling private changes and public merges longer than 0.5-2 hours is
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   174
apt to produce some mess when pushing eventually!
30182
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   175
db768c888dfa minor update of Mercurial HOWTO;
wenzelm
parents: 29481
diff changeset
   176
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   177
Content discipline
29481
3e8420c1124a tuned ASCII art;
wenzelm
parents: 28918
diff changeset
   178
------------------
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   179
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   180
The following principles should be kept in mind when producing
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   181
changesets that are meant to be published at some point.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   182
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   183
  * The author of changes needs to be properly identified, using
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   184
    [ui]username configuration as described above.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   185
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   186
    While Mercurial also provides means for signed changesets, we want
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   187
    to keep things simple and trust that users specify their identity
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   188
    correctly (and uniquely).
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   189
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   190
  * The history of sources is an integral part of the sources
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   191
    themselves.  This means that private experiments and branches
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   192
    should not be published by accident.  Named branches are not
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   193
    allowed on the public version.  Note that old SVN-style branching
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   194
    is replaced by regular repository clones in Mercurial.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   195
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   196
    Exchanging local experiments with some other users can be done
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   197
    directly on peer-to-peer basis, without affecting the central
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   198
    pull/push area.
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
  * Log messages are an integral part of the history of sources.
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   201
    Other people will have to inspect them routinely, to understand
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   202
    why things have been done in a certain way at some point.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   203
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   204
    Authors of log entries should be aware that published changes are
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   205
    actually read.  The main point is not to announce novelties, but
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   206
    to describe faithfully what has been done, and provide some clues
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   207
    about the motivation behind it.  The main recipient is someone who
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   208
    needs to understand the change in the distant future to isolate
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   209
    problems.  Sometimes it is helpful to reference past changes via
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   210
    changeset ids in the log entry.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   211
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   212
  * The standard changelog entry format of the Isabelle repository
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   213
    admits several (vaguely related) items to be rolled into one
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   214
    changeset.  Each item is then described on a separate line that
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   215
    may become longer as screen line and is terminated by punctuation.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   216
    These lines are roughly ordered by importance.
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   217
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   218
    This format conforms to established Isabelle tradition.  In
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   219
    contrast, the default of Mercurial prefers a single headline
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   220
    followed by a long body text.  The reason for that is a somewhat
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   221
    different development model of typical "distributed" projects,
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   222
    where external changes pass through a hierarchy of reviewers and
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   223
    maintainers, until they end up in some authoritative repository.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   224
    Isabelle changesets can be more spontaneous, growing from the
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   225
    bottom-up.
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   226
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   227
    The web style of http://isabelle.in.tum.de/repos/isabelle/
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   228
    accommodates the Isabelle changelog format.  Note that multiple
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   229
    lines will sometimes display as a single paragraph in HTML, so
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   230
    some terminating punctuation is required.  Do not squeeze multiple
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   231
    items on the same line in the original text!
28907
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   232
1a470f95ef18 Important notes on Mercurial repository access for Isabelle.
wenzelm
parents:
diff changeset
   233
32361
141e5151b918 clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
wenzelm
parents: 30182
diff changeset
   234
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
   235
-----------------------------------------
28908
4571302e1594 further notes;
wenzelm
parents: 28907
diff changeset
   236
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   237
Compared to a proper distribution or development snapshot, it is
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   238
relatively hard to build from the raw repository version.  Essential
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   239
contributing components are missing and need to be reconstructed by
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   240
running the Admin/build script by hand.  Afterwards the main Isabelle
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   241
system and logic images can be compiled via the toplevel ./build
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   242
script.  Note that the repository lacks some textual version
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   243
identifiers in the sources and scripts; this implies some changed
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   244
behavior when processing settings etc.
28908
4571302e1594 further notes;
wenzelm
parents: 28907
diff changeset
   245
40601
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   246
There is no guarantee that the NEWS file is up to date at an arbitrary
021278fdd0a8 some updates after 2 years of Mercurial usage;
wenzelm
parents: 36858
diff changeset
   247
point in history.