7 <title>The Isabelle System Distribution</title>
12 <h1>The Isabelle System Distribution</h1>
14 <h2>Version information</h2>
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.
22 <h2>System requirements</h2>
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.
32 Furthermore, Isabelle needs the following software, which is not part
35 <li> A full Standard ML Compiler (e.g. SML of New Jersey).
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).
43 The following ML system and platform combinations are known to work
46 <li> SML/NJ 110.x on any Unix platform (e.g. Linux, Suns).
47 <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
48 problems with Linux and HP-UX, though.
49 <li> Poly/ML versions 2.x and 3.1 on Suns.
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 it is free. The current
57 official release is 110 (there is an <a
58 href="ftp://ftp.cl.cam.ac.uk/MIRRORED/smlnj/release/110/smlnj-110.0-3.i386.rpm">RPM
59 archive</a> available for Linux/x86). We still support the old 0.93
60 release, but do not recommend to use it.
64 <a href="http://www.harlequin.com/products/ads/ml/">MLWorks</a> is a
65 commercial ML programming environment. Isabelle on MLWorks 2.0 works
66 well. It is about 20% faster than on SML/NJ while using slightly less
67 memory and disk space. A few minor features (e.g. ML top-level pretty
68 printing) are not supported, though.
72 Poly/ML used to be a commercial product by Abstract Hardware Limited
73 (now Abstract, Inc.). It is no longer available. We're awaiting news
74 about future availability of Poly/ML.
81 Binary rpm packages are available for Isabelle/HOL and ZF on the
82 Linux/x86 platform. Alternatively, the system may be built from
83 scratch as described in file <tt>INSTALL</tt> of the Isabelle sources.
84 Further background information may be found in the <em>Isabelle System
85 Manual</em>, distributed with the sources (directory <tt>doc</tt>).
88 <h2>Unser interfaces</h2>
90 The distribution includes only a very primitive interface based on
91 ordinary terminal sessions.
95 <a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
96 David Aspinall is a more elaborate interface for Isabelle. It runs
97 under recent versions of XEmacs and is useful to both novices and
102 <a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> is
103 a generic Emacs interface for proof assistants, including Isabelle
104 (both for the classic and Isar version). Proof General is suitable
105 for use by pacifists and Emacs militants alike. Its most prominent
106 feature is script management, providing a metaphor of <em>live proof
110 <h2>Other sources of information</h2>
112 <h3>Mailing list</h3>
114 The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
115 provides a forum for Isabelle users to discuss problems and exchange
116 information. To join, send a message to
117 <tt>isabelle-users-request@cl.cam.ac.uk</tt>.
120 <h3>Personal mail</h3>
122 <a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br>
123 Computer Laboratory<br>
124 University of Cambridge<br>
126 Cambridge CB2 3QG<br>
129 E-mail: lcp@cl.cam.ac.uk<br>
130 Phone: +44-223-334600<br>
131 Fax: +44-223-334748<br>
137 <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
138 Institut fuer Informatik<br>
143 E-mail: nipkow@www.in.tum.de<br>
144 Phone: +49-89-289-22690<br>
145 Fax: +49-89-289-28183<br>
151 Please report any problems you encounter. While we shall try to be
152 helpful, we can accept no responsibility for the deficiencies of
153 Isabelle and their consequences.