| author | wenzelm |
| Wed, 05 Jan 2000 11:48:08 +0100 | |
| changeset 8097 | 80a3c30d088b |
| parent 8068 | 72d783f7313a |
| child 8385 | 514df4f1df10 |
| permissions | -rw-r--r-- |
| 3259 | 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 |
||
| 6486 | 16 |
This is the internal repository version of Isabelle. The current line |
| 7959 | 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. |
|
| 3259 | 20 |
|
21 |
||
22 |
<h2>System requirements</h2> |
|
23 |
||
24 |
Isabelle requires a real Unix box with sufficient resources. Fun |
|
| 7959 | 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. |
|
| 6486 | 27 |
Speaking by today's hardware standards, any moderate Linux box should |
28 |
make a nice platform for Isabelle. |
|
| 3259 | 29 |
|
30 |
<p> |
|
31 |
||
| 6077 | 32 |
Furthermore, Isabelle needs the following software, which is not part |
33 |
of the distribution: |
|
| 3259 | 34 |
<ul> |
| 5665 | 35 |
<li> A full Standard ML Compiler (e.g. SML of New Jersey). |
| 3279 | 36 |
<li> The GNU bash shell (version 1.x or 2.x). |
| 5665 | 37 |
<li> Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x |
| 6077 | 38 |
is <em>not</em> sufficient). |
| 3259 | 39 |
</ul> |
40 |
||
41 |
<p> |
|
42 |
||
43 |
The following ML system and platform combinations are known to work |
|
| 6077 | 44 |
very well: |
| 3259 | 45 |
<ul> |
| 6486 | 46 |
<li> SML/NJ 110.x on any Unix platform (e.g. Linux, Suns). |
| 3259 | 47 |
<li> SML/NJ 0.93 on Suns and SGIs. There seem to be several |
| 5665 | 48 |
problems with Linux and HP-UX, though. |
49 |
<li> Poly/ML versions 2.x and 3.1 on Suns. |
|
| 3259 | 50 |
</ul> |
51 |
||
52 |
<p> |
|
53 |
||
| 4431 | 54 |
<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 it is free. The current |
|
| 6077 | 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. |
|
| 3259 | 61 |
|
62 |
<p> |
|
63 |
||
| 4431 | 64 |
<a href="http://www.harlequin.com/products/ads/ml/">MLWorks</a> is a |
| 6077 | 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 |
|
| 6125 | 67 |
memory and disk space. A few minor features (e.g. ML top-level pretty |
| 7959 | 68 |
printing) are not supported, though. |
| 5665 | 69 |
|
70 |
<p> |
|
71 |
||
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. |
|
| 4431 | 75 |
|
76 |
<p> |
|
| 3259 | 77 |
|
78 |
||
79 |
<h2>Installation</h2> |
|
80 |
||
| 6486 | 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>). |
|
| 3259 | 86 |
|
87 |
||
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
88 |
<h2>User interfaces</h2> |
| 3306 | 89 |
|
90 |
The distribution includes only a very primitive interface based on |
|
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
91 |
ordinary terminal sessions. Advanced interfaces are available from |
|
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
92 |
other sources: |
| 6077 | 93 |
|
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
94 |
<UL> |
|
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
95 |
<LI> |
| 5534 | 96 |
<a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by |
| 4481 | 97 |
David Aspinall is a more elaborate interface for Isabelle. It runs |
| 5534 | 98 |
under recent versions of XEmacs and is useful to both novices and |
99 |
experts. |
|
| 3306 | 100 |
|
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
101 |
<LI> |
| 6077 | 102 |
<a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> is |
| 7483 | 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 |
|
107 |
script editing</em>. |
|
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
108 |
</UL> |
| 3306 | 109 |
|
| 3259 | 110 |
<h2>Other sources of information</h2> |
111 |
||
112 |
<h3>Mailing list</h3> |
|
113 |
||
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
114 |
The electronic mailing list <TT>isabelle-users@cl.cam.ac.uk</TT> |
| 3259 | 115 |
provides a forum for Isabelle users to discuss problems and exchange |
116 |
information. To join, send a message to |
|
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
117 |
<A HREF="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</A>. |
| 3259 | 118 |
|
119 |
||
120 |
<h3>Personal mail</h3> |
|
121 |
||
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> |
|
125 |
Pembroke Street<br> |
|
126 |
Cambridge CB2 3QG<br> |
|
127 |
England<br> |
|
128 |
<br> |
|
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
129 |
E-mail: <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A><br> |
| 3259 | 130 |
Phone: +44-223-334600<br> |
131 |
Fax: +44-223-334748<br> |
|
132 |
||
133 |
<p> |
|
134 |
or |
|
135 |
<p> |
|
136 |
||
| 5401 | 137 |
<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br> |
| 3259 | 138 |
Institut fuer Informatik<br> |
139 |
T. U. Muenchen<br> |
|
140 |
D-80290 Muenchen<br> |
|
141 |
Germany<br> |
|
142 |
<br> |
|
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
143 |
E-mail: <A HREF="mailto:nipkow@in.tum.de">nipkow@in.tum.de</A><br> |
| 3259 | 144 |
Phone: +49-89-289-22690<br> |
145 |
Fax: +49-89-289-28183<br> |
|
146 |
||
147 |
<p> |
|
148 |
||
149 |
<hr> |
|
150 |
||
151 |
Please report any problems you encounter. While we shall try to be |
|
| 5665 | 152 |
helpful, we can accept no responsibility for the deficiencies of |
| 3259 | 153 |
Isabelle and their consequences. |
154 |
||
155 |
<hr> |
|
156 |
||
157 |
</body> |
|
158 |
</html> |