README.html
author wenzelm
Sun Jul 23 11:58:30 2000 +0200 (2000-07-23)
changeset 9406 d505b11ce30d
parent 8809 85539b33be03
child 9927 7a9652294fe0
permissions -rw-r--r--
tuned;
     1 <html>
     2 
     3 <!-- $Id$ -->
     4 
     5 <head>
     6 <title>The Isabelle System Distribution</title>
     7 </head>
     8 
     9 <body>
    10 
    11 <h1>The Isabelle System Distribution</h1>
    12 
    13 <h2>Version information</h2>
    14 
    15 This is the internal repository version of Isabelle.  The current line
    16 of development introduces many new features, while attempting to keep
    17 incompatibilities over Isabelle98-X at a minimum.  See the
    18 <tt>NEWS</tt> file in the distribution for more details.
    19 
    20 
    21 <h2>System requirements</h2>
    22 
    23 Isabelle requires a real Unix box with sufficient resources. Fun
    24 starts at about 32-64 MB of free main memory (somewhat depending on
    25 your ML system), with several tens of MB disk space and a decent CPU.
    26 Speaking by today's hardware standards, any moderate Linux box should
    27 give a very nice platform for Isabelle.
    28 
    29 <p>
    30 
    31 Furthermore, Isabelle needs the following software, which is not part
    32 of the distribution:
    33 <ul>
    34 <li> A full Standard ML Compiler (e.g. Poly/ML).
    35 <li> The GNU bash shell (version 1.x or 2.x).
    36 <li> Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
    37 is <em>not</em> sufficient).
    38 </ul>
    39 
    40 <p>
    41 
    42 The following ML system and platform combinations are known to work
    43 very well:
    44 <ul>
    45 <li> Poly/ML 3.x on Linux and Sparc/Solaris.
    46 <li> SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
    47 </ul>
    48 
    49 <p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a
    50 commercial product, is back in the free world.  It is by far the best
    51 compiler for running Isabelle, requiring the least memory and offering
    52 the highest performance.
    53 
    54 <p> <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 supports many more platforms.
    57 The current official release is 110.  Basically, we still support the
    58 old 0.93 release, but do not recommend to use it under normal
    59 circumstances.
    60 
    61 <p> MLWorks is a commercial ML programming environment developed by <a
    62 href="http://www.harlequin.com/">Harlequin</a> and was unfortunately
    63 withdrawn after that company was taken over.  Isabelle on MLWorks 2.0
    64 works reasonably well.  It is about 20% faster than on SML/NJ while
    65 using slightly less memory and disk space.  A few features (e.g. ML
    66 top-level pretty printing) are not supported, though.
    67 
    68 
    69 <h2>Installation</h2>
    70 
    71 RPM packages are available for Isabelle/HOL and ZF on the Linux/x86
    72 platform.  The system may be easily built from scratch as well, taking
    73 the traditional tar.gz distribution.  See file <tt>INSTALL</tt> as
    74 distributed with Isabelle for more information.
    75 
    76 Further background information may be found in the <em>Isabelle System
    77 Manual</em>, distributed with the sources (directory <tt>doc</tt>).
    78 
    79 
    80 <h2>User interfaces</h2>
    81 
    82 The distribution includes only a very primitive interface based on
    83 ordinary terminal sessions. Advanced interfaces are available from
    84 other sources:
    85 
    86 <ul>
    87 
    88 <li>
    89 <a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by
    90 David Aspinall and others is a generic Emacs interface for proof
    91 assistants, including Isabelle (both for the classic and Isar
    92 version).  Proof General is suitable for use by pacifists and Emacs
    93 militants alike. Its most prominent feature is script management,
    94 providing a metaphor of <em>live proof script editing</em>.  Proof
    95 General has recently gained a rather large following of both beginning
    96 and expert users of Isabelle.
    97 
    98 <li>
    99 <a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
   100 David Aspinall is an older and simpler Emacs interface for Isabelle.
   101 It runs under recent versions of XEmacs.
   102 
   103 </ul>
   104 
   105 
   106 <h2>Other sources of information</h2>
   107 
   108 <h3>The Isabelle Page</h3>
   109 
   110 The Isabelle home page may be accessed both from Cambridge and Munich:
   111 
   112 <ul>
   113 
   114 <li> <a
   115 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a>
   116 
   117 <li> <a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a>
   118 
   119 </ul>
   120 
   121 
   122 <h3>Mailing list</h3>
   123 
   124 The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
   125 provides a forum for Isabelle users to discuss problems and exchange
   126 information. To join, send a message to <a
   127 href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.
   128 
   129 
   130 <h3>Personal mail</h3>
   131 
   132 <a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br>
   133 Computer Laboratory<br>
   134 University of Cambridge<br>
   135 Pembroke Street<br>
   136 Cambridge CB2 3QG<br>
   137 England<br>
   138 <br>
   139 E-mail: <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A><br>
   140 Phone: +44-223-334600<br>
   141 Fax:   +44-223-334748<br>
   142 
   143 <p>
   144 or
   145 <p>
   146 
   147 <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
   148 Institut fuer Informatik<br>
   149 T. U. Muenchen<br>
   150 D-80290 Muenchen<br>
   151 Germany<br>
   152 <br>
   153 E-mail: <A HREF="mailto:nipkow@in.tum.de">nipkow@in.tum.de</A><br>
   154 Phone: +49-89-289-22690<br>
   155 Fax:   +49-89-289-28183<br>
   156 
   157 <p>
   158 
   159 <hr>
   160 
   161 Please report any problems you encounter.  While we shall try to be
   162 helpful, we can accept no responsibility for the deficiencies of
   163 Isabelle and their consequences.
   164 
   165 <hr>
   166 
   167 </body>
   168 </html>