README
1The Isabelle System Distribution
2================================
3
4Version information
5-------------------
6
7This is some repository version of Isabelle.
8
9See the NEWS file in the distribution for details on user-relevant
10changes.
11
12
13Installation
14------------
15
16Isabelle works on the three main platform families: Linux, Windows,
17and macOS. The application bundles from the Isabelle web page
18include sources, documentation, and add-on tools for all supported
19platforms.
20
21Some technical background information may be found in the Isabelle
22System Manual (directory doc).
23
24
25User interface
26--------------
27
28Isabelle/jEdit is an advanced Prover IDE based on jEdit and
29Isabelle/Scala. It is the main example application of the
30Isabelle/PIDE framework, and the default user interface of
31Isabelle. It provides a metaphor of continuous proof checking of a
32versioned collection of theory sources, with instantaneous feedback
33in real-time and rich semantic markup associated with the formal
34text.
35
36
37Other sources of information
38----------------------------
39
40 * The Isabelle Page
41
42 The Isabelle home page may be accessed from the following mirror
43 sites:
44
45 * https://www.cl.cam.ac.uk/research/hvg/Isabelle
46 * https://isabelle.in.tum.de
47 * https://mirror.cse.unsw.edu.au/pub/isabelle
48 * https://mirror.clarkson.edu/isabelle
49
50 * Mailing list
51
52 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
53 forum for Isabelle users to discuss problems and exchange
54 information. To join, send a message to
55 isabelle-users-request@cl.cam.ac.uk.
56
57 * Personal mail
58
59 Lawrence C Paulson
60 Computer Laboratory
61 University of Cambridge
62 JJ Thomson Avenue
63 Cambridge CB3 0FD
64 England
65 E-mail: lcp@cl.cam.ac.uk
66 Phone: +44-223-763500
67 Fax: +44-223-334748
68
69 or
70
71 Tobias Nipkow
72 Institut f��r Informatik
73 Technische Universit��t M��nchen
74 Boltzmannstr. 3
75 D-85748 Garching
76 Germany
77 E-mail: nipkow@in.tum.de
78 Phone: +49-89-289-17302
79 Fax: +49-89-289-17307
80
81NOTE:
82 Please report any problems you encounter. While we shall try to be
83 helpful, we can accept no responsibility for the deficiencies of
84 Isabelle and their consequences.
85
README_REPOSITORY
1Important notes on Mercurial repository access for Isabelle
2===========================================================
3
4Quick start in 30min
5--------------------
6
71a. Linux and Mac OS X: ensure that Mercurial is installed
8 (see also https://www.mercurial-scm.org)
9
101b. Windows: ensure that Cygwin64 with curl and Mercurial is installed
11 (see also https://www.cygwin.com)
12
132. Clone repository (bash shell commands):
14
15 hg clone https://isabelle.in.tum.de/repos/isabelle
16
17 cd isabelle
18
19 ./bin/isabelle components -I
20
21 ./bin/isabelle components -a
22
23 ./bin/isabelle jedit -l HOL
24
25 ./bin/isabelle build -b HOL #optional: build session image manually
26
273. Update repository (bash shell commands):
28
29 cd isabelle
30
31 hg pull -u
32
33 ./bin/isabelle components -a
34
35 ./bin/isabelle jedit -l HOL
36
37 ./bin/isabelle jedit -b -f #optional: force fresh build of Isabelle/Scala
38
394. Access documentation (bash shell commands):
40
41 ./bin/isabelle build_doc -a
42
43 ./bin/isabelle doc system
44
45
46Introduction
47------------
48
49Mercurial https://www.mercurial-scm.org belongs to source code
50management systems that follow the so-called paradigm of "distributed
51version control". This means plain revision control without the
52legacy of CVS or SVN (and without the extra complexity introduced by
53git). See also http://hginit.com/ for an introduction to the main
54ideas. The Mercurial book http://hgbook.red-bean.com/ explains many
55more details.
56
57Mercurial offers some flexibility in organizing the flow of changes,
58both between individual developers and designated pull/push areas that
59are shared with others. This additional freedom demands additional
60responsibility to maintain a certain development process that fits to
61a particular project.
62
63Regular Mercurial operations are strictly monotonic, where changeset
64transactions are only added, but never deleted or mutated. There are
65special tools to manipulate repositories via non-monotonic actions
66(such as "rollback" or "strip"), but recovering from gross mistakes
67that have escaped into the public can be hard and embarrassing. It is
68much easier to inspect and amend changesets routinely before pushing.
69
70The effect of the critical "pull" / "push" operations can be tested in
71a dry run via "incoming" / "outgoing". The "fetch" extension includes
72useful sanity checks beyond raw "pull" / "update" / "merge", although
73it has lost popularity in recent years. Most other operations are
74local to the user's repository clone. This gives some freedom for
75experimentation without affecting anybody else.
76
77Mercurial provides nice web presentation of incoming changes with a
78digest of log entries; this also includes RSS/Atom news feeds. There
79are add-on history browsers such as "hg view" and TortoiseHg. Unlike
80the default web view, some of these tools help to inspect the semantic
81content of non-trivial merge nodes.
82
83
84Initial configuration
85---------------------
86
87The main Isabelle repository can be cloned like this:
88
89 hg clone https://isabelle.in.tum.de/repos/isabelle
90
91This will create a local directory "isabelle", unless an alternative
92name is specified. The full repository meta-data and history of
93changes is in isabelle/.hg; local configuration for this clone can be
94added to isabelle/.hg/hgrc, but note that hgrc files are never copied
95by another clone operation.
96
97
98There is also $HOME/.hgrc for per-user Mercurial configuration. The
99initial configuration requires at least an entry to identify yourself
100as follows:
101
102 [ui]
103 username = XXX
104
105Isabelle contributors are free to choose either a short "login name"
106(for accounts at TU Munich) or a "full name" -- with or without mail
107address. It is important to stick to this choice once and for all.
108The machine default that Mercurial produces for unspecified
109[ui]username is not appropriate.
110
111Such configuration can be given in $HOME/.hgrc (for each home
112directory on each machine) or in .hg/hgrc (for each repository clone).
113
114
115Here are some further examples for hgrc. This is how to provide
116default options for common commands:
117
118 [defaults]
119 log = -l 10
120
121This is how to configure some extension, which is called "graphlog"
122and provides the "glog" command:
123
124 [extensions]
125 hgext.graphlog =
126
127
128Shared pull/push access
129-----------------------
130
131The entry point https://isabelle.in.tum.de/repos/isabelle is world
132readable, both via plain web browsing and the hg client as described
133above. Anybody can produce a clone, change it locally, and then use
134regular mechanisms of Mercurial to report changes upstream, say via
135mail to someone with write access to that file space. It is also
136quite easy to publish changed clones again on the web, using the
137ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts
138that are included in the Mercurial distribution, and send a "pull
139request" to someone else. There are also public hosting services for
140Mercurial repositories, notably Bitbucket.
141
142The downstream/upstream mode of operation is quite common in the
143distributed version control community, and works well for occasional
144changes produced by anybody out there. Of course, upstream
145maintainers need to review and moderate changes being proposed, before
146pushing anything onto the official Isabelle repository at TUM. Direct
147pushes are also reviewed routinely in a post-hoc fashion; everybody
148hooked on the main repository is called to keep an eye on incoming
149changes. In any case, changesets need to be understandable, both at
150the time of writing and many years later.
151
152Push access to the Isabelle repository requires an account at TUM,
153with properly configured ssh to isabelle-server.in.tum.de. You also
154need to be a member of the "isabelle" Unix group.
155
156Sharing a locally modified clone then works as follows, using your
157user name instead of "wenzelm":
158
159 hg out ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
160
161In fact, the "out" or "outgoing" command performs only a dry run: it
162displays the changesets that would get published. An actual "push",
163with a lasting effect on the Isabelle repository, works like this:
164
165 hg push ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
166
167
168Default paths for push and pull can be configured in
169isabelle/.hg/hgrc, for example:
170
171 [paths]
172 default = ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
173
174Now "hg pull" or "hg push" will use that shared file space, unless a
175different URL is specified explicitly.
176
177When cloning a repository, the default path is set to the initial
178source URL. So we could have cloned via that ssh URL in the first
179place, to get exactly to the same point:
180
181 hg clone ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
182
183
184Simple merges
185-------------
186
187The main idea of Mercurial is to let individual users produce
188independent branches of development first, but merge with others
189frequently. The basic hg merge operation is more general than
190required for the mode of operation with a shared pull/push area. The
191"fetch" extension accommodates this case nicely, automating trivial
192merges and requiring manual intervention for actual conflicts only.
193
194The fetch extension can be configured via $HOME/.hgrc like this:
195
196 [extensions]
197 hgext.fetch =
198
199 [defaults]
200 fetch = -m "merged"
201
202To keep merges semantically trivial and prevent genuine merge
203conflicts or lost updates, it is essential to observe to following
204general discipline wrt. the public Isabelle push area:
205
206 * Before editing, pull or fetch the latest version.
207
208 * Accumulate private commits for a maximum of 1-3 days.
209
210 * Start publishing again by pull or fetch, which normally produces
211 local merges.
212
213 * Test the merged result, e.g. like this:
214
215 isabelle build -a
216
217 * Push back in real time.
218
219Piling private changes and public merges longer than 0.5-2 hours is
220apt to produce some mess when pushing eventually!
221
222The pull-test-push cycle should not be repeated too fast, to avoid
223delaying others from doing the same concurrently.
224
225
226Content discipline
227------------------
228
229The following principles should be kept in mind when producing
230changesets that are meant to be published at some point.
231
232 * The author of changes needs to be properly identified, using
233 [ui]username configuration as described above.
234
235 While Mercurial also provides means for signed changesets, we want
236 to keep things simple and trust that users specify their identity
237 correctly (and uniquely).
238
239 * The history of sources is an integral part of the sources
240 themselves. This means that private experiments and branches
241 should not be published by accident. Named branches are not
242 allowed on the public version. Note that old SVN-style branching
243 is replaced by regular repository clones in Mercurial.
244
245 Exchanging local experiments with some other users can be done
246 directly on peer-to-peer basis, without affecting the central
247 pull/push area.
248
249 * Log messages are an integral part of the history of sources.
250 Other people will have to inspect them routinely, to understand
251 why things have been done in a certain way at some point.
252
253 Authors of log entries should be aware that published changes are
254 actually read. The main point is not to announce novelties, but
255 to describe faithfully what has been done, and provide some clues
256 about the motivation behind it. The main recipient is someone who
257 needs to understand the change in the distant future to isolate
258 problems. Sometimes it is helpful to reference past changes
259 formally via changeset ids in the log entry.
260
261 * The standard changelog entry format of the Isabelle repository
262 admits several (somehow related) items to be rolled into one
263 changeset. Each item is then described on a separate line that
264 may become longer as screen line and is terminated by punctuation.
265 These lines are roughly ordered by importance.
266
267 This format conforms to established Isabelle tradition. In
268 contrast, the default of Mercurial prefers a single headline
269 followed by a long body text. The reason for that is a somewhat
270 different development model of typical "distributed" projects,
271 where external changes pass through a hierarchy of reviewers and
272 maintainers, until they end up in some authoritative repository.
273 Isabelle changesets can be more spontaneous, growing from the
274 bottom-up.
275
276 The web style of https://isabelle.in.tum.de/repos/isabelle
277 accommodates the Isabelle changelog format. Note that multiple
278 lines will sometimes display as a single paragraph in HTML, so
279 some terminating punctuation is required. Do not squeeze multiple
280 items on the same line in the original text!
281
282
283Testing of changes (before push)
284--------------------------------
285
286The integrity of the standard pull/push area of Isabelle needs the be
287preserved at all time. This means that a complete test with default
288configuration needs to be finished successfully before push. If the
289preparation of the push involves a pull/merge phase, its result needs
290to covered by the test as well.
291
292There are several possibilities to perform the test, e.g. using the
293Isabelle testboard at TUM. In contrast, the subsequent command-line
294examples are for tests on the local machine:
295
296 ./bin/isabelle build -a #regular test
297
298 ./bin/isabelle build -a -o document=pdf #test with document preparation (optional)
299
300 ./bin/isabelle build -a -j2 -o threads=4 #test on multiple cores (example)
301
302See also the chapter on Isabelle sessions and build management in the
303"system" manual. The build option -S is particularly useful for quick
304tests of individual commits, e.g. for each step of a longer chain of
305changes, but the final push always requires a full test as above!
306
307Note that implicit dependencies on Isabelle components are specified
308via catalog files in $ISABELLE_HOME/Admin/components/ as part of the
309Mercurial history. This allows to bisect over a range of Isabelle
310versions while references to the contributing components change
311accordingly. Recall that "isabelle components -a" updates the local
312component store monotonically according to that information, and thus
313resolves missing components.
314