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.</p> |
20 changes.</p> |
21 |
21 |
22 <h2>System requirements</h2> |
22 <h2>System requirements</h2> |
23 |
23 |
24 <p>Isabelle requires a real Unix box with sufficient resources, say 64 MB |
24 <p>Isabelle requires a regular Unix platform (e.g. GNU Linux) with the |
25 of free main memory and a decent CPU. Speaking by today's hardware |
25 following additional software:</p> |
26 standards, any moderate Linux box should give a very nice platform for |
|
27 Isabelle.</p> |
|
28 |
|
29 <p>Furthermore, Isabelle needs the following software, which is not part |
|
30 of the distribution:</p> |
|
31 <ul> |
|
32 <li>A full Standard ML Compiler (e.g. Poly/ML).</li> |
|
33 <li>The GNU bash shell (version 1.x or 2.x).</li> |
|
34 <li>Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x |
|
35 is <em>not</em> sufficient).</li> |
|
36 </ul> |
|
37 |
|
38 <p>The following ML system and platform combinations are known to work |
|
39 very well:</p> |
|
40 |
26 |
41 <ul> |
27 <ul> |
42 <li>Poly/ML 4.x on Linux/x86, Solaris/Sparc, and PowerPC platforms.</li> |
28 <li>A full Standard ML Compiler (e.g. Poly/ML 4.1.x, SML/NJ 110.x).</li> |
43 <li>SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).</li> |
29 <li>The GNU bash shell (version 2.x).</li> |
|
30 <li>Perl (version 5.x).</li> |
|
31 <li>XEmacs (version 21.4.x) -- for the ProofGeneral interface.</li> |
|
32 <li>A complete LaTeX installation (e.g. teTeX 1.0) -- for document preparation.</li> |
44 </ul> |
33 </ul> |
45 |
|
46 <p><a href="http://www.polyml.org/">Poly/ML</a>, previously a |
|
47 commercial product, is back in the free world. It is by far the best |
|
48 compiler for running Isabelle, requiring the least memory and offering |
|
49 the highest performance.</p> |
|
50 |
|
51 <p><a href="http://smlnj.sourceforge.net/">SML/NJ</a> needs more |
|
52 store and disk space, but on the other hand supports more platforms. |
|
53 The current official release is 110.</p> |
|
54 |
34 |
55 <h2>Installation</h2> |
35 <h2>Installation</h2> |
56 |
36 |
57 <p>Binary packages are available for Isabelle/HOL and ZF for several |
37 <p>Binary packages are available for Isabelle/HOL and ZF for several |
58 platforms from the Isabelle web page. The system may be easily built |
38 platforms from the Isabelle web page. The system may be easily built |