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