README.html
author paulson
Mon, 28 Dec 1998 16:56:07 +0100
changeset 6048 88e6e55dd168
parent 5708 fb09ab6a447f
child 6077 60d97d521453
permissions -rw-r--r--
new theorem update_type


<html>

<!-- $Id$ -->

<head>
<title>The Isabelle System Distribution</title>
</head>

<body>

<h1>The Isabelle System Distribution</h1>

<h2>Version information</h2>

This is the internal repository version of Isabelle.  Starting with
Isabelle98, the current line of Isabelle introduces many new features,
but also some incompatibilities with Isabelle94-XX.  See the
<tt>NEWS</tt> file in the distribution for more details.


<h2>System requirements</h2>

Isabelle requires a real Unix box with sufficient resources. Fun
starts at about 32MB of main memory (somewhat depending on your ML
system), with several tens of MB disk space and a relatively fast CPU.

<p>

Furthermore, it needs the following software, which is not part of the
distribution:
<ul>
<li> A full Standard ML Compiler (e.g. SML of New Jersey).
<li> The GNU bash shell (version 1.x or 2.x).
<li> Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
is *not* sufficient).
</ul>

<p>

The following ML system and platform combinations are known to work
quite well:
<ul>
<li> SML/NJ 110.x on any Unix platform (e.g. Suns, Linux).
<li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
problems with Linux and HP-UX, though.
<li> Poly/ML versions 2.x and 3.1 on Suns.
</ul>

<p>

<a
href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a>
needs lots of store and disk space, but it is free.  The current
official release is 110.  We also still support the old 0.93 release.

<p>

<a href="http://www.harlequin.com/products/ads/ml/">MLWorks</a> is a
commercial ML programming environment.  Isabelle on MLWorks 2.0 works well.
It is about 20% faster than on SML/NJ while using slightly less memory and
disk space.  A few minor features (e.g. top-level pretty printing) are not yet
supported, though.

<p>

Poly/ML used to be a commercial product by Abstract Hardware Limited
(now Abstract, Inc.).  It is no longer available.  We're awaiting news
about future availability of Poly/ML.

<p>


<h2>Installation</h2>

See file <tt>INSTALL</tt> in the Isabelle sources on how to build the
system. Further background information may be found in the
<em>Isabelle System Manual</em>, distributed with the sources (see
directory <tt>doc</tt>).


<h2>Interfaces</h2>

The distribution includes only a very primitive interface based on
ordinary terminal sessions.<p>

<a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
David Aspinall is a more elaborate interface for Isabelle.  It runs
under recent versions of XEmacs and is useful to both novices and
experts.


<h2>Other sources of information</h2>

<h3>Mailing list</h3>

The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
provides a forum for Isabelle users to discuss problems and exchange
information. To join, send a message to
<tt>isabelle-users-request@cl.cam.ac.uk</tt>.


<h3>Personal mail</h3>

<a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br>
Computer Laboratory<br>
University of Cambridge<br>
Pembroke Street<br>
Cambridge CB2 3QG<br>
England<br>
<br>
E-mail: lcp@cl.cam.ac.uk<br>
Phone: +44-223-334600<br>
Fax:   +44-223-334748<br>

<p>
or
<p>

<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
Institut fuer Informatik<br>
T. U. Muenchen<br>	
D-80290 Muenchen<br>
Germany<br>
<br>
E-mail: nipkow@www.in.tum.de<br>
Phone: +49-89-289-22690<br>
Fax:   +49-89-289-28183<br>

<p>

<hr>

Please report any problems you encounter.  While we shall try to be
helpful, we can accept no responsibility for the deficiencies of
Isabelle and their consequences.

<hr>

</body>
</html>