13 |
13 |
14 <h1>The Isabelle System Distribution</h1> |
14 <h1>The Isabelle System Distribution</h1> |
15 |
15 |
16 <h2>Version information</h2> |
16 <h2>Version information</h2> |
17 |
17 |
18 This is the internal repository version of Isabelle. See the |
18 <p>This is the internal repository version of Isabelle. See the |
19 <tt>NEWS</tt> file in the distribution for details on user-relevant |
19 <tt>NEWS</tt> file in the distribution for details on user-relevant |
20 changes. |
20 changes.</p> |
21 |
|
22 |
21 |
23 <h2>System requirements</h2> |
22 <h2>System requirements</h2> |
24 |
23 |
25 Isabelle requires a real Unix box with sufficient resources, say 64 MB |
24 <p>Isabelle requires a real Unix box with sufficient resources, say 64 MB |
26 of free main memory and a decent CPU. Speaking by today's hardware |
25 of free main memory and a decent CPU. Speaking by today's hardware |
27 standards, any moderate Linux box should give a very nice platform for |
26 standards, any moderate Linux box should give a very nice platform for |
28 Isabelle. |
27 Isabelle.</p> |
29 |
28 |
30 <p> |
29 <p>Furthermore, Isabelle needs the following software, which is not part |
31 |
30 of the distribution:</p> |
32 Furthermore, Isabelle needs the following software, which is not part |
|
33 of the distribution: |
|
34 <ul> |
31 <ul> |
35 <li>A full Standard ML Compiler (e.g. Poly/ML). |
32 <li>A full Standard ML Compiler (e.g. Poly/ML).</li> |
36 <li>The GNU bash shell (version 1.x or 2.x). |
33 <li>The GNU bash shell (version 1.x or 2.x).</li> |
37 <li>Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x |
34 <li>Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x |
38 is <em>not</em> sufficient). |
35 is <em>not</em> sufficient).</li> |
39 </ul> |
36 </ul> |
40 |
37 |
41 <p> |
38 <p>The following ML system and platform combinations are known to work |
|
39 very well:</p> |
42 |
40 |
43 The following ML system and platform combinations are known to work |
|
44 very well: |
|
45 <ul> |
41 <ul> |
46 <li>Poly/ML 4.x on Linux/x86, Solaris/Sparc, and PowerPC platforms. |
42 <li>Poly/ML 4.x on Linux/x86, Solaris/Sparc, and PowerPC platforms.</li> |
47 <li>SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.). |
43 <li>SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).</li> |
48 </ul> |
44 </ul> |
49 |
45 |
50 <p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a |
46 <p><a href="http://www.polyml.org/">Poly/ML</a>, previously a |
51 commercial product, is back in the free world. It is by far the best |
47 commercial product, is back in the free world. It is by far the best |
52 compiler for running Isabelle, requiring the least memory and offering |
48 compiler for running Isabelle, requiring the least memory and offering |
53 the highest performance. |
49 the highest performance.</p> |
54 |
50 |
55 <p> <a href="http://smlnj.sourceforge.net/">SML/NJ</a> needs more |
51 <p><a href="http://smlnj.sourceforge.net/">SML/NJ</a> needs more |
56 store and disk space, but on the other hand supports more platforms. |
52 store and disk space, but on the other hand supports more platforms. |
57 The current official release is 110. |
53 The current official release is 110.</p> |
58 |
|
59 |
54 |
60 <h2>Installation</h2> |
55 <h2>Installation</h2> |
61 |
56 |
62 Binary packages are available for Isabelle/HOL and ZF for several |
57 <p>Binary packages are available for Isabelle/HOL and ZF for several |
63 platforms from the Isabelle web page. The system may be easily built |
58 platforms from the Isabelle web page. The system may be easily built |
64 from scratch as well, taking the traditional tar.gz source |
59 from scratch as well, taking the traditional tar.gz source |
65 distribution. See file <tt>INSTALL</tt> as distributed with Isabelle |
60 distribution. See file <tt>INSTALL</tt> as distributed with Isabelle |
66 for more information. |
61 for more information.</p> |
67 |
62 |
68 Further background information may be found in the <em>Isabelle System |
63 <p>Further background information may be found in the <em>Isabelle System |
69 Manual</em>, distributed with the sources (directory <tt>doc</tt>). |
64 Manual</em>, distributed with the sources (directory <tt>doc</tt>).</p> |
70 |
|
71 |
65 |
72 <h2>User interface</h2> |
66 <h2>User interface</h2> |
73 |
67 |
74 The canonical Isabelle user interface is <a |
68 <p>The canonical Isabelle user interface is <a |
75 href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by David Aspinall |
69 href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by David Aspinall |
76 and others. It is a generic (X)Emacs interface for proof assistants, |
70 and others. It is a generic (X)Emacs interface for proof assistants, |
77 including Isabelle (both for the classic and Isar version). Proof |
71 including Isabelle (both for the classic and Isar version). Proof |
78 General is suitable for use by pacifists and Emacs militants |
72 General is suitable for use by pacifists and Emacs militants |
79 alike. Its most prominent feature is script management, providing a |
73 alike. Its most prominent feature is script management, providing a |
80 metaphor of <em>live proof script editing</em>. Proof General has |
74 metaphor of <em>live proof script editing</em>. Proof General has |
81 recently gained a rather large following of both beginning and expert |
75 recently gained a rather large following of both beginning and expert |
82 users of Isabelle. |
76 users of Isabelle.</p> |
83 |
77 |
84 <p> |
78 <p>Proof General is distributed together with the XEmacs |
85 |
|
86 Proof General is distributed together with the XEmacs |
|
87 <a href="http://x-symbol.sourceforge.net"> |
79 <a href="http://x-symbol.sourceforge.net"> |
88 X-Symbol package</a>, which provides a nice way to get proper |
80 X-Symbol package</a>, which provides a nice way to get proper |
89 mathematical symbols displayed on screen. |
81 mathematical symbols displayed on screen.</p> |
90 |
|
91 |
82 |
92 <h2>Other sources of information</h2> |
83 <h2>Other sources of information</h2> |
93 |
84 |
94 <h3>The Isabelle Page</h3> |
85 <h3>The Isabelle Page</h3> |
95 |
86 |
96 The Isabelle home page may be accessed both from Cambridge and Munich: |
87 <p>The Isabelle home page may be accessed both from Cambridge and Munich:</p> |
97 |
88 |
98 <ul> |
89 <ul> |
99 |
90 <li><a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a></li> |
100 <li><a |
91 <li><a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a></li> |
101 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a> |
|
102 |
|
103 <li><a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a> |
|
104 |
|
105 </ul> |
92 </ul> |
106 |
93 |
107 |
94 |
108 <h3>Mailing list</h3> |
95 <h3>Mailing list</h3> |
109 |
96 |
110 The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt> |
97 <p>The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt> |
111 provides a forum for Isabelle users to discuss problems and exchange |
98 provides a forum for Isabelle users to discuss problems and exchange |
112 information. To join, send a message to <a |
99 information. To join, send a message to <a |
113 href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>. |
100 href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.</p> |
114 |
101 |
115 |
102 |
116 <h3>Personal mail</h3> |
103 <h3>Personal mail</h3> |
117 |
104 |
118 <a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br> |
105 <a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br> |