README.html
author oheimb
Fri Jun 02 20:38:28 2000 +0200 (2000-06-02)
changeset 9028 8a1ec8f05f14
parent 8809 85539b33be03
child 9406 d505b11ce30d
permissions -rw-r--r--
added HOL/Prolog
     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 <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
    48 problems with Linux and HP-UX, though.
    49 </ul>
    50 
    51 <p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a
    52 commercial product, is back in the free world.  It is by far the best
    53 compiler for running Isabelle, requiring the least memory and offering
    54 the highest 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 supports many more platforms.
    59 The current official release is 110.  Basically, we still support the
    60 old 0.93 release, but do not recommend it.
    61 
    62 <p> MLWorks is a commercial ML programming environment developed by <a
    63 href="http://www.harlequin.com/">Harlequin</a> and was unfortunately
    64 withdrawn after that company was taken over.  Isabelle on MLWorks 2.0
    65 works well.  It is about 20% faster than on SML/NJ while using
    66 slightly less memory and disk space.  A few minor features (e.g. ML
    67 top-level pretty printing) are not supported, though.
    68 
    69 
    70 <h2>Installation</h2>
    71 
    72 RPM packages are available for Isabelle/HOL and ZF on the Linux/x86
    73 platform.  The system may be easily built from scratch as well, taking
    74 the traditional tar.gz distribution.  See file <tt>INSTALL</tt> as
    75 distributed with Isabelle for more information.
    76 
    77 Further background information may be found in the <em>Isabelle System
    78 Manual</em>, distributed with the sources (directory <tt>doc</tt>).
    79 
    80 
    81 <h2>User interfaces</h2>
    82 
    83 The distribution includes only a very primitive interface based on
    84 ordinary terminal sessions. Advanced interfaces are available from
    85 other sources:
    86 
    87 <ul>
    88 
    89 <li>
    90 <a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by
    91 David Aspinall and others is a generic Emacs interface for proof
    92 assistants, including Isabelle (both for the classic and Isar
    93 version).  Proof General is suitable for use by pacifists and Emacs
    94 militants alike. Its most prominent feature is script management,
    95 providing a metaphor of <em>live proof script editing</em>.  Proof
    96 General has recently gained a rather large following of both beginning
    97 and expert users of Isabelle.
    98 
    99 <li>
   100 <a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
   101 David Aspinall is an older and simpler Emacs interface for Isabelle.
   102 It runs under recent versions of XEmacs.
   103 
   104 </ul>
   105 
   106 
   107 <h2>Other sources of information</h2>
   108 
   109 <h3>The Isabelle Page</h3>
   110 
   111 The Isabelle home page may be accessed both from Cambridge and Munich:
   112 
   113 <ul>
   114 
   115 <li> <a
   116 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a>
   117 
   118 <li> <a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a>
   119 
   120 </ul>
   121 
   122 
   123 <h3>Mailing list</h3>
   124 
   125 The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
   126 provides a forum for Isabelle users to discuss problems and exchange
   127 information. To join, send a message to <a
   128 href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.
   129 
   130 
   131 <h3>Personal mail</h3>
   132 
   133 <a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br>
   134 Computer Laboratory<br>
   135 University of Cambridge<br>
   136 Pembroke Street<br>
   137 Cambridge CB2 3QG<br>
   138 England<br>
   139 <br>
   140 E-mail: <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A><br>
   141 Phone: +44-223-334600<br>
   142 Fax:   +44-223-334748<br>
   143 
   144 <p>
   145 or
   146 <p>
   147 
   148 <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
   149 Institut fuer Informatik<br>
   150 T. U. Muenchen<br>
   151 D-80290 Muenchen<br>
   152 Germany<br>
   153 <br>
   154 E-mail: <A HREF="mailto:nipkow@in.tum.de">nipkow@in.tum.de</A><br>
   155 Phone: +49-89-289-22690<br>
   156 Fax:   +49-89-289-28183<br>
   157 
   158 <p>
   159 
   160 <hr>
   161 
   162 Please report any problems you encounter.  While we shall try to be
   163 helpful, we can accept no responsibility for the deficiencies of
   164 Isabelle and their consequences.
   165 
   166 <hr>
   167 
   168 </body>
   169 </html>