README.html
author paulson
Thu Mar 09 10:35:07 2000 +0100 (2000-03-09)
changeset 8385 514df4f1df10
parent 8068 72d783f7313a
child 8809 85539b33be03
permissions -rw-r--r--
updated discussion of compilers
     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.  The current line
    17 of development introduces many new features, while attempting to keep
    18 incompatibilities over Isabelle98-X at a minimum.  See the
    19 <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 free main memory (somewhat depending on
    26 your ML system), with several tens of MB disk space and a decent CPU.
    27 Speaking by today's hardware standards, any moderate Linux box should
    28 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. Poly/ML).
    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> Poly/ML 3.x on Linux and Suns.
    47 <li> SML/NJ 110.x on any Unix platform (e.g. Linux, Suns).
    48 <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
    49 problems with Linux and HP-UX, though.
    50 </ul>
    51 
    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.
    55 
    56 <p> <a
    57 href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a>
    58 needs lots of store and disk space, but it is free.  The current
    59 official release is 110 (there is an <a
    60 href="ftp://ftp.cl.cam.ac.uk/MIRRORED/smlnj/release/110/smlnj-110.0-3.i386.rpm">RPM
    61 archive</a> available for Linux/x86).  We still support the old 0.93
    62 release, but do not recommend it.
    63 
    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. 
    70 
    71 
    72 
    73 <h2>Installation</h2>
    74 
    75 Binary rpm packages are available for Isabelle/HOL and ZF on the
    76 Linux/x86 platform.  Alternatively, the system may be built from
    77 scratch as described in file <tt>INSTALL</tt> of the Isabelle sources.
    78 Further background information may be found in the <em>Isabelle System
    79 Manual</em>, distributed with the sources (directory <tt>doc</tt>).
    80 
    81 
    82 <h2>User interfaces</h2>
    83 
    84 The distribution includes only a very primitive interface based on
    85 ordinary terminal sessions. Advanced interfaces are available from 
    86 other sources:
    87 
    88 <UL>
    89 <LI>
    90 <a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
    91 David Aspinall is a more elaborate interface for Isabelle.  It runs
    92 under recent versions of XEmacs and is useful to both novices and
    93 experts.
    94 
    95 <LI>
    96 <a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> is
    97 a generic Emacs interface for proof assistants, including Isabelle
    98 (both for the classic and Isar version).  Proof General is suitable
    99 for use by pacifists and Emacs militants alike. Its most prominent
   100 feature is script management, providing a metaphor of <em>live proof
   101 script editing</em>.
   102 </UL>
   103 
   104 <h2>Other sources of information</h2>
   105 
   106 <h3>Mailing list</h3>
   107 
   108 The electronic mailing list <TT>isabelle-users@cl.cam.ac.uk</TT>
   109 provides a forum for Isabelle users to discuss problems and exchange
   110 information. To join, send a message to
   111 <A HREF="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</A>.
   112 
   113 
   114 <h3>Personal mail</h3>
   115 
   116 <a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br>
   117 Computer Laboratory<br>
   118 University of Cambridge<br>
   119 Pembroke Street<br>
   120 Cambridge CB2 3QG<br>
   121 England<br>
   122 <br>
   123 E-mail: <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A><br>
   124 Phone: +44-223-334600<br>
   125 Fax:   +44-223-334748<br>
   126 
   127 <p>
   128 or
   129 <p>
   130 
   131 <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
   132 Institut fuer Informatik<br>
   133 T. U. Muenchen<br>	
   134 D-80290 Muenchen<br>
   135 Germany<br>
   136 <br>
   137 E-mail: <A HREF="mailto:nipkow@in.tum.de">nipkow@in.tum.de</A><br>
   138 Phone: +49-89-289-22690<br>
   139 Fax:   +49-89-289-28183<br>
   140 
   141 <p>
   142 
   143 <hr>
   144 
   145 Please report any problems you encounter.  While we shall try to be
   146 helpful, we can accept no responsibility for the deficiencies of
   147 Isabelle and their consequences.
   148 
   149 <hr>
   150 
   151 </body>
   152 </html>