1 100721 download Isabelle repository + install runnable system
2 ===========================================================WN
4 # clone the munich repository
5 #/usr/local$ sudo hg clone http://isabelle.in.tum.de/repos/isabelle isabisac
7 # clone the IST repository
8 /usr/local$ sudo hg clone -U https://intra.ist.tugraz.at/hg/isa/ isabisac #changesets
9 /usr/local/isabisac$ sudo hg update -C 875b6efa7ced #from tip ??why nothttps://..
10 /usr/local/isabisac$ sudo chown -R neuper * #become owner
11 hg update -C Isabelle2009-2 #go to release
12 hg branch isac-from-Isabelle2009-2 #make branch
15 # download Isabelle2009-2 distribution, cp missing dirs to repository
16 ~/Downloads/Isabelle2009-2$ sudo cp -r contrib/ /usr/local/isabisac/
17 sudo cp -r heaps/ /usr/local/isabisac/
18 /usr/local$ ln -s isabisac Isabelle
20 export SCALA_HOME=/usr/local/isabisac/contrib/scala-2.8.0.RC5
21 isabisac/Admin$ ./build jars
23 !test runnable distribution!
25 # insert the isac-hooks in Pure/thm.ML into isabelle
28 # cp isac into the repository
29 ...$ cp -r isac /usr/local/isabisac/src/Pure
30 hg add .......................
36 Important notes on Mercurial repository access for Isabelle
37 ===========================================================
42 Mercurial http://www.selenic.com/mercurial belongs to the current
43 generation of source code management systems that follow the so-called
44 paradigm of "distributed version control". This is a terrific name
45 for plain revision control without the legacy of CVS or SVN. See also
46 http://hginit.com/ for an introduction to the main ideas. The
47 Mercurial book http://hgbook.red-bean.com/ explains many more details.
49 Mercurial offers great flexibility in organizing the flow of changes,
50 both between individual developers and designated pull/push areas that
51 are shared with others. This additional power demands some additional
52 responsibility to maintain a certain development process that fits to
55 Regular Mercurial operations are strictly monotonic, where changeset
56 transactions are only added, but never deleted. There are special
57 tools to manipulate repositories via non-monotonic actions (such as
58 "rollback" or "strip"), but recovering from gross mistakes that have
59 escaped into the public can be hard and embarrassing. It is much
60 easier to inspect and amend changesets routinely before pushing.
62 The effect of the critical "pull" / "push" operations can be tested in
63 a dry run via "incoming" / "outgoing". The "fetch" extension includes
64 useful sanity checks beyond raw "pull" / "update" / "merge". Most
65 other operations are local to the user's repository clone. This gives
66 some freedom for experimentation without affecting anybody else.
68 Mercurial provides nice web presentation of incoming changes with a
69 digest of log entries; this also includes RSS/Atom news feeds. There
70 are add-on browsers, notably hgtk that is part of the TortoiseHg
71 distribution and works for generic Python/GTk platforms. The
72 alternative "view" utility helps to inspect the semantic content of
79 The official Isabelle repository can be cloned like this:
81 hg clone http://isabelle.in.tum.de/repos/isabelle
83 This will create a local directory "isabelle", unless an alternative
84 name is specified. The full repository meta-data and history of
85 changes is in isabelle/.hg; local configuration for this clone can be
86 added to isabelle/.hg/hgrc, but note that hgrc files are never copied
87 by another clone operation.
90 There is also $HOME/.hgrc for per-user Mercurial configuration. The
91 initial configuration requires at least an entry to identify yourself
97 Isabelle contributors are free to choose either a short "login name"
98 (for accounts at TU Munich) or a "full name" -- with or without mail
99 address. It is important to stick to this choice once and for all.
100 The machine default that Mercurial produces for unspecified
101 [ui]username is not appropriate.
103 Such configuration can be given in $HOME/.hgrc (for each home
104 directory on each machine) or in .hg/hgrc (for each repository clone).
107 Here are some further examples for hgrc. This is how to provide
108 default options for common commands:
113 This is how to configure some extension, which is called "graphlog"
114 and provides the "glog" command:
120 Shared pull/push access
121 -----------------------
123 The entry point http://isabelle.in.tum.de/repos/isabelle is world
124 readable, both via plain web browsing and the hg client as described
125 above. Anybody can produce a clone, change it locally, and then use
126 regular mechanisms of Mercurial to report changes upstream, say via
127 mail to someone with write access to that file space. It is also
128 quite easy to publish changed clones again on the web, using the
129 ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
130 that are included in the Mercurial distribution, and send a "pull
131 request" to someone else. There are also public hosting services for
132 Mercurial repositories.
134 The downstream/upstream mode of operation is quite common in the
135 distributed version control community, and works well for occasional
136 changes produced by anybody out there. Of course, upstream
137 maintainers need to review and moderate changes being proposed, before
138 pushing anything onto the official Isabelle repository at TUM. Direct
139 pushes are also reviewed routinely in a post-hoc fashion; everybody
140 hooked on the main repository is called to keep an eye on incoming
141 changes. In any case, changesets need to be understandable, at the
142 time of writing and many years later.
144 Push access to the Isabelle repository requires an account at TUM,
145 with properly configured ssh to the local machines (e.g. macbroy20,
146 atbroy100). You also need to be a member of the "isabelle" Unix
149 Sharing a locally modified clone then works as follows, using your
150 user name instead of "wenzelm":
152 hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
154 In fact, the "out" or "outgoing" command performs only a dry run: it
155 displays the changesets that would get published. An actual "push",
156 with a lasting effect on the Isabelle repository, works like this:
158 hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
161 Default paths for push and pull can be configured in
162 isabelle/.hg/hgrc, for example:
165 default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
167 Now "hg pull" or "hg push" will use that shared file space, unless a
168 different URL is specified explicitly.
170 When cloning a repository, the default path is set to the initial
171 source URL. So we could have cloned via that ssh URL in the first
172 place, to get exactly to the same point:
174 hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
180 The main idea of Mercurial is to let individual users produce
181 independent branches of development first, but merge with others
182 frequently. The basic hg merge operation is more general than
183 required for the mode of operation with a shared pull/push area. The
184 "fetch" extension accommodates this case nicely, automating trivial
185 merges and requiring manual intervention for actual conflicts only.
187 The fetch extension can be configured via $HOME/.hgrc like this:
195 To keep merges semantically trivial and prevent genuine merge
196 conflicts or lost updates, it is essential to observe to following
197 general discipline wrt. the public Isabelle push area:
199 * Before editing, pull or fetch the latest version.
201 * Accumulate private commits for a maximum of 1-3 days.
203 * Start publishing again by pull or fetch, which normally produces
206 * Test the merged result as usual and push back in real time.
208 Piling private changes and public merges longer than 0.5-2 hours is
209 apt to produce some mess when pushing eventually!
215 The following principles should be kept in mind when producing
216 changesets that are meant to be published at some point.
218 * The author of changes needs to be properly identified, using
219 [ui]username configuration as described above.
221 While Mercurial also provides means for signed changesets, we want
222 to keep things simple and trust that users specify their identity
223 correctly (and uniquely).
225 * The history of sources is an integral part of the sources
226 themselves. This means that private experiments and branches
227 should not be published by accident. Named branches are not
228 allowed on the public version. Note that old SVN-style branching
229 is replaced by regular repository clones in Mercurial.
231 Exchanging local experiments with some other users can be done
232 directly on peer-to-peer basis, without affecting the central
235 * Log messages are an integral part of the history of sources.
236 Other people will have to inspect them routinely, to understand
237 why things have been done in a certain way at some point.
239 Authors of log entries should be aware that published changes are
240 actually read. The main point is not to announce novelties, but
241 to describe faithfully what has been done, and provide some clues
242 about the motivation behind it. The main recipient is someone who
243 needs to understand the change in the distant future to isolate
244 problems. Sometimes it is helpful to reference past changes via
245 changeset ids in the log entry.
247 * The standard changelog entry format of the Isabelle repository
248 admits several (vaguely related) items to be rolled into one
249 changeset. Each item is then described on a separate line that
250 may become longer as screen line and is terminated by punctuation.
251 These lines are roughly ordered by importance.
253 This format conforms to established Isabelle tradition. In
254 contrast, the default of Mercurial prefers a single headline
255 followed by a long body text. The reason for that is a somewhat
256 different development model of typical "distributed" projects,
257 where external changes pass through a hierarchy of reviewers and
258 maintainers, until they end up in some authoritative repository.
259 Isabelle changesets can be more spontaneous, growing from the
262 The web style of http://isabelle.in.tum.de/repos/isabelle/
263 accommodates the Isabelle changelog format. Note that multiple
264 lines will sometimes display as a single paragraph in HTML, so
265 some terminating punctuation is required. Do not squeeze multiple
266 items on the same line in the original text!
269 Building a repository version of Isabelle
270 -----------------------------------------
272 Compared to a proper distribution or development snapshot, it is
273 relatively hard to build from the raw repository version. Essential
274 contributing components are missing and need to be reconstructed by
275 running the Admin/build script by hand. Afterwards the main Isabelle
276 system and logic images can be compiled via the toplevel ./build
277 script. Note that the repository lacks some textual version
278 identifiers in the sources and scripts; this implies some changed
279 behavior when processing settings etc.
281 There is no guarantee that the NEWS file is up to date at an arbitrary