1 %title% |
|
2 Isabelle Binary Distribution |
|
3 |
|
4 %body% |
|
5 |
|
6 <p> |
|
7 |
|
8 The binary distribution of <!-- _GP_ distname --> provides everything |
|
9 required for easy installation of the full Isabelle working |
|
10 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> |
|
26 package. Both of these require a recent version of <a |
|
27 href="http://www.xemacs.org">XEmacs</a> (e.g. version 21). |
|
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 --> binary 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> |
|
70 rpm -i --prefix /usr/share polyml.i386.rpm |
|
71 rpm -i --prefix /usr/share isabelle.rpm |
|
72 rpm -i --prefix /usr/share isabelle-HOL.i386.rpm |
|
73 rpm -i --prefix /usr/share proofgeneral.rpm |
|
74 rpm -i --prefix /usr/share xsymbol.rpm |
|
75 </pre> |
|
76 |
|
77 <p> |
|
78 |
|
79 |
|
80 <h2>(2) Generic Linux/x86 or Solaris/Sparc systems</h2> |
|
81 |
|
82 The following <!-- _GP_ distname --> binary 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> |
|
119 |
|
120 <p> |
|