author | kleing |
Tue, 10 May 2005 06:59:32 +0200 | |
changeset 15947 | 393cfc718433 |
parent 15943 | dd7b303465a2 |
child 15951 | 63ac2e550040 |
permissions | -rw-r--r-- |
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 |
|
15938 | 10 |
working environment on common Unix platforms (e.g. Linux, Darwin, Solaris) |
10016 | 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 |
|
10115 | 16 |
suitable implementation of Standard ML (e.g. <a |
11568 | 17 |
href="http://www.polyml.org">Poly/ML</a> as included below). A |
10115 | 18 |
<em>comfortable</em> Isabelle working environment demands further user |
19 |
interface support, as provided by <a |
|
14292 | 20 |
href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> (please <a |
21 |
href="http://proofgeneral.inf.ed.ac.uk/register">register</a>). The Proof General |
|
14017 | 22 |
distribution now includes the <a |
23 |
href="http://x-symbol.sourceforge.net">X-Symbol</a> package. It |
|
24 |
should be used with a recent version of <a |
|
14636
c374608547ae
added GNU Emacs, fixed x-symbol enabling (Options menu, not Customize)
kleing
parents:
14630
diff
changeset
|
25 |
href="http://www.xemacs.org">XEmacs 21</a> or <a |
15943 | 26 |
href="http://www.gnu.org/software/emacs/emacs.html">GNU Emacs 21</a> (with |
27 |
Mule enabled). |
|
10016 | 28 |
|
29 |
<p> |
|
30 |
||
10085 | 31 |
|
32 |
<h2>Packages</h2> |
|
33 |
||
14017 | 34 |
We provide a complete set of packages for Isabelle, Proof General, and |
14630 | 35 |
PolyML. |
36 |
<p> |
|
14636
c374608547ae
added GNU Emacs, fixed x-symbol enabling (Options menu, not Customize)
kleing
parents:
14630
diff
changeset
|
37 |
While XEmacs 21 is not included here, most operating system |
10085 | 38 |
distributions already provide a suitable package, although not |
12732 | 39 |
installed by default. Some of the packages below are platform |
40 |
dependent; we include binaries for Linux/x86, Solaris/Sparc, and |
|
14630 | 41 |
Darwin/PPC (MacOS X). |
42 |
<p> |
|
43 |
Short <a href="#install">installation instructions</a> are near the |
|
44 |
bottom of this page. For more information, see the file INSTALL in |
|
45 |
<!-- _GP_ distname -->.tar.gz. |
|
10016 | 46 |
|
47 |
<p> |
|
48 |
||
49 |
<!-- _GP_ setdowncolor("\"#E0E0E0\"") --> |
|
15947 | 50 |
<table border="0" cellspacing="5" cellpadding="4" width="520" style="margin: 0px auto 0px auto"> |
10085 | 51 |
|
12722 | 52 |
<!-- _GP_ downloadhead("Isabelle") --> |
12998 | 53 |
<!-- _GP_ download(1, "Sources and documentation", distname . ".tar.gz", "../..") --> |
12731 | 54 |
<!-- _GP_ download(1, "Documentation in PDF", distname . "_pdf.tar.gz", "../..") --> |
55 |
<!-- _GP_ download(1, "Theory library in PDF and HTML", distname . "_library.tar.gz", "../..") --> |
|
10085 | 56 |
|
12722 | 57 |
<!-- _GP_ downloadhead("Proof General") --> |
14630 | 58 |
<!-- _GP_ download(1, "Proof General", "contrib/ProofGeneral-3.5.tar.gz", "../..") --> |
12722 | 59 |
|
10085 | 60 |
<!-- _GP_ downloadhead("Poly/ML compiler and runtime system") --> |
61 |
<!-- _GP_ download(1, "Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") --> |
|
12722 | 62 |
<!-- _GP_ download(3, "Poly/ML binary modules", "contrib/polyml_x86-linux.tar.gz", "../..") --> |
10085 | 63 |
<!-- _GP_ download(0, "", "contrib/polyml_sparc-solaris.tar.gz", "../..") --> |
11568 | 64 |
<!-- _GP_ download(0, "", "contrib/polyml_ppc-darwin.tar.gz", "../..") --> |
10085 | 65 |
|
12722 | 66 |
<!-- _GP_ downloadhead("Precompiled logics") --> |
67 |
<!-- _GP_ download(3, "HOL", "HOL_x86-linux.tar.gz", "../..") --> |
|
10085 | 68 |
<!-- _GP_ download(0, "", "HOL_sparc-solaris.tar.gz", "../..") --> |
12722 | 69 |
<!-- _GP_ download(0, "", "HOL_ppc-darwin.tar.gz", "../..") --> |
14024 | 70 |
<!-- _GP_ download(3, "HOL-Complex", "HOL-Complex_x86-linux.tar.gz", "../..") --> |
71 |
<!-- _GP_ download(0, "", "HOL-Complex_sparc-solaris.tar.gz", "../..") --> |
|
72 |
<!-- _GP_ download(0, "", "HOL-Complex_ppc-darwin.tar.gz", "../..") --> |
|
14630 | 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", "../..") --> |
|
12722 | 76 |
<!-- _GP_ download(3, "ZF", "ZF_x86-linux.tar.gz", "../..") --> |
10085 | 77 |
<!-- _GP_ download(0, "", "ZF_sparc-solaris.tar.gz", "../..") --> |
12722 | 78 |
<!-- _GP_ download(0, "", "ZF_ppc-darwin.tar.gz", "../..") --> |
10085 | 79 |
|
14630 | 80 |
<!-- _GP_ downloadhead("HOL4 proof terms") --> |
81 |
<!-- _GP_ download(1, "HOL4 proof terms", "contrib/HOL4-proofs.tar.gz", "../..") --> |
|
15947 | 82 |
</table> |
14630 | 83 |
|
10016 | 84 |
|
85 |
<p> |
|
86 |
||
10085 | 87 |
<h2>Installation</h2> |
10016 | 88 |
|
14630 | 89 |
<a name="install">In</a> fact, there is no installation required. Users may just unpack all |
12722 | 90 |
required packages within the same directory. The default settings of |
91 |
Isabelle should be reasonable for most circumstances. |
|
10016 | 92 |
|
93 |
<p> |
|
94 |
||
12732 | 95 |
A typical Linux/x86 site installation of Isabelle/HOL works as |
96 |
follows. By using GNU <tt>tar</tt>, the archives are uncompressed and |
|
97 |
unpacked into the <tt>/usr/local</tt> directory (this location may be |
|
98 |
changed to anything appropriate). |
|
10016 | 99 |
|
100 |
<p> |
|
101 |
||
10085 | 102 |
<tt> |
103 |
tar -C /usr/local -xzf |
|
104 |
<!-- _GP_ href(distname . ".tar.gz", distname . ".tar.gz") --> <br> |
|
105 |
tar -C /usr/local -xzf |
|
12722 | 106 |
<!-- _GP_ href("contrib/ProofGeneral.tar.gz", "ProofGeneral.tar.gz") --> <br> |
107 |
tar -C /usr/local -xzf |
|
10085 | 108 |
<!-- _GP_ href("contrib/polyml_base.tar.gz", "polyml_base.tar.gz") --> <br> |
109 |
tar -C /usr/local -xzf |
|
110 |
<!-- _GP_ href("contrib/polyml_x86-linux.tar.gz", "polyml_x86-linux.tar.gz") --> <br> |
|
111 |
tar -C /usr/local -xzf |
|
112 |
<!-- _GP_ href("HOL_x86-linux.tar.gz", "HOL_x86-linux.tar.gz") --> <br> |
|
113 |
</tt> |
|
10016 | 114 |
|
115 |
<p> |
|
116 |
||
11062 | 117 |
Users may now invoke Isabelle without further ado, e.g. run the main |
118 |
executable <tt>/usr/local/Isabelle/bin/Isabelle</tt> to launch the |
|
12052 | 119 |
Proof General interface for Isabelle/Isar. Note that there is a |
14636
c374608547ae
added GNU Emacs, fixed x-symbol enabling (Options menu, not Customize)
kleing
parents:
14630
diff
changeset
|
120 |
separate option in the Proof General <em>Options</em> menu to enable |
14017 | 121 |
X-Symbol. |
10085 | 122 |
|
15482 | 123 |
<p> |
124 |
||
125 |
If Emacs appears to hang when the prover process is started, see the |
|
126 |
<A HREF="http://proofgeneral.inf.ed.ac.uk/FAQ">Proof General FAQ</a> |
|
127 |
for advice. |
|
128 |
||
15947 | 129 |
<h3>Other platforms</h3> |
14668 | 130 |
|
15938 | 131 |
<p>Although Isabelle is nativly designed for Unix environments |
132 |
(e.g. Solaris, Linux), it may also run under similar, Unix-like |
|
133 |
platforms. The following installation instructions are hints |
|
134 |
contributed by Isabelle users. Feel free to contact us for any |
|
135 |
suggestions, corrections or improvements.</p> |
|
14668 | 136 |
|
15935 | 137 |
<ul> |
15938 | 138 |
<li><a href="notes_macos_darwin.html">Installation notes for Mac OS X</a></li> |
139 |
<li><a href="notes_win_cygwin.html">Installation notes for Cygwin/Windows</a></li> |
|
15935 | 140 |
</ul> |
141 |