28 |
28 |
29 |
29 |
30 <h2>Packages</h2> |
30 <h2>Packages</h2> |
31 |
31 |
32 We provide a complete set of packages for Isabelle, Proof General, and |
32 We provide a complete set of packages for Isabelle, Proof General, and |
33 PolyML. The Proof General package contains a development snapshot |
33 PolyML. |
34 that works well with <!-- _GP_ distname -->. We will update it to the |
34 <p> |
35 newest stable version as soon as it is released. |
|
36 |
|
37 While XEmacs-21 is not included here, most operating system |
35 While XEmacs-21 is not included here, most operating system |
38 distributions already provide a suitable package, although not |
36 distributions already provide a suitable package, although not |
39 installed by default. Some of the packages below are platform |
37 installed by default. Some of the packages below are platform |
40 dependent; we include binaries for Linux/x86, Solaris/Sparc, and |
38 dependent; we include binaries for Linux/x86, Solaris/Sparc, and |
41 Darwin/PPC (MacOS X). |
39 Darwin/PPC (MacOS X). |
|
40 <p> |
|
41 Short <a href="#install">installation instructions</a> are near the |
|
42 bottom of this page. For more information, see the file INSTALL in |
|
43 <!-- _GP_ distname -->.tar.gz. |
42 |
44 |
43 <p> |
45 <p> |
44 |
46 |
45 <!-- _GP_ setdowncolor("\"#E0E0E0\"") --> |
47 <!-- _GP_ setdowncolor("\"#E0E0E0\"") --> |
46 <center> |
48 <center> |
51 <!-- _GP_ download(1, "Sources and documentation", distname . ".tar.gz", "../..") --> |
53 <!-- _GP_ download(1, "Sources and documentation", distname . ".tar.gz", "../..") --> |
52 <!-- _GP_ download(1, "Documentation in PDF", distname . "_pdf.tar.gz", "../..") --> |
54 <!-- _GP_ download(1, "Documentation in PDF", distname . "_pdf.tar.gz", "../..") --> |
53 <!-- _GP_ download(1, "Theory library in PDF and HTML", distname . "_library.tar.gz", "../..") --> |
55 <!-- _GP_ download(1, "Theory library in PDF and HTML", distname . "_library.tar.gz", "../..") --> |
54 |
56 |
55 <!-- _GP_ downloadhead("Proof General") --> |
57 <!-- _GP_ downloadhead("Proof General") --> |
56 <!-- _GP_ download(1, "Proof General", "contrib/ProofGeneral.tar.gz", "../..") --> |
58 <!-- _GP_ download(1, "Proof General", "contrib/ProofGeneral-3.5.tar.gz", "../..") --> |
57 |
59 |
58 <!-- _GP_ downloadhead("Poly/ML compiler and runtime system") --> |
60 <!-- _GP_ downloadhead("Poly/ML compiler and runtime system") --> |
59 <!-- _GP_ download(1, "Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") --> |
61 <!-- _GP_ download(1, "Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") --> |
60 <!-- _GP_ download(3, "Poly/ML binary modules", "contrib/polyml_x86-linux.tar.gz", "../..") --> |
62 <!-- _GP_ download(3, "Poly/ML binary modules", "contrib/polyml_x86-linux.tar.gz", "../..") --> |
61 <!-- _GP_ download(0, "", "contrib/polyml_sparc-solaris.tar.gz", "../..") --> |
63 <!-- _GP_ download(0, "", "contrib/polyml_sparc-solaris.tar.gz", "../..") --> |
66 <!-- _GP_ download(0, "", "HOL_sparc-solaris.tar.gz", "../..") --> |
68 <!-- _GP_ download(0, "", "HOL_sparc-solaris.tar.gz", "../..") --> |
67 <!-- _GP_ download(0, "", "HOL_ppc-darwin.tar.gz", "../..") --> |
69 <!-- _GP_ download(0, "", "HOL_ppc-darwin.tar.gz", "../..") --> |
68 <!-- _GP_ download(3, "HOL-Complex", "HOL-Complex_x86-linux.tar.gz", "../..") --> |
70 <!-- _GP_ download(3, "HOL-Complex", "HOL-Complex_x86-linux.tar.gz", "../..") --> |
69 <!-- _GP_ download(0, "", "HOL-Complex_sparc-solaris.tar.gz", "../..") --> |
71 <!-- _GP_ download(0, "", "HOL-Complex_sparc-solaris.tar.gz", "../..") --> |
70 <!-- _GP_ download(0, "", "HOL-Complex_ppc-darwin.tar.gz", "../..") --> |
72 <!-- _GP_ download(0, "", "HOL-Complex_ppc-darwin.tar.gz", "../..") --> |
|
73 <!-- _GP_ download(3, "HOL4", "HOL4_x86-linux.tar.gz", "../..") --> |
|
74 <!-- _GP_ download(0, "", "HOL4_sparc-solaris.tar.gz", "../..") --> |
|
75 <!-- _GP_ download(0, "", "HOL4_ppc-darwin.tar.gz", "../..") --> |
71 <!-- _GP_ download(3, "ZF", "ZF_x86-linux.tar.gz", "../..") --> |
76 <!-- _GP_ download(3, "ZF", "ZF_x86-linux.tar.gz", "../..") --> |
72 <!-- _GP_ download(0, "", "ZF_sparc-solaris.tar.gz", "../..") --> |
77 <!-- _GP_ download(0, "", "ZF_sparc-solaris.tar.gz", "../..") --> |
73 <!-- _GP_ download(0, "", "ZF_ppc-darwin.tar.gz", "../..") --> |
78 <!-- _GP_ download(0, "", "ZF_ppc-darwin.tar.gz", "../..") --> |
|
79 |
|
80 <!-- _GP_ downloadhead("HOL4 proof terms") --> |
|
81 <!-- _GP_ download(1, "HOL4 proof terms", "contrib/HOL4-proofs.tar.gz", "../..") --> |
74 |
82 |
75 </table> |
83 </table> |
76 </center> |
84 </center> |
77 |
85 |
78 <p> |
86 <p> |
79 |
87 |
80 <h2>Installation</h2> |
88 <h2>Installation</h2> |
81 |
89 |
82 In fact, there is no installation required. Users may just unpack all |
90 <a name="install">In</a> fact, there is no installation required. Users may just unpack all |
83 required packages within the same directory. The default settings of |
91 required packages within the same directory. The default settings of |
84 Isabelle should be reasonable for most circumstances. |
92 Isabelle should be reasonable for most circumstances. |
85 |
93 |
86 <p> |
94 <p> |
87 |
95 |