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