updated discussion of compilers
authorpaulson
Thu Mar 09 10:35:07 2000 +0100 (2000-03-09)
changeset 8385514df4f1df10
parent 8384 13bc74731ae6
child 8386 3e56677d3b98
updated discussion of compilers
README.html
     1.1 --- a/README.html	Wed Mar 08 23:49:30 2000 +0100
     1.2 +++ b/README.html	Thu Mar 09 10:35:07 2000 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  Furthermore, Isabelle needs the following software, which is not part
     1.5  of the distribution:
     1.6  <ul>
     1.7 -<li> A full Standard ML Compiler (e.g. SML of New Jersey).
     1.8 +<li> A full Standard ML Compiler (e.g. Poly/ML).
     1.9  <li> The GNU bash shell (version 1.x or 2.x).
    1.10  <li> Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
    1.11  is <em>not</em> sufficient).
    1.12 @@ -43,37 +43,31 @@
    1.13  The following ML system and platform combinations are known to work
    1.14  very well:
    1.15  <ul>
    1.16 +<li> Poly/ML 3.x on Linux and Suns.
    1.17  <li> SML/NJ 110.x on any Unix platform (e.g. Linux, Suns).
    1.18  <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
    1.19  problems with Linux and HP-UX, though.
    1.20 -<li> Poly/ML versions 2.x and 3.1 on Suns.
    1.21  </ul>
    1.22  
    1.23 -<p>
    1.24 +<p> <A HREF="http://www.polyml.org/">Poly/ML</A>, previously a commercial
    1.25 +product, is back in the public domain.  It is the best compiler for running
    1.26 +Isabelle, requiring the least memory and offering the fastest performance.
    1.27  
    1.28 -<a
    1.29 +<p> <a
    1.30  href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a>
    1.31  needs lots of store and disk space, but it is free.  The current
    1.32  official release is 110 (there is an <a
    1.33  href="ftp://ftp.cl.cam.ac.uk/MIRRORED/smlnj/release/110/smlnj-110.0-3.i386.rpm">RPM
    1.34  archive</a> available for Linux/x86).  We still support the old 0.93
    1.35 -release, but do not recommend to use it.
    1.36 -
    1.37 -<p>
    1.38 +release, but do not recommend it.
    1.39  
    1.40 -<a href="http://www.harlequin.com/products/ads/ml/">MLWorks</a> is a
    1.41 -commercial ML programming environment.  Isabelle on MLWorks 2.0 works
    1.42 -well.  It is about 20% faster than on SML/NJ while using slightly less
    1.43 -memory and disk space.  A few minor features (e.g. ML top-level pretty
    1.44 -printing) are not supported, though.
    1.45 +<p> MLWorks is a commercial ML programming environment developed by 
    1.46 +<a href="http://www.harlequin.com/">Harlequin</A> and was
    1.47 +unfortunately withdrawn after that company was taken over.  Isabelle on
    1.48 +MLWorks 2.0 works well.  It is about 20% faster than on SML/NJ while using
    1.49 +slightly less memory and disk space.  A few minor features (e.g. ML top-level
    1.50 +pretty printing) are not supported, though. 
    1.51  
    1.52 -<p>
    1.53 -
    1.54 -Poly/ML used to be a commercial product by Abstract Hardware Limited
    1.55 -(now Abstract, Inc.).  It is no longer available.  We're awaiting news
    1.56 -about future availability of Poly/ML.
    1.57 -
    1.58 -<p>
    1.59  
    1.60  
    1.61  <h2>Installation</h2>