|
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 |
|
|
|
16 |
This is <strong>Isabelle-94 revision 8</strong> as of May
|
|
|
17 |
1997. Basically, it should be backwards compatible to earlier
|
|
|
18 |
Isabelle-94 releases. Older versions (like Isabelle-93) are quite
|
|
|
19 |
different, though. See also the <tt>NEWS</tt> file in the distribution
|
|
|
20 |
for a more detailed list of new features and changes.
|
|
|
21 |
|
|
|
22 |
|
|
|
23 |
<h2>System requirements</h2>
|
|
|
24 |
|
|
|
25 |
Isabelle requires a real Unix box with sufficient resources. Fun
|
|
3274
|
26 |
starts at about 32MB of memory (somewhat depending on your ML system),
|
|
3259
|
27 |
several tens of MB disk space and with a relatively fast CPU.
|
|
|
28 |
|
|
|
29 |
<p>
|
|
|
30 |
|
|
|
31 |
Furthermore, it needs the following software, which is not part of the
|
|
|
32 |
distribution:
|
|
|
33 |
<ul>
|
|
|
34 |
<li> A full Standard ML Compiler (e.g. Poly/ML or SML of New Jersey).
|
|
3279
|
35 |
<li> The GNU bash shell (version 1.x or 2.x).
|
|
3259
|
36 |
<li> Perl 5.x - the Pathologically Eclectic Rubbish Lister.
|
|
|
37 |
</ul>
|
|
|
38 |
|
|
|
39 |
The ML system and GNU bash are absolutely essential. Perl is optional
|
|
|
40 |
for core functionality, but still highly recommended.
|
|
|
41 |
|
|
|
42 |
<p>
|
|
|
43 |
|
|
|
44 |
The following ML system and platform combinations are known to work
|
|
|
45 |
quite well:
|
|
|
46 |
<ul>
|
|
3279
|
47 |
<li> Poly/ML versions 2.x and 3.1 on Suns.
|
|
3259
|
48 |
<li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
|
|
|
49 |
problems with Linux and HP-UX.
|
|
|
50 |
<li> SML/NJ 1.07 on Suns, Linux, etc.
|
|
3360
|
51 |
<li> SML/NJ 1.09.27 and 1.09.28 on Suns, Linux, etc.
|
|
3259
|
52 |
</ul>
|
|
|
53 |
|
|
|
54 |
<p>
|
|
|
55 |
|
|
3274
|
56 |
<a href="http://www.ahl.co.uk/poly-ml.html">Poly/ML</a> is a
|
|
|
57 |
commercial product and costs money, but it is stable and efficient. It
|
|
|
58 |
requires relatively little memory (starting at about 16MB) and disk
|
|
|
59 |
space (about 40MB for all distributed object logics).
|
|
3259
|
60 |
|
|
|
61 |
<p>
|
|
|
62 |
|
|
3274
|
63 |
SML/NJ needs lots of store and disk space, but it is <a
|
|
|
64 |
href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">free</a>.
|
|
|
65 |
The last official release is 0.93. Recent working versions may be
|
|
|
66 |
better suited, under normal circumstances. Beware of the many
|
|
|
67 |
incompatibilities among SML/NJ versions! From the 1.09.x family, we
|
|
|
68 |
now only support 1.09.27, or later. An unofficial pre-built binary
|
|
3360
|
69 |
distribution of at least SML/NJ 1.09.27 for Linux is also <a
|
|
3274
|
70 |
href="http://www4.informatik.tu-muenchen.de/~wenzelm/resources.html">available.</a>
|
|
3360
|
71 |
If you have to re-build SML/NJ 1.09.x yourself from the sources, just
|
|
|
72 |
comment out all targets except "sml" (cf. the installation
|
|
|
73 |
instructions of the SML/NJ distribution).
|
|
3259
|
74 |
|
|
|
75 |
|
|
|
76 |
<h2>Installation</h2>
|
|
|
77 |
|
|
|
78 |
See file <tt>INSTALL</tt> in the Isabelle sources on how to build the
|
|
|
79 |
system. Further background information may be found in the
|
|
|
80 |
<em>Isabelle System Manual</em>, distributed as <tt>dvi</tt> with the
|
|
|
81 |
sources.
|
|
|
82 |
|
|
|
83 |
|
|
3306
|
84 |
<h2>Interfaces</h2>
|
|
|
85 |
|
|
|
86 |
The distribution includes only a very primitive interface based on
|
|
|
87 |
ordinary terminal sessions.<p>
|
|
|
88 |
|
|
3322
|
89 |
David Aspinall has written a more elaborate <a
|
|
3306
|
90 |
href="ftp://ftp.dcs.ed.ac.uk/pub/da/Isamode.tar.gz">user interface</a>
|
|
3322
|
91 |
for Isabelle. It runs under recent versions of GNU Emacs and XEmacs,
|
|
|
92 |
the latter being recommended. It's useful to both novices and
|
|
|
93 |
experts.
|
|
3306
|
94 |
|
|
|
95 |
|
|
3259
|
96 |
<h2>Other sources of information</h2>
|
|
|
97 |
|
|
|
98 |
<h3>Mailing list</h3>
|
|
|
99 |
|
|
|
100 |
The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
|
|
|
101 |
provides a forum for Isabelle users to discuss problems and exchange
|
|
|
102 |
information. To join, send a message to
|
|
|
103 |
<tt>isabelle-users-request@cl.cam.ac.uk</tt>.
|
|
|
104 |
|
|
|
105 |
|
|
|
106 |
<h3>Personal mail</h3>
|
|
|
107 |
|
|
|
108 |
<a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br>
|
|
|
109 |
Computer Laboratory<br>
|
|
|
110 |
University of Cambridge<br>
|
|
|
111 |
Pembroke Street<br>
|
|
|
112 |
Cambridge CB2 3QG<br>
|
|
|
113 |
England<br>
|
|
|
114 |
<br>
|
|
|
115 |
E-mail: lcp@cl.cam.ac.uk<br>
|
|
|
116 |
Phone: +44-223-334600<br>
|
|
|
117 |
Fax: +44-223-334748<br>
|
|
|
118 |
|
|
|
119 |
<p>
|
|
|
120 |
or
|
|
|
121 |
<p>
|
|
|
122 |
|
|
|
123 |
<a href="http://www4.informatik.tu-muenchen.de:80/~nipkow/">Tobias Nipkow</a><br>
|
|
|
124 |
Institut fuer Informatik<br>
|
|
|
125 |
T. U. Muenchen<br>
|
|
|
126 |
D-80290 Muenchen<br>
|
|
|
127 |
Germany<br>
|
|
|
128 |
<br>
|
|
|
129 |
E-mail: nipkow@informatik.tu-muenchen.de<br>
|
|
|
130 |
Phone: +49-89-289-22690<br>
|
|
|
131 |
Fax: +49-89-289-28183<br>
|
|
|
132 |
|
|
|
133 |
<p>
|
|
|
134 |
|
|
|
135 |
<hr>
|
|
|
136 |
|
|
|
137 |
Please report any problems you encounter. While we shall try to be
|
|
|
138 |
helpful, we can accept no responsibility for the deficiences of
|
|
|
139 |
Isabelle and their consequences.
|
|
|
140 |
|
|
|
141 |
<hr>
|
|
|
142 |
|
|
|
143 |
</body>
|
|
|
144 |
</html>
|