11 <h1>The Isabelle System Distribution</h1> |
11 <h1>The Isabelle System Distribution</h1> |
12 |
12 |
13 <h2>Version information</h2> |
13 <h2>Version information</h2> |
14 |
14 |
15 This is the internal repository version of Isabelle. The current line |
15 This is the internal repository version of Isabelle. The current line |
16 of development introduces many new features, while attempting to keep |
16 of Isabelle99 development introduces many new concepts, while |
17 incompatibilities over Isabelle98-X at a minimum. See the |
17 attempting to keep incompatibilities over Isabelle98 at a minimum. |
18 <tt>NEWS</tt> file in the distribution for more details. |
18 See the <tt>NEWS</tt> file in the distribution for more details. |
19 |
19 |
20 |
20 |
21 <h2>System requirements</h2> |
21 <h2>System requirements</h2> |
22 |
22 |
23 Isabelle requires a real Unix box with sufficient resources. Fun |
23 Isabelle requires a real Unix box with sufficient resources. Fun |
24 starts at about 32-64 MB of free main memory (somewhat depending on |
24 starts at about 32-64 MB of free main memory (somewhat depending on |
25 your ML system), with several tens of MB disk space and a decent CPU. |
25 the ML system), with several tens of MB disk space and a decent CPU. |
26 Speaking by today's hardware standards, any moderate Linux box should |
26 Speaking by today's hardware standards, any moderate Linux box should |
27 give a very nice platform for Isabelle. |
27 give a very nice platform for Isabelle. |
28 |
28 |
29 <p> |
29 <p> |
30 |
30 |
40 <p> |
40 <p> |
41 |
41 |
42 The following ML system and platform combinations are known to work |
42 The following ML system and platform combinations are known to work |
43 very well: |
43 very well: |
44 <ul> |
44 <ul> |
45 <li> Poly/ML 3.x on Linux and Sparc/Solaris. |
45 <li> Poly/ML 3.x on Linux/x86 and Solaris/Sparc. |
46 <li> SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.). |
46 <li> SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.). |
47 </ul> |
47 </ul> |
48 |
48 |
49 <p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a |
49 <p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a |
50 commercial product, is back in the free world. It is by far the best |
50 commercial product, is back in the free world. It is by far the best |
66 top-level pretty printing) are not supported, though. |
66 top-level pretty printing) are not supported, though. |
67 |
67 |
68 |
68 |
69 <h2>Installation</h2> |
69 <h2>Installation</h2> |
70 |
70 |
71 RPM packages are available for Isabelle/HOL and ZF on the Linux/x86 |
71 Binary packages are available for Isabelle/HOL and ZF on the Linux/x86 |
72 platform. The system may be easily built from scratch as well, taking |
72 platform. The system may be easily built from scratch as well, taking |
73 the traditional tar.gz distribution. See file <tt>INSTALL</tt> as |
73 the traditional tar.gz source distribution. See file <tt>INSTALL</tt> |
74 distributed with Isabelle for more information. |
74 as distributed with Isabelle for more information. |
75 |
75 |
76 Further background information may be found in the <em>Isabelle System |
76 Further background information may be found in the <em>Isabelle System |
77 Manual</em>, distributed with the sources (directory <tt>doc</tt>). |
77 Manual</em>, distributed with the sources (directory <tt>doc</tt>). |
78 |
78 |
79 |
79 |
80 <h2>User interfaces</h2> |
80 <h2>User interface</h2> |
81 |
81 |
82 The distribution includes only a very primitive interface based on |
82 The canonical Isabelle user interface is <a |
83 ordinary terminal sessions. Advanced interfaces are available from |
83 href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by |
84 other sources: |
84 David Aspinall and others. It is a generic (X)Emacs interface for |
85 |
85 proof assistants, including Isabelle (both for the classic and Isar |
86 <ul> |
|
87 |
|
88 <li> |
|
89 <a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by |
|
90 David Aspinall and others is a generic Emacs interface for proof |
|
91 assistants, including Isabelle (both for the classic and Isar |
|
92 version). Proof General is suitable for use by pacifists and Emacs |
86 version). Proof General is suitable for use by pacifists and Emacs |
93 militants alike. Its most prominent feature is script management, |
87 militants alike. Its most prominent feature is script management, |
94 providing a metaphor of <em>live proof script editing</em>. Proof |
88 providing a metaphor of <em>live proof script editing</em>. Proof |
95 General has recently gained a rather large following of both beginning |
89 General has recently gained a rather large following of both beginning |
96 and expert users of Isabelle. |
90 and expert users of Isabelle. |
97 |
91 |
98 <li> |
92 <p> |
99 <a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by |
|
100 David Aspinall is an older and simpler Emacs interface for Isabelle. |
|
101 It runs under recent versions of XEmacs. |
|
102 |
93 |
103 </ul> |
94 Proof~General may be used together with the Emacs |
|
95 <a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/"> |
|
96 X-Symbol package</a>, which provides a nice way to get proper |
|
97 mathematical symbols displayed on screen. |
104 |
98 |
105 |
99 |
106 <h2>Other sources of information</h2> |
100 <h2>Other sources of information</h2> |
107 |
101 |
108 <h3>The Isabelle Page</h3> |
102 <h3>The Isabelle Page</h3> |