README.html
author wenzelm
Fri Mar 19 11:24:00 1999 +0100 (1999-03-19)
changeset 6404 2daaf2943c79
parent 6125 59507030d953
child 6486 1f1d5e00e0a5
permissions -rw-r--r--
common qed and end of proofs;
     1 
     2 <html>
     3 
     4 <!-- $Id$ -->
     5 
     6 <head>
     7 <title>The Isabelle System Distribution</title>
     8 </head>
     9 
    10 <body>
    11 
    12 <h1>The Isabelle System Distribution</h1>
    13 
    14 <h2>Version information</h2>
    15 
    16 This is the internal repository version of Isabelle.  Starting with
    17 Isabelle98, the current line of Isabelle development introduces many
    18 new features, but also some incompatibilities with Isabelle94-XX.  See
    19 the <tt>NEWS</tt> file in the distribution for more details.
    20 
    21 
    22 <h2>System requirements</h2>
    23 
    24 Isabelle requires a real Unix box with sufficient resources. Fun
    25 starts at about 32-64 MB of main memory (somewhat depending on your ML
    26 system), with several tens of MB disk space and a decent CPU.
    27 Speaking by today's hardware standards, even a rather low-end Linux
    28 box should make a nice platform for Isabelle.
    29 
    30 <p>
    31 
    32 Furthermore, Isabelle needs the following software, which is not part
    33 of the distribution:
    34 <ul>
    35 <li> A full Standard ML Compiler (e.g. SML of New Jersey).
    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
    38 is <em>not</em> sufficient).
    39 </ul>
    40 
    41 <p>
    42 
    43 The following ML system and platform combinations are known to work
    44 very well:
    45 <ul>
    46 <li> SML/NJ 110.x on any Unix platform (e.g. Suns, Linux).
    47 <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
    48 problems with Linux and HP-UX, though.
    49 <li> Poly/ML versions 2.x and 3.1 on Suns.
    50 </ul>
    51 
    52 <p>
    53 
    54 <a
    55 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
    57 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
    59 archive</a> available for Linux/x86).  We still support the old 0.93
    60 release, but do not recommend to use it.
    61 
    62 <p>
    63 
    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 yet 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 
    78 
    79 <h2>Installation</h2>
    80 
    81 See file <tt>INSTALL</tt> in the Isabelle sources on how to build the
    82 system. Further background information may be found in the
    83 <em>Isabelle System Manual</em>, distributed with the sources (see
    84 directory <tt>doc</tt>).
    85 
    86 
    87 <h2>Interfaces</h2>
    88 
    89 The distribution includes only a very primitive interface based on
    90 ordinary terminal sessions.
    91 
    92 <p>
    93 
    94 <a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
    95 David Aspinall is a more elaborate interface for Isabelle.  It runs
    96 under recent versions of XEmacs and is useful to both novices and
    97 experts.
    98 
    99 <p>
   100 
   101 <a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> is
   102 a generic Emacs interface for proof assistants, including Isabelle (as
   103 of version 2.0).  Proof General is suitable for use by pacifists and
   104 Emacs militants alike. Its most prominent feature is script
   105 management, providing a metaphor of <em>live proof script
   106 editing</em>.
   107 
   108 
   109 <h2>Other sources of information</h2>
   110 
   111 <h3>Mailing list</h3>
   112 
   113 The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
   114 provides a forum for Isabelle users to discuss problems and exchange
   115 information. To join, send a message to
   116 <tt>isabelle-users-request@cl.cam.ac.uk</tt>.
   117 
   118 
   119 <h3>Personal mail</h3>
   120 
   121 <a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br>
   122 Computer Laboratory<br>
   123 University of Cambridge<br>
   124 Pembroke Street<br>
   125 Cambridge CB2 3QG<br>
   126 England<br>
   127 <br>
   128 E-mail: lcp@cl.cam.ac.uk<br>
   129 Phone: +44-223-334600<br>
   130 Fax:   +44-223-334748<br>
   131 
   132 <p>
   133 or
   134 <p>
   135 
   136 <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
   137 Institut fuer Informatik<br>
   138 T. U. Muenchen<br>	
   139 D-80290 Muenchen<br>
   140 Germany<br>
   141 <br>
   142 E-mail: nipkow@www.in.tum.de<br>
   143 Phone: +49-89-289-22690<br>
   144 Fax:   +49-89-289-28183<br>
   145 
   146 <p>
   147 
   148 <hr>
   149 
   150 Please report any problems you encounter.  While we shall try to be
   151 helpful, we can accept no responsibility for the deficiencies of
   152 Isabelle and their consequences.
   153 
   154 <hr>
   155 
   156 </body>
   157 </html>