| author | schirmer |
| Thu, 31 Oct 2002 18:27:10 +0100 | |
| changeset 13688 | a0b16d42d489 |
| parent 13141 | f4ed10eaaff8 |
| child 14007 | 8c2b9750628f |
| 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 |
||
| 11575 | 15 |
This is the internal repository version of Isabelle. See the |
16 |
<tt>NEWS</tt> file in the distribution for details on user-relevant |
|
17 |
changes. |
|
| 3259 | 18 |
|
19 |
||
20 |
<h2>System requirements</h2> |
|
21 |
||
| 11575 | 22 |
Isabelle requires a real Unix box with sufficient resources, say 64 MB |
23 |
of free main memory and a decent CPU. Speaking by today's hardware |
|
24 |
standards, any moderate Linux box should give a very nice platform for |
|
25 |
Isabelle. |
|
| 3259 | 26 |
|
27 |
<p> |
|
28 |
||
| 6077 | 29 |
Furthermore, Isabelle needs the following software, which is not part |
30 |
of the distribution: |
|
| 3259 | 31 |
<ul> |
| 13016 | 32 |
<li>A full Standard ML Compiler (e.g. Poly/ML). |
33 |
<li>The GNU bash shell (version 1.x or 2.x). |
|
34 |
<li>Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x |
|
| 6077 | 35 |
is <em>not</em> sufficient). |
| 3259 | 36 |
</ul> |
37 |
||
38 |
<p> |
|
39 |
||
40 |
The following ML system and platform combinations are known to work |
|
| 6077 | 41 |
very well: |
| 3259 | 42 |
<ul> |
| 13016 | 43 |
<li>Poly/ML 4.x and 3.x on Linux/x86, Solaris/Sparc, and PowerPC platforms. |
44 |
<li>SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.). |
|
| 3259 | 45 |
</ul> |
46 |
||
| 8809 | 47 |
<p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a |
48 |
commercial product, is back in the free world. It is by far the best |
|
49 |
compiler for running Isabelle, requiring the least memory and offering |
|
50 |
the highest performance. |
|
| 3259 | 51 |
|
| 8385 | 52 |
<p> <a |
| 4431 | 53 |
href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a> |
| 8809 | 54 |
needs lots of store and disk space, but supports many more platforms. |
55 |
The current official release is 110. Basically, we still support the |
|
| 9406 | 56 |
old 0.93 release, but do not recommend to use it under normal |
57 |
circumstances. |
|
| 3259 | 58 |
|
| 11575 | 59 |
<p> MLWorks used to be a commercial ML programming environment |
60 |
developed by <a href="http://www.harlequin.com/">Harlequin</a> and was |
|
61 |
unfortunately withdrawn after that company was taken over. Isabelle |
|
62 |
on MLWorks 2.0 works reasonably well. |
|
| 3259 | 63 |
|
64 |
||
65 |
<h2>Installation</h2> |
|
66 |
||
| 9927 | 67 |
Binary packages are available for Isabelle/HOL and ZF on the Linux/x86 |
| 8809 | 68 |
platform. The system may be easily built from scratch as well, taking |
| 9927 | 69 |
the traditional tar.gz source distribution. See file <tt>INSTALL</tt> |
70 |
as distributed with Isabelle for more information. |
|
| 8809 | 71 |
|
| 6486 | 72 |
Further background information may be found in the <em>Isabelle System |
73 |
Manual</em>, distributed with the sources (directory <tt>doc</tt>). |
|
| 3259 | 74 |
|
75 |
||
| 9927 | 76 |
<h2>User interface</h2> |
| 6077 | 77 |
|
| 9927 | 78 |
The canonical Isabelle user interface is <a |
| 10079 | 79 |
href="http://www.proofgeneral.org">Proof General</a> by David Aspinall |
80 |
and others. It is a generic (X)Emacs interface for proof assistants, |
|
81 |
including Isabelle (both for the classic and Isar version). Proof |
|
82 |
General is suitable for use by pacifists and Emacs militants |
|
83 |
alike. Its most prominent feature is script management, providing a |
|
84 |
metaphor of <em>live proof script editing</em>. Proof General has |
|
85 |
recently gained a rather large following of both beginning and expert |
|
86 |
users of Isabelle. |
|
| 8809 | 87 |
|
| 9927 | 88 |
<p> |
| 8809 | 89 |
|
| 11146 | 90 |
Proof General may be used together with the Emacs |
| 13141 | 91 |
<a href="http://x-symbol.sourceforge.net"> |
| 9927 | 92 |
X-Symbol package</a>, which provides a nice way to get proper |
93 |
mathematical symbols displayed on screen. |
|
| 8809 | 94 |
|
| 3306 | 95 |
|
| 3259 | 96 |
<h2>Other sources of information</h2> |
97 |
||
| 8809 | 98 |
<h3>The Isabelle Page</h3> |
99 |
||
100 |
The Isabelle home page may be accessed both from Cambridge and Munich: |
|
101 |
||
102 |
<ul> |
|
103 |
||
| 13016 | 104 |
<li><a |
| 8809 | 105 |
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a> |
106 |
||
| 13016 | 107 |
<li><a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a> |
| 8809 | 108 |
|
109 |
</ul> |
|
110 |
||
111 |
||
| 3259 | 112 |
<h3>Mailing list</h3> |
113 |
||
| 8809 | 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 |
| 8809 | 116 |
information. To join, send a message to <a |
117 |
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> |
| 9927 | 138 |
Institut für Informatik<br> |
139 |
T. U. München<br> |
|
140 |
D-80290 München<br> |
|
| 3259 | 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> |