|
10016
|
1 |
%title%
|
|
|
2 |
Isabelle Packages
|
|
|
3 |
|
|
|
4 |
%body%
|
|
|
5 |
|
|
|
6 |
<p>
|
|
|
7 |
|
|
|
8 |
The following source and binary packages of <!-- _GP_ distname -->
|
|
|
9 |
provide everything required for easy installation of the full Isabelle
|
|
|
10 |
working environment on common Unix platforms.
|
|
|
11 |
|
|
|
12 |
<p>
|
|
|
13 |
|
|
|
14 |
A <em>minimal</em> Isabelle installation requires only <tt>bash</tt>
|
|
|
15 |
and <tt>perl</tt> (usually provided by the operating system), and a
|
|
|
16 |
suitable implementation of Standard ML (e.g. Poly/ML as provided
|
|
|
17 |
below).
|
|
|
18 |
|
|
|
19 |
<p>
|
|
|
20 |
|
|
|
21 |
A <em>comfortable</em> Isabelle working environment demands further
|
|
|
22 |
user interface support, as provided by <a
|
|
|
23 |
href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a>
|
|
|
24 |
together with the (optional) <a
|
|
|
25 |
href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">X-Symbol</a>
|
|
10028
|
26 |
package. Both of these should be used with a recent version of <a
|
|
|
27 |
href="http://www.xemacs.org">XEmacs</a> (e.g. version 21.1).
|
|
10016
|
28 |
|
|
|
29 |
<p>
|
|
|
30 |
|
|
|
31 |
Below we offer tuned distributions of Proof General and X-Symbol, such
|
|
|
32 |
that <em>no manual configuration</em> is required when used with
|
|
|
33 |
Isabelle. (In case that the original distributions are used instead,
|
|
|
34 |
refer to their included instructions for installation details.) Note
|
|
|
35 |
that XEmacs-21 is not included here -- most operating system
|
|
|
36 |
distributions already provide suitable packages, although not
|
|
|
37 |
installed by default.
|
|
|
38 |
|
|
|
39 |
<p>
|
|
|
40 |
|
|
|
41 |
|
|
|
42 |
<h2>(1) Linux/x86 systems with RPM</h2>
|
|
|
43 |
|
|
|
44 |
This version of the <!-- _GP_ distname --> distribution is for
|
|
|
45 |
Linux/x86 systems with RPM package management, as used by most Linux
|
|
|
46 |
distributions. Note that <tt>rpm</tt> requires root user access for
|
|
|
47 |
installation.
|
|
|
48 |
|
|
|
49 |
<p>
|
|
|
50 |
|
|
|
51 |
<!-- _GP_ setdowncolor("\"#E0E0E0\"") -->
|
|
|
52 |
<center>
|
|
|
53 |
<table border="0" cellspacing="5" cellpadding="4" width="520">
|
|
|
54 |
<!-- _GP_ download("Poly/ML system", "contrib/polyml.i386.rpm", "../..") -->
|
|
|
55 |
<!-- _GP_ download("Isabelle main system", "isabelle.rpm", "../..") -->
|
|
|
56 |
<!-- _GP_ download("Isabelle/HOL image", "isabelle-HOL.i386.rpm", "../..") -->
|
|
|
57 |
<!-- _GP_ download("Isabelle/HOL-Real image (optional)", "isabelle-HOL-Real.i386.rpm", "../..") -->
|
|
|
58 |
<!-- _GP_ download("Isabelle/ZF image (optional)", "isabelle-ZF.i386.rpm", "../..") -->
|
|
|
59 |
<!-- _GP_ download("Isabelle pdf documentation (optional)", "isabelle-pdfdocs.rpm", "../..") -->
|
|
|
60 |
<!-- _GP_ download("Proof General system (recommended)", "contrib/proofgeneral.rpm", "../..") -->
|
|
|
61 |
<!-- _GP_ download("X-Symbol package (recommended)", "contrib/xsymbol.rpm", "../..") -->
|
|
|
62 |
</table>
|
|
|
63 |
</center>
|
|
|
64 |
|
|
|
65 |
<p>
|
|
|
66 |
|
|
|
67 |
Example installation in <tt>/usr/share</tt> (the default location):
|
|
|
68 |
|
|
|
69 |
<pre>
|
|
10022
|
70 |
rpm -i --force --prefix /usr/share polyml.i386.rpm
|
|
|
71 |
rpm -i --force --prefix /usr/share isabelle.rpm
|
|
|
72 |
rpm -i --force --prefix /usr/share isabelle-HOL.i386.rpm
|
|
|
73 |
rpm -i --force --prefix /usr/share proofgeneral.rpm
|
|
|
74 |
rpm -i --force --prefix /usr/share xsymbol.rpm
|
|
10016
|
75 |
</pre>
|
|
|
76 |
|
|
|
77 |
<p>
|
|
|
78 |
|
|
|
79 |
|
|
|
80 |
<h2>(2) Generic Linux/x86 or Solaris/Sparc systems</h2>
|
|
|
81 |
|
|
|
82 |
The following <!-- _GP_ distname --> distribution works for any
|
|
|
83 |
Linux/x86 or Solaris/Sparc system -- actually only Poly/ML is platform
|
|
|
84 |
dependent. Installation does not rely on package management; it may
|
|
|
85 |
be performed by non-root users as well.
|
|
|
86 |
|
|
|
87 |
<p>
|
|
|
88 |
|
|
|
89 |
<!-- _GP_ setdowncolor("\"#E0E0E0\"") -->
|
|
|
90 |
<center>
|
|
|
91 |
<table border="0" cellspacing="5" cellpadding="4" width="520">
|
|
|
92 |
<!-- _GP_ download("Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") -->
|
|
|
93 |
<!-- _GP_ download("Poly/ML module for Linux/x86", "contrib/polyml_x86-linux.tar.gz", "../..") -->
|
|
|
94 |
<!-- _GP_ download("Poly/ML module for Solaris/Sparc", "contrib/polyml_sparc-solaris.tar.gz", "../..") -->
|
|
|
95 |
<!-- _GP_ download("Isabelle main system", distname . ".tar.gz", "../..") -->
|
|
|
96 |
<!-- _GP_ download("Isabelle pdf documentation (optional)", distname . "_pdf.tar.gz", "../..") --> <!-- _GP_ download("Proof General system (recommended)", "contrib/ProofGeneral.tar.gz", "../..") -->
|
|
|
97 |
<!-- _GP_ download("X-Symbol package (recommended)", "contrib/x-symbol.tar.gz", "../..") -->
|
|
|
98 |
</table>
|
|
|
99 |
</center>
|
|
|
100 |
|
|
|
101 |
<p>
|
|
|
102 |
|
|
|
103 |
Example installation in <tt>/usr/local</tt> for Linux/x86:
|
|
|
104 |
|
|
|
105 |
<pre>
|
|
|
106 |
tar -C /usr/local -x -z -f polyml_base.tar.gz
|
|
|
107 |
tar -C /usr/local -x -z -f polyml_x86-linux.tar.gz
|
|
|
108 |
tar -C /usr/local -x -z -f <!-- _GP_ distname . ".tar.gz"-->
|
|
|
109 |
tar -C /usr/local -x -z -f ProofGeneral.tar.gz
|
|
|
110 |
tar -C /usr/local -x -z -f x-symbol.tar.gz
|
|
|
111 |
|
|
|
112 |
cd <!-- _GP_ "/usr/local/" . distname -->
|
|
|
113 |
./configure
|
|
|
114 |
./build
|
|
|
115 |
./bin/isatool install -p /usr/local/bin
|
|
|
116 |
</pre>
|
|
|
117 |
|
|
|
118 |
<p>
|