30 <p> |
30 <p> |
31 |
31 |
32 Furthermore, Isabelle needs the following software, which is not part |
32 Furthermore, Isabelle needs the following software, which is not part |
33 of the distribution: |
33 of the distribution: |
34 <ul> |
34 <ul> |
35 <li> A full Standard ML Compiler (e.g. SML of New Jersey). |
35 <li> A full Standard ML Compiler (e.g. Poly/ML). |
36 <li> The GNU bash shell (version 1.x or 2.x). |
36 <li> The GNU bash shell (version 1.x or 2.x). |
37 <li> Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x |
37 <li> Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x |
38 is <em>not</em> sufficient). |
38 is <em>not</em> sufficient). |
39 </ul> |
39 </ul> |
40 |
40 |
41 <p> |
41 <p> |
42 |
42 |
43 The following ML system and platform combinations are known to work |
43 The following ML system and platform combinations are known to work |
44 very well: |
44 very well: |
45 <ul> |
45 <ul> |
|
46 <li> Poly/ML 3.x on Linux and Suns. |
46 <li> SML/NJ 110.x on any Unix platform (e.g. Linux, Suns). |
47 <li> SML/NJ 110.x on any Unix platform (e.g. Linux, Suns). |
47 <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several |
48 <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several |
48 problems with Linux and HP-UX, though. |
49 problems with Linux and HP-UX, though. |
49 <li> Poly/ML versions 2.x and 3.1 on Suns. |
|
50 </ul> |
50 </ul> |
51 |
51 |
52 <p> |
52 <p> <A HREF="http://www.polyml.org/">Poly/ML</A>, previously a commercial |
|
53 product, is back in the public domain. It is the best compiler for running |
|
54 Isabelle, requiring the least memory and offering the fastest performance. |
53 |
55 |
54 <a |
56 <p> <a |
55 href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a> |
57 href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a> |
56 needs lots of store and disk space, but it is free. The current |
58 needs lots of store and disk space, but it is free. The current |
57 official release is 110 (there is an <a |
59 official release is 110 (there is an <a |
58 href="ftp://ftp.cl.cam.ac.uk/MIRRORED/smlnj/release/110/smlnj-110.0-3.i386.rpm">RPM |
60 href="ftp://ftp.cl.cam.ac.uk/MIRRORED/smlnj/release/110/smlnj-110.0-3.i386.rpm">RPM |
59 archive</a> available for Linux/x86). We still support the old 0.93 |
61 archive</a> available for Linux/x86). We still support the old 0.93 |
60 release, but do not recommend to use it. |
62 release, but do not recommend it. |
61 |
63 |
62 <p> |
64 <p> MLWorks is a commercial ML programming environment developed by |
|
65 <a href="http://www.harlequin.com/">Harlequin</A> and was |
|
66 unfortunately withdrawn after that company was taken over. Isabelle on |
|
67 MLWorks 2.0 works well. It is about 20% faster than on SML/NJ while using |
|
68 slightly less memory and disk space. A few minor features (e.g. ML top-level |
|
69 pretty printing) are not supported, though. |
63 |
70 |
64 <a href="http://www.harlequin.com/products/ads/ml/">MLWorks</a> is a |
|
65 commercial ML programming environment. Isabelle on MLWorks 2.0 works |
|
66 well. It is about 20% faster than on SML/NJ while using slightly less |
|
67 memory and disk space. A few minor features (e.g. ML top-level pretty |
|
68 printing) are not supported, though. |
|
69 |
|
70 <p> |
|
71 |
|
72 Poly/ML used to be a commercial product by Abstract Hardware Limited |
|
73 (now Abstract, Inc.). It is no longer available. We're awaiting news |
|
74 about future availability of Poly/ML. |
|
75 |
|
76 <p> |
|
77 |
71 |
78 |
72 |
79 <h2>Installation</h2> |
73 <h2>Installation</h2> |
80 |
74 |
81 Binary rpm packages are available for Isabelle/HOL and ZF on the |
75 Binary rpm packages are available for Isabelle/HOL and ZF on the |