|
wenzelm@3259
|
1 |
<html>
|
|
wenzelm@3259
|
2 |
|
|
wenzelm@3259
|
3 |
<!-- $Id$ -->
|
|
wenzelm@3259
|
4 |
|
|
wenzelm@3259
|
5 |
<head>
|
|
wenzelm@3259
|
6 |
<title>The Isabelle System Distribution</title>
|
|
wenzelm@3259
|
7 |
</head>
|
|
wenzelm@3259
|
8 |
|
|
wenzelm@3259
|
9 |
<body>
|
|
wenzelm@3259
|
10 |
|
|
wenzelm@3259
|
11 |
<h1>The Isabelle System Distribution</h1>
|
|
wenzelm@3259
|
12 |
|
|
wenzelm@3259
|
13 |
<h2>Version information</h2>
|
|
wenzelm@3259
|
14 |
|
|
wenzelm@6486
|
15 |
This is the internal repository version of Isabelle. The current line
|
|
wenzelm@9927
|
16 |
of Isabelle99 development introduces many new concepts, while
|
|
wenzelm@9927
|
17 |
attempting to keep incompatibilities over Isabelle98 at a minimum.
|
|
wenzelm@9927
|
18 |
See the <tt>NEWS</tt> file in the distribution for more details.
|
|
wenzelm@3259
|
19 |
|
|
wenzelm@3259
|
20 |
|
|
wenzelm@3259
|
21 |
<h2>System requirements</h2>
|
|
wenzelm@3259
|
22 |
|
|
wenzelm@3259
|
23 |
Isabelle requires a real Unix box with sufficient resources. Fun
|
|
wenzelm@7959
|
24 |
starts at about 32-64 MB of free main memory (somewhat depending on
|
|
wenzelm@9927
|
25 |
the ML system), with several tens of MB disk space and a decent CPU.
|
|
wenzelm@6486
|
26 |
Speaking by today's hardware standards, any moderate Linux box should
|
|
wenzelm@8809
|
27 |
give a very nice platform for Isabelle.
|
|
wenzelm@3259
|
28 |
|
|
wenzelm@3259
|
29 |
<p>
|
|
wenzelm@3259
|
30 |
|
|
wenzelm@6077
|
31 |
Furthermore, Isabelle needs the following software, which is not part
|
|
wenzelm@6077
|
32 |
of the distribution:
|
|
wenzelm@3259
|
33 |
<ul>
|
|
paulson@8385
|
34 |
<li> A full Standard ML Compiler (e.g. Poly/ML).
|
|
wenzelm@3279
|
35 |
<li> The GNU bash shell (version 1.x or 2.x).
|
|
wenzelm@5665
|
36 |
<li> Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
|
|
wenzelm@6077
|
37 |
is <em>not</em> sufficient).
|
|
wenzelm@3259
|
38 |
</ul>
|
|
wenzelm@3259
|
39 |
|
|
wenzelm@3259
|
40 |
<p>
|
|
wenzelm@3259
|
41 |
|
|
wenzelm@3259
|
42 |
The following ML system and platform combinations are known to work
|
|
wenzelm@6077
|
43 |
very well:
|
|
wenzelm@3259
|
44 |
<ul>
|
|
wenzelm@11066
|
45 |
<li> Poly/ML 4.x and 3.x on Linux/x86 and Solaris/Sparc.
|
|
wenzelm@8809
|
46 |
<li> SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
|
|
wenzelm@3259
|
47 |
</ul>
|
|
wenzelm@3259
|
48 |
|
|
wenzelm@8809
|
49 |
<p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a
|
|
wenzelm@8809
|
50 |
commercial product, is back in the free world. It is by far the best
|
|
wenzelm@8809
|
51 |
compiler for running Isabelle, requiring the least memory and offering
|
|
wenzelm@8809
|
52 |
the highest performance.
|
|
wenzelm@3259
|
53 |
|
|
paulson@8385
|
54 |
<p> <a
|
|
wenzelm@4431
|
55 |
href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a>
|
|
wenzelm@8809
|
56 |
needs lots of store and disk space, but supports many more platforms.
|
|
wenzelm@8809
|
57 |
The current official release is 110. Basically, we still support the
|
|
wenzelm@9406
|
58 |
old 0.93 release, but do not recommend to use it under normal
|
|
wenzelm@9406
|
59 |
circumstances.
|
|
wenzelm@3259
|
60 |
|
|
wenzelm@8809
|
61 |
<p> MLWorks is a commercial ML programming environment developed by <a
|
|
wenzelm@8809
|
62 |
href="http://www.harlequin.com/">Harlequin</a> and was unfortunately
|
|
wenzelm@8809
|
63 |
withdrawn after that company was taken over. Isabelle on MLWorks 2.0
|
|
wenzelm@11066
|
64 |
works reasonably well.
|
|
wenzelm@3259
|
65 |
|
|
wenzelm@3259
|
66 |
|
|
wenzelm@3259
|
67 |
<h2>Installation</h2>
|
|
wenzelm@3259
|
68 |
|
|
wenzelm@9927
|
69 |
Binary packages are available for Isabelle/HOL and ZF on the Linux/x86
|
|
wenzelm@8809
|
70 |
platform. The system may be easily built from scratch as well, taking
|
|
wenzelm@9927
|
71 |
the traditional tar.gz source distribution. See file <tt>INSTALL</tt>
|
|
wenzelm@9927
|
72 |
as distributed with Isabelle for more information.
|
|
wenzelm@8809
|
73 |
|
|
wenzelm@6486
|
74 |
Further background information may be found in the <em>Isabelle System
|
|
wenzelm@6486
|
75 |
Manual</em>, distributed with the sources (directory <tt>doc</tt>).
|
|
wenzelm@3259
|
76 |
|
|
wenzelm@3259
|
77 |
|
|
wenzelm@9927
|
78 |
<h2>User interface</h2>
|
|
wenzelm@3306
|
79 |
|
|
wenzelm@9927
|
80 |
The canonical Isabelle user interface is <a
|
|
wenzelm@10079
|
81 |
href="http://www.proofgeneral.org">Proof General</a> by David Aspinall
|
|
wenzelm@10079
|
82 |
and others. It is a generic (X)Emacs interface for proof assistants,
|
|
wenzelm@10079
|
83 |
including Isabelle (both for the classic and Isar version). Proof
|
|
wenzelm@10079
|
84 |
General is suitable for use by pacifists and Emacs militants
|
|
wenzelm@10079
|
85 |
alike. Its most prominent feature is script management, providing a
|
|
wenzelm@10079
|
86 |
metaphor of <em>live proof script editing</em>. Proof General has
|
|
wenzelm@10079
|
87 |
recently gained a rather large following of both beginning and expert
|
|
wenzelm@10079
|
88 |
users of Isabelle.
|
|
wenzelm@8809
|
89 |
|
|
wenzelm@9927
|
90 |
<p>
|
|
wenzelm@3306
|
91 |
|
|
wenzelm@11146
|
92 |
Proof General may be used together with the Emacs
|
|
wenzelm@9927
|
93 |
<a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">
|
|
wenzelm@9927
|
94 |
X-Symbol package</a>, which provides a nice way to get proper
|
|
wenzelm@9927
|
95 |
mathematical symbols displayed on screen.
|
|
wenzelm@8809
|
96 |
|
|
wenzelm@3306
|
97 |
|
|
wenzelm@3259
|
98 |
<h2>Other sources of information</h2>
|
|
wenzelm@3259
|
99 |
|
|
wenzelm@8809
|
100 |
<h3>The Isabelle Page</h3>
|
|
wenzelm@8809
|
101 |
|
|
wenzelm@8809
|
102 |
The Isabelle home page may be accessed both from Cambridge and Munich:
|
|
wenzelm@8809
|
103 |
|
|
wenzelm@8809
|
104 |
<ul>
|
|
wenzelm@8809
|
105 |
|
|
wenzelm@8809
|
106 |
<li> <a
|
|
wenzelm@8809
|
107 |
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a>
|
|
wenzelm@8809
|
108 |
|
|
wenzelm@8809
|
109 |
<li> <a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a>
|
|
wenzelm@8809
|
110 |
|
|
wenzelm@8809
|
111 |
</ul>
|
|
wenzelm@8809
|
112 |
|
|
wenzelm@8809
|
113 |
|
|
wenzelm@3259
|
114 |
<h3>Mailing list</h3>
|
|
wenzelm@3259
|
115 |
|
|
wenzelm@8809
|
116 |
The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
|
|
wenzelm@3259
|
117 |
provides a forum for Isabelle users to discuss problems and exchange
|
|
wenzelm@8809
|
118 |
information. To join, send a message to <a
|
|
wenzelm@8809
|
119 |
href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.
|
|
wenzelm@3259
|
120 |
|
|
wenzelm@3259
|
121 |
|
|
wenzelm@3259
|
122 |
<h3>Personal mail</h3>
|
|
wenzelm@3259
|
123 |
|
|
wenzelm@3259
|
124 |
<a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br>
|
|
wenzelm@3259
|
125 |
Computer Laboratory<br>
|
|
wenzelm@3259
|
126 |
University of Cambridge<br>
|
|
wenzelm@3259
|
127 |
Pembroke Street<br>
|
|
wenzelm@3259
|
128 |
Cambridge CB2 3QG<br>
|
|
wenzelm@3259
|
129 |
England<br>
|
|
wenzelm@3259
|
130 |
<br>
|
|
oheimb@8068
|
131 |
E-mail: <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A><br>
|
|
wenzelm@3259
|
132 |
Phone: +44-223-334600<br>
|
|
wenzelm@3259
|
133 |
Fax: +44-223-334748<br>
|
|
wenzelm@3259
|
134 |
|
|
wenzelm@3259
|
135 |
<p>
|
|
wenzelm@3259
|
136 |
or
|
|
wenzelm@3259
|
137 |
<p>
|
|
wenzelm@3259
|
138 |
|
|
wenzelm@5401
|
139 |
<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
|
|
wenzelm@9927
|
140 |
Institut für Informatik<br>
|
|
wenzelm@9927
|
141 |
T. U. München<br>
|
|
wenzelm@9927
|
142 |
D-80290 München<br>
|
|
wenzelm@3259
|
143 |
Germany<br>
|
|
wenzelm@3259
|
144 |
<br>
|
|
oheimb@8068
|
145 |
E-mail: <A HREF="mailto:nipkow@in.tum.de">nipkow@in.tum.de</A><br>
|
|
wenzelm@3259
|
146 |
Phone: +49-89-289-22690<br>
|
|
wenzelm@3259
|
147 |
Fax: +49-89-289-28183<br>
|
|
wenzelm@3259
|
148 |
|
|
wenzelm@3259
|
149 |
<p>
|
|
wenzelm@3259
|
150 |
|
|
wenzelm@3259
|
151 |
<hr>
|
|
wenzelm@3259
|
152 |
|
|
wenzelm@3259
|
153 |
Please report any problems you encounter. While we shall try to be
|
|
wenzelm@5665
|
154 |
helpful, we can accept no responsibility for the deficiencies of
|
|
wenzelm@3259
|
155 |
Isabelle and their consequences.
|
|
wenzelm@3259
|
156 |
|
|
wenzelm@3259
|
157 |
<hr>
|
|
wenzelm@3259
|
158 |
|
|
wenzelm@3259
|
159 |
</body>
|
|
wenzelm@3259
|
160 |
</html>
|