README.html
author wenzelm
Fri Dec 12 18:10:59 1997 +0100 (1997-12-12)
changeset 4401 384108c6e209
parent 4183 706902a9abdd
child 4414 ac5cb6219db7
permissions -rw-r--r--
prepared for Isabelle98;
     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 <strong>Isabelle98</strong> as of January 1998.  Compared to
    17 the Isabelle94 line it introduces many new features, but also some
    18 imcompatibilities.  See the <tt>NEWS</tt> file in the distribution for
    19 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 32MB of memory (somewhat depending on your ML system),
    26 with several tens of MB disk space and a relatively fast CPU.
    27 
    28 <p>
    29 
    30 Furthermore, it needs the following software, which is not part of the
    31 distribution:
    32 <ul>
    33 <li> A full Standard ML Compiler (e.g. Poly/ML or SML of New Jersey).
    34 <li> The GNU bash shell (version 1.x or 2.x).
    35 <li> Perl 5.x - the Pathologically Eclectic Rubbish Lister.
    36 </ul>
    37 
    38 <p>
    39 
    40 The following ML system and platform combinations are known to work
    41 quite well:
    42 <ul>
    43 <li> Poly/ML versions 2.x and 3.1 on Suns.
    44 <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
    45 problems with Linux and HP-UX.
    46 <li> SML/NJ versions 109.27 to 109.33 on Suns, Linux, etc.
    47 <li> SML/NJ 110 on Suns, Linux, etc.
    48 </ul>
    49 
    50 <p>
    51 
    52 <a href="http://www.ahl.co.uk/poly-ml.html">Poly/ML</a> is a
    53 commercial product and costs money, but it is stable and efficient. It
    54 requires relatively little memory (starting at about 16MB) and disk
    55 space (about 40MB for all distributed object logics).
    56 
    57 <p>
    58 
    59 SML/NJ needs lots of store and disk space, but it is <a
    60 href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">free</a>.
    61 The current official release is 110.  We also still support the old
    62 0.93 release and working versions 109.27 to 109.33.  Support for the
    63 109 line of SML/NJ will be dropped next time!  There is an unofficial
    64 pre-built binary distribution of <a
    65 href="http://www4.informatik.tu-muenchen.de/~isabelle/dist/smlnj-110/">SML/NJ
    66 110 for Linux.</a>
    67 
    68 
    69 <h2>Installation</h2>
    70 
    71 See file <tt>INSTALL</tt> in the Isabelle sources on how to build the
    72 system. Further background information may be found in the
    73 <em>Isabelle System Manual</em>, distributed as <tt>dvi</tt> with the
    74 sources.
    75 
    76 
    77 <h2>Interfaces</h2>
    78 
    79 The distribution includes only a very primitive interface based on
    80 ordinary terminal sessions.<p>
    81 
    82 David Aspinall has written a more elaborate <a
    83 href="ftp://ftp.dcs.ed.ac.uk/pub/da/Isamode.tar.gz">user interface</a>
    84 for Isabelle.  It runs under recent versions of GNU Emacs and XEmacs,
    85 the latter being recommended.  It's useful to both novices and
    86 experts.
    87 
    88 
    89 <h2>Other sources of information</h2>
    90 
    91 <h3>Mailing list</h3>
    92 
    93 The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
    94 provides a forum for Isabelle users to discuss problems and exchange
    95 information. To join, send a message to
    96 <tt>isabelle-users-request@cl.cam.ac.uk</tt>.
    97 
    98 
    99 <h3>Personal mail</h3>
   100 
   101 <a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br>
   102 Computer Laboratory<br>
   103 University of Cambridge<br>
   104 Pembroke Street<br>
   105 Cambridge CB2 3QG<br>
   106 England<br>
   107 <br>
   108 E-mail: lcp@cl.cam.ac.uk<br>
   109 Phone: +44-223-334600<br>
   110 Fax:   +44-223-334748<br>
   111 
   112 <p>
   113 or
   114 <p>
   115 
   116 <a href="http://www4.informatik.tu-muenchen.de:80/~nipkow/">Tobias Nipkow</a><br>
   117 Institut fuer Informatik<br>
   118 T. U. Muenchen<br>	
   119 D-80290 Muenchen<br>
   120 Germany<br>
   121 <br>
   122 E-mail: nipkow@informatik.tu-muenchen.de<br>
   123 Phone: +49-89-289-22690<br>
   124 Fax:   +49-89-289-28183<br>
   125 
   126 <p>
   127 
   128 <hr>
   129 
   130 Please report any problems you encounter.  While we shall try to be
   131 helpful, we can accept no responsibility for the deficiences of
   132 Isabelle and their consequences.
   133 
   134 <hr>
   135 
   136 </body>
   137 </html>