| author | nipkow |
| Wed, 30 Aug 2000 13:22:10 +0200 | |
| changeset 9737 | 7aae235675dc |
| parent 9406 | d505b11ce30d |
| child 9927 | 7a9652294fe0 |
| permissions | -rw-r--r-- |
| 3259 | 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 |
||
| 6486 | 15 |
This is the internal repository version of Isabelle. The current line |
| 7959 | 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. |
|
| 3259 | 19 |
|
20 |
||
21 |
<h2>System requirements</h2> |
|
22 |
||
23 |
Isabelle requires a real Unix box with sufficient resources. Fun |
|
| 7959 | 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. |
|
| 6486 | 26 |
Speaking by today's hardware standards, any moderate Linux box should |
| 8809 | 27 |
give a very nice platform for Isabelle. |
| 3259 | 28 |
|
29 |
<p> |
|
30 |
||
| 6077 | 31 |
Furthermore, Isabelle needs the following software, which is not part |
32 |
of the distribution: |
|
| 3259 | 33 |
<ul> |
| 8385 | 34 |
<li> A full Standard ML Compiler (e.g. Poly/ML). |
| 3279 | 35 |
<li> The GNU bash shell (version 1.x or 2.x). |
| 5665 | 36 |
<li> Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x |
| 6077 | 37 |
is <em>not</em> sufficient). |
| 3259 | 38 |
</ul> |
39 |
||
40 |
<p> |
|
41 |
||
42 |
The following ML system and platform combinations are known to work |
|
| 6077 | 43 |
very well: |
| 3259 | 44 |
<ul> |
| 8809 | 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.). |
|
| 3259 | 47 |
</ul> |
48 |
||
| 8809 | 49 |
<p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a |
50 |
commercial product, is back in the free world. It is by far the best |
|
51 |
compiler for running Isabelle, requiring the least memory and offering |
|
52 |
the highest performance. |
|
| 3259 | 53 |
|
| 8385 | 54 |
<p> <a |
| 4431 | 55 |
href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a> |
| 8809 | 56 |
needs lots of store and disk space, but supports many more platforms. |
57 |
The current official release is 110. Basically, we still support the |
|
| 9406 | 58 |
old 0.93 release, but do not recommend to use it under normal |
59 |
circumstances. |
|
| 3259 | 60 |
|
| 8809 | 61 |
<p> MLWorks is a commercial ML programming environment developed by <a |
62 |
href="http://www.harlequin.com/">Harlequin</a> and was unfortunately |
|
63 |
withdrawn after that company was taken over. Isabelle on MLWorks 2.0 |
|
| 9406 | 64 |
works reasonably well. It is about 20% faster than on SML/NJ while |
65 |
using slightly less memory and disk space. A few features (e.g. ML |
|
| 8809 | 66 |
top-level pretty printing) are not supported, though. |
| 3259 | 67 |
|
68 |
||
69 |
<h2>Installation</h2> |
|
70 |
||
| 8809 | 71 |
RPM packages are available for Isabelle/HOL and ZF on the Linux/x86 |
72 |
platform. The system may be easily built from scratch as well, taking |
|
73 |
the traditional tar.gz distribution. See file <tt>INSTALL</tt> as |
|
74 |
distributed with Isabelle for more information. |
|
75 |
||
| 6486 | 76 |
Further background information may be found in the <em>Isabelle System |
77 |
Manual</em>, distributed with the sources (directory <tt>doc</tt>). |
|
| 3259 | 78 |
|
79 |
||
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
80 |
<h2>User interfaces</h2> |
| 3306 | 81 |
|
82 |
The distribution includes only a very primitive interface based on |
|
| 8809 | 83 |
ordinary terminal sessions. Advanced interfaces are available from |
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
84 |
other sources: |
| 6077 | 85 |
|
| 8809 | 86 |
<ul> |
| 3306 | 87 |
|
| 8809 | 88 |
<li> |
89 |
<a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by |
|
90 |
David Aspinall and others is a generic Emacs interface for proof |
|
91 |
assistants, including Isabelle (both for the classic and Isar |
|
92 |
version). Proof General is suitable for use by pacifists and Emacs |
|
93 |
militants alike. Its most prominent feature is script management, |
|
94 |
providing a metaphor of <em>live proof script editing</em>. Proof |
|
95 |
General has recently gained a rather large following of both beginning |
|
96 |
and expert users of Isabelle. |
|
97 |
||
98 |
<li> |
|
99 |
<a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by |
|
100 |
David Aspinall is an older and simpler Emacs interface for Isabelle. |
|
101 |
It runs under recent versions of XEmacs. |
|
102 |
||
103 |
</ul> |
|
104 |
||
| 3306 | 105 |
|
| 3259 | 106 |
<h2>Other sources of information</h2> |
107 |
||
| 8809 | 108 |
<h3>The Isabelle Page</h3> |
109 |
||
110 |
The Isabelle home page may be accessed both from Cambridge and Munich: |
|
111 |
||
112 |
<ul> |
|
113 |
||
114 |
<li> <a |
|
115 |
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a> |
|
116 |
||
117 |
<li> <a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a> |
|
118 |
||
119 |
</ul> |
|
120 |
||
121 |
||
| 3259 | 122 |
<h3>Mailing list</h3> |
123 |
||
| 8809 | 124 |
The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt> |
| 3259 | 125 |
provides a forum for Isabelle users to discuss problems and exchange |
| 8809 | 126 |
information. To join, send a message to <a |
127 |
href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>. |
|
| 3259 | 128 |
|
129 |
||
130 |
<h3>Personal mail</h3> |
|
131 |
||
132 |
<a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br> |
|
133 |
Computer Laboratory<br> |
|
134 |
University of Cambridge<br> |
|
135 |
Pembroke Street<br> |
|
136 |
Cambridge CB2 3QG<br> |
|
137 |
England<br> |
|
138 |
<br> |
|
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
139 |
E-mail: <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A><br> |
| 3259 | 140 |
Phone: +44-223-334600<br> |
141 |
Fax: +44-223-334748<br> |
|
142 |
||
143 |
<p> |
|
144 |
or |
|
145 |
<p> |
|
146 |
||
| 5401 | 147 |
<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br> |
| 3259 | 148 |
Institut fuer Informatik<br> |
| 8809 | 149 |
T. U. Muenchen<br> |
| 3259 | 150 |
D-80290 Muenchen<br> |
151 |
Germany<br> |
|
152 |
<br> |
|
|
8068
72d783f7313a
corrected, improved eMail addresses, user interface section
oheimb
parents:
7959
diff
changeset
|
153 |
E-mail: <A HREF="mailto:nipkow@in.tum.de">nipkow@in.tum.de</A><br> |
| 3259 | 154 |
Phone: +49-89-289-22690<br> |
155 |
Fax: +49-89-289-28183<br> |
|
156 |
||
157 |
<p> |
|
158 |
||
159 |
<hr> |
|
160 |
||
161 |
Please report any problems you encounter. While we shall try to be |
|
| 5665 | 162 |
helpful, we can accept no responsibility for the deficiencies of |
| 3259 | 163 |
Isabelle and their consequences. |
164 |
||
165 |
<hr> |
|
166 |
||
167 |
</body> |
|
168 |
</html> |