updated "op +", "op -", "op *". "HOL.divide" in src & test
find . -type f -exec sed -i s/"\"op +\""/"\"Groups.plus_class.plus\""/g {} \;
find . -type f -exec sed -i s/"\"op -\""/"\"Groups.minus_class.minus\""/g {} \;
find . -type f -exec sed -i s/"\"op *\""/"\"Groups.times_class.times\""/g {} \;
find . -type f -exec sed -i s/"\"HOL.divide\""/"\"Rings.inverse_class.divide\""/g {} \;
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 a new generation
43 of source code management systems, following the paradigm of
44 "distributed version control". Compared to the old centralized model
45 of CVS or SVN, this gives considerable more power and freedom in
46 organizing the flow of changes, both between individual developers and
47 designated pull/push areas that are shared with others.
49 More power for the user also means more responsibility! Due to its
50 decentralized nature, changesets that have been published once,
51 e.g. via "push" to a shared repository that is visible on the net,
52 cannot be easily retracted from the public again. Regular Mercurial
53 operations are strictly monotonic, where changset transactions are
54 only added, but never deleted. There are special tools to manipulate
55 individual repositories via non-monotonic actions, but this does not
56 yet retrieve any changesets that have escaped into the public by
59 Only global operations like "pull" and "push" fall into this critical
60 category. Note that "incoming" / "outgoing" allow to inspect
61 changesets before exchanging them globally. Anything else in
62 Mercurial is local to the user's repository clone (including "commit",
63 "update", "merge" etc.) and is in fact much simpler and safer to use
64 than the corresponding operations of CVS or SVN.
70 The official Isabelle repository can be cloned like this:
72 hg clone http://isabelle.in.tum.de/repos/isabelle
74 This will create a local directory "isabelle", unless an alternative
75 name is specified. The full repository meta-data and history of
76 changes is in isabelle/.hg; local configuration for this clone can be
77 added to isabelle/.hg/hgrc, but note that hgrc files are never copied
78 by another clone operation!
81 There is also $HOME/.hgrc for per-user Mercurial configuration. The
82 initial configuration should include at least an entry to identify
83 yourself. For example, something like this in /home/wenzelm/.hgrc:
88 Of course, the user identity can be also configured in
89 isabelle/.hg/hgrc on per-repository basis. Failing to specify the
90 username correctly makes the system invent funny machine names that
91 may persist indefinitely in the public flow of changesets.
93 In principle, user names can be chosen freely, but for longterm
94 committers of the Isabelle repository the obvious choice is to keep
95 with the old CVS naming scheme. Others should use their regular "full
96 name"; including an email address is optional.
99 There are other useful configuration to go into $HOME/.hgrc,
100 e.g. defaults for common commands:
105 The next example shows how to install some Mercurial extension:
110 Now the additional glog command will be available.
113 See also the fine documentation for further details, especially the
114 book http://hgbook.red-bean.com/
116 There is also a nice tutorial at http://hginit.com/
119 Shared pull/push access
120 -----------------------
122 The entry point http://isabelle.in.tum.de/repos/isabelle is world
123 readable, both via plain web browsing and the hg client as described
124 above. Anybody can produce a clone, change it arbitrarily, and then
125 use regular mechanisms of Mercurial to report changes upstream, say
126 via e-mail to someone with write access to that file space. It is
127 also quite easy to publish changed clones again on the web, using the
128 adhoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
129 that are included in the Mercurial distribution.
131 The downstream/upstream mode of operation is quite common in the
132 distributed version control community, and works well for occasional
133 changes produced by anybody out there. Of course, upstream
134 maintainers need to review and moderate changes being proposed, before
135 pushing anything onto the official Isabelle repository at TUM.
138 Write access to the Isabelle repository requires an account at TUM,
139 with properly configured ssh access to the local machines
140 (e.g. macbroy20, atbroy100). You also need to be a member of the
141 "isabelle" Unix group.
143 Sharing a locally modified clone then works as follows, using your
144 user name instead of "wenzelm":
146 hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
148 In fact, the "out" or "outgoing" command performs only a dry run: it
149 displays the changesets that would get published. An actual "push",
150 with a lasting effect on the Isabelle repository, works like this:
152 hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
155 Default paths for push and pull can be configure in isabelle/.hg/hgrc,
159 default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
161 Now "hg pull" or "hg push" will use that shared file space, unless a
162 different URL is specified explicitly.
164 When cloning a repository, the default path is set to the initial
165 source URL. So we could have cloned via that ssh URL in the first
166 place, to get exactly to the same point:
168 hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
174 The main idea of Mercurial is to let individual users produce
175 independent branches of development first, but merge with others
176 frequently. The basic hg merge operation is more general than
177 required for the mode of operation with a shared pull/push area. The
178 hg fetch extension accommodates this case nicely, automating trivial
179 merges and requiring manual intervention for actual conflicts only.
181 The fetch extension can be configured via the user's ~/.hgrc like
190 Note that the potential for merge conflicts can be greatly reduced by
191 doing "hg fetch" before any starting local changes!
197 Old-style centralized version control is occasionally compared to "a
198 library where everybody scribbles into the books". Or seen the other
199 way round, the centralized model discourages individual
200 experimentation (with local branches etc.), because everything is
201 forced to happen on a shared file space. With Mercurial, arbitrary
202 variations on local clones are no problem, but care is required again
203 when publishing changes eventually.
205 The following principles should be kept in mind when producing
206 changesets that might become public at some point.
208 * The author of changes should be properly identified, using
209 ui/username configuration as described above.
211 While Mercurial also provides means for signed changesets, we want
212 to keep things simple and trust that users specify their identity
215 * The history of sources is an integral part of the sources
216 themselves. This means that private experiments and branches
217 should not be published, unless they are really meant to become
218 universally available.
220 Note that exchanging local experiments with some other users can
221 be done directly on peer-to-peer basis, without affecting the
222 central pull/push area.
224 * Log messages are an integral part of the history of sources.
225 Other users will have to look there eventually, to understand why
226 things have been done in a certain way at some point.
228 Mercurial provides nice web presentation of incoming changes with
229 a digest of log entries; this also includes RSS/Atom news feeds.
230 Users should be aware that others will actually read what is
231 written into log messages. There are also add-on browsers,
232 notably hgtk that is part of the TortoiseHg distribution and works
233 for generic Python/GTk platforms.
235 The usual changelog presentation style for the Isabelle repository
236 admits log entries that consist of several lines, but without the
237 special headline that is used in Mercurial projects elsewhere.
238 Since some display styles strip newlines from text, it is
239 advisable to separate lines via punctuation, and not rely on
240 two-dimensional presentation too much.
243 Building a repository version of Isabelle
244 -----------------------------------------
246 Compared to a proper distribution or development snapshot, a
247 repository version of Isabelle lacks textual version identifiers in
248 some sources and scripts, and various components produced by
249 Admin/build are missing. After applying that script with suitable
250 arguments, the regular user instructions for building and running
251 Isabelle from sources apply.
253 Needless to say, the results from the build process must not be added