29 <p> |
29 <p> |
30 |
30 |
31 Below we offer tuned distributions of Proof General and X-Symbol, such |
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 |
32 that <em>no manual configuration</em> is required when used with |
33 Isabelle. (In case that the original distributions are used instead, |
33 Isabelle. (In case that the original distributions are used instead, |
34 refer to their included instructions for installation details.) Note |
34 refer to their included instructions for the installation details.) |
35 that XEmacs-21 is not included here -- most operating system |
35 Note that XEmacs-21 is not included here -- most operating system |
36 distributions already provide suitable packages, although not |
36 distributions already provide suitable packages, although not |
37 installed by default. |
37 installed by default. |
38 |
38 |
39 <p> |
39 <p> |
40 |
40 |
50 |
50 |
51 <!-- _GP_ setdowncolor("\"#E0E0E0\"") --> |
51 <!-- _GP_ setdowncolor("\"#E0E0E0\"") --> |
52 <center> |
52 <center> |
53 <table border="0" cellspacing="5" cellpadding="4" width="520"> |
53 <table border="0" cellspacing="5" cellpadding="4" width="520"> |
54 <!-- _GP_ download("Poly/ML system", "contrib/polyml.i386.rpm", "../..") --> |
54 <!-- _GP_ download("Poly/ML system", "contrib/polyml.i386.rpm", "../..") --> |
55 <!-- _GP_ download("Isabelle main system", "isabelle.rpm", "../..") --> |
55 <!-- _GP_ download("Isabelle system", "isabelle.rpm", "../..") --> |
56 <!-- _GP_ download("Isabelle/HOL image", "isabelle-HOL.i386.rpm", "../..") --> |
56 <!-- _GP_ download("Isabelle/HOL image", "isabelle-HOL.i386.rpm", "../..") --> |
57 <!-- _GP_ download("Isabelle/HOL-Real image (optional)", "isabelle-HOL-Real.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", "../..") --> |
58 <!-- _GP_ download("Isabelle/ZF image (optional)", "isabelle-ZF.i386.rpm", "../..") --> |
59 <!-- _GP_ download("Isabelle pdf documentation (optional)", "isabelle-pdfdocs.rpm", "../..") --> |
59 <!-- _GP_ download("Isabelle pdf documentation (optional)", "isabelle-pdfdocs.rpm", "../..") --> |
60 <!-- _GP_ download("Proof General system (recommended)", "contrib/proofgeneral.rpm", "../..") --> |
60 <!-- _GP_ download("Proof General (recommended)", "contrib/proofgeneral.rpm", "../..") --> |
61 <!-- _GP_ download("X-Symbol package (recommended)", "contrib/xsymbol.rpm", "../..") --> |
61 <!-- _GP_ download("X-Symbol package (recommended)", "contrib/xsymbol.rpm", "../..") --> |
62 </table> |
62 </table> |
63 </center> |
63 </center> |
64 |
64 |
65 <p> |
65 <p> |
66 |
66 |
67 Example installation in <tt>/usr/share</tt> (the default location): |
67 Example installation procedure (the location of <tt>--prefix |
|
68 /usr/share</tt> may be changed): |
68 |
69 |
69 <pre> |
70 <pre> |
70 rpm -i --prefix /usr/share polyml.i386.rpm |
71 rpm -i --prefix /usr/share polyml.i386.rpm |
71 rpm -i --prefix /usr/share isabelle.rpm |
72 rpm -i --prefix /usr/share isabelle.rpm |
72 rpm -i --prefix /usr/share isabelle-HOL.i386.rpm |
73 rpm -i --prefix /usr/share isabelle-HOL.i386.rpm |
84 |
85 |
85 |
86 |
86 <h2>(2) Generic Linux/x86 or Solaris/Sparc systems</h2> |
87 <h2>(2) Generic Linux/x86 or Solaris/Sparc systems</h2> |
87 |
88 |
88 The following <!-- _GP_ distname --> distribution works for any |
89 The following <!-- _GP_ distname --> distribution works for any |
89 Linux/x86 or Solaris/Sparc system -- actually only Poly/ML is platform |
90 Linux/x86 or Solaris/Sparc system. Installation does not rely on |
90 dependent. Installation does not rely on package management; it may |
91 package management. |
91 be performed by non-root users as well. |
|
92 |
92 |
93 <p> |
93 <p> |
94 |
94 |
95 <!-- _GP_ setdowncolor("\"#E0E0E0\"") --> |
95 <!-- _GP_ setdowncolor("\"#E0E0E0\"") --> |
96 <center> |
96 <center> |
97 <table border="0" cellspacing="5" cellpadding="4" width="520"> |
97 <table border="0" cellspacing="5" cellpadding="4" width="520"> |
98 <!-- _GP_ download("Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") --> |
98 <!-- _GP_ download("Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") --> |
99 <!-- _GP_ download("Poly/ML module for Linux/x86", "contrib/polyml_x86-linux.tar.gz", "../..") --> |
99 <!-- _GP_ download("Poly/ML module for Linux/x86", "contrib/polyml_x86-linux.tar.gz", "../..") --> |
100 <!-- _GP_ download("Poly/ML module for Solaris/Sparc", "contrib/polyml_sparc-solaris.tar.gz", "../..") --> |
100 <!-- _GP_ download("Poly/ML module for Solaris/Sparc", "contrib/polyml_sparc-solaris.tar.gz", "../..") --> |
101 <!-- _GP_ download("Isabelle main system", distname . ".tar.gz", "../..") --> |
101 <!-- _GP_ download("Isabelle system", distname . ".tar.gz", "../..") --> |
102 <!-- _GP_ download("Isabelle pdf documentation (optional)", distname . "_pdf.tar.gz", "../..") --> <!-- _GP_ download("Proof General system (recommended)", "contrib/ProofGeneral.tar.gz", "../..") --> |
102 <!-- _GP_ download("Isabelle pdf documentation (optional)", distname . "_pdf.tar.gz", "../..") --> <!-- _GP_ download("Proof General (recommended)", "contrib/ProofGeneral.tar.gz", "../..") --> |
103 <!-- _GP_ download("X-Symbol package (recommended)", "contrib/x-symbol.tar.gz", "../..") --> |
103 <!-- _GP_ download("X-Symbol package (recommended)", "contrib/x-symbol.tar.gz", "../..") --> |
104 </table> |
104 </table> |
105 </center> |
105 </center> |
106 |
106 |
107 <p> |
107 <p> |