17 <div id="content"> |
17 <div id="content"> |
18 |
18 |
19 <h2>General</h2> |
19 <h2>General</h2> |
20 |
20 |
21 <p> |
21 <p> |
22 Isabelle runs on common Unix platforms. |
22 Isabelle runs on common Unix platforms. We provide |
23 For Linux, Solaris and MaxOS / Darwin, we provide ready-to-install bundles; |
23 ready-to-use binary packages for Linux/x86, MaxOS X / |
24 for other Unices, Isabelle has to be built from scratch. |
24 Darwin, and Solaris. For other platforms, Isabelle logics |
|
25 need to be compiled separately (see also <a |
|
26 href="//dist/packages/Isabelle/INSTALL">INSTALL</a>). |
25 </p> |
27 </p> |
26 |
28 |
27 <p> |
29 <p> |
28 A usable Isabelle system consists of the following components: |
30 A practically usable Isabelle system consists of the |
|
31 following components: |
29 </p> |
32 </p> |
30 |
33 |
31 <ul> |
34 <ul> |
32 <li>a suitable ML environment for Standard ML</li> |
35 <li>a suitable ML environment for Standard ML</li> |
33 <li>the Isabelle system itself, including the desired object logic(s) |
36 <li>the Isabelle system itself, including the desired object logics |
34 (e. g. HOL)</li> |
37 (e. g. HOL, HOL-Complex)</li> |
35 <li>the ProofGeneral user interface</li> |
38 <li>the ProofGeneral user interface</li> |
36 </ul> |
39 </ul> |
37 |
40 |
38 <p>Optionally, theory graph browsing may be used if a Java JRE 1.1 or above |
41 <p>Optionally, theory graph browsing may be used if a Java JRE 1.1 or above |
39 is installed.</p> |
42 is installed.</p> |
40 |
43 |
41 <p>For operating-system-specific instructions:</p> |
44 <p>For operating-system-specific instructions:</p> |
42 |
45 |
43 <ul> |
46 <ul> |
44 <li><a href="#install_linux">Linux (x86)</a></li> |
47 <li><a href="#install_linux">Linux (x86)</a></li> |
|
48 <li><a href="#install_darwin">MacOS X / Darwin (ppc)</a></li> |
45 <li><a href="#install_solaris">Solaris (sparc)</a></li> |
49 <li><a href="#install_solaris">Solaris (sparc)</a></li> |
46 <li><a href="#install_darwin">MacOS X / Darwin</a></li> |
|
47 <li><a href="#install_windows">Windows</a></li> |
|
48 </ul> |
50 </ul> |
49 |
51 |
50 <h2 id="install_linux">Linux</h2> |
52 <h2 id="install_linux">Linux</h2> |
51 |
53 |
52 <p>Commonly, an installation of Isabelle could work as follows:</p> |
54 <p>Installation of Isabelle/HOL on common Linux/x86 platforms |
|
55 works as follows:</p> |
53 |
56 |
54 <ul> |
57 <ul> |
55 <li>Ensure that your system has a running XEmacs 21 or Emacs 21 |
58 <li>For ProofGeneral, ensure that your system has a |
56 with mule support (for ProofGeneral)</li> |
59 working installation of XEmacs 21, or Emacs 21 with |
57 <li>Get the packages for <a href="http://www.polyml.org">Poly/ML</a>, |
60 mule support. The XEmacs 21.1.x and 21.4.x versions |
58 <a href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> (including |
61 are known to work reasonably well, but the beta branch |
59 the Emacs <a href="http://x-symbol.sourceforge.net">X-Symbol</a> package) |
62 of XEmacs 21.5.x usually fails!</li> |
60 and Isabelle, |
63 |
61 either from our <a href="download.html">package page</a> or from the |
64 <li>Get the packages for <a |
62 links below. When you download ProofGeneral, please |
65 href="http://www.polyml.org">Poly/ML</a>, <a |
63 <a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li> |
66 href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> |
64 <li>Likewise download the compiled image(s) of your desired object logic(s)</li> |
67 and Isabelle – all of this is available from the |
|
68 Isabelle <a href="download.html">Packages</a> page. |
|
69 When you download ProofGeneral for the first time, |
|
70 please <a |
|
71 href="http://proofgeneral.inf.ed.ac.uk/register">register</a>.</li> |
|
72 |
|
73 <li>Likewise download the compiled images of the desired |
|
74 Isabelle object logics.</li> |
|
75 |
65 <li>Unpack the archives to an appropriate location, e. g. |
76 <li>Unpack the archives to an appropriate location, e. g. |
66 <tt class="shellcmd">/usr/local</tt>: |
77 <tt class="shellcmd">/usr/local</tt>: |
67 <ul class="shellcmd"> |
78 <ul class="shellcmd"> |
68 <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li> |
79 <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.tar.gz"?></li> |
69 <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li> |
80 <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_x86-linux.tar.gz"?></li> |
70 <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_base.tar.gz"?></li> |
81 <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_x86-linux.tar.gz"?></li> |
71 <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_x86-linux.tar.gz"?></li> |
82 <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li> |
72 <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_x86-linux.tar.gz"?></li> |
|
73 </ul> |
83 </ul> |
74 </li> |
84 </li> |
75 <li>Under most circumstances, the default settings of Isabelle should be reasonable for |
85 |
76 invoking Isabelle/ProofGeneral without further ado: |
86 <li>Under most circumstances, the default settings of |
|
87 Isabelle should be reasonable for invoking |
|
88 Isabelle/ProofGeneral without further ado: |
77 <ul class="shellcmd"> |
89 <ul class="shellcmd"> |
78 <li>/usr/local/Isabelle/bin/Isabelle</li> |
90 <li>/usr/local/Isabelle/bin/Isabelle</li> |
79 </ul> |
91 </ul> |
80 Note that there is a separate option in |
92 |
81 the Proof General <em>Options</em> menu to enable X-Symbol. |
93 Failure on this is typically a problem with unstable |
82 </li> |
94 XEmacs versions; consider command line option |
83 <li>If Emacs appears to hang when the prover process is started, see the |
95 <code>-p</code> to specify a different xemacs |
84 <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for |
96 executable. |
85 advice. |
97 |
|
98 The X-Symbol package is already included in Proof |
|
99 General, but needs to be enabled separately; use the |
|
100 <code>-x</code> command line option, or the |
|
101 <em>Options</em> menu. |
86 </li> |
102 </li> |
87 </ul> |
103 </ul> |
88 |
104 |
89 <p>For more information, see the file <a href="//dist/packages/Isabelle/INSTALL">INSTALL</a>.</p> |
105 <h2 id="install_darwin">MaxOS X / Darwin</h2> |
|
106 |
|
107 <p>Ensure that your system provides the following:</p> |
|
108 <ul> |
|
109 <li>MacOS X 10.2.2 or higher</li> |
|
110 |
|
111 <li>XEmacs 21, or Emacs 21 with mule support (for |
|
112 ProofGeneral) – for further reference, see the |
|
113 <a href="installation_macos_emacs.html">MacOS X Emacs |
|
114 hints</a>. </li> |
|
115 </ul> |
|
116 |
|
117 <p>Then installation on MacOS X / Darwin is analogous to |
|
118 Linux, but note that some GNU executables are named |
|
119 differently.</p> |
|
120 |
|
121 <ul> |
|
122 <li>Unpack the archives to an appropriate location, e. g. |
|
123 <tt class="shellcmd">/usr/local</tt>: |
|
124 <ul class="shellcmd"> |
|
125 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.tar.gz"?></li> |
|
126 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li> |
|
127 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_ppc-darwin.tar.gz"?></li> |
|
128 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_ppc-darwin.tar.gz"?></li> |
|
129 </ul> |
|
130 </li> |
|
131 |
|
132 <li>Invoke Isabelle/ProofGeneral as follows: |
|
133 <ul class="shellcmd"> |
|
134 <li>/usr/local/Isabelle/bin/Isabelle</li> |
|
135 </ul> |
|
136 </li> |
|
137 |
|
138 </ul> |
90 |
139 |
91 <h2 id="install_solaris">Solaris</h2> |
140 <h2 id="install_solaris">Solaris</h2> |
92 |
141 |
93 <p>Before you start, ensure the following for your system:</p> |
142 <p>Ensure that the following tools are available on your system:</p> |
94 <ul> |
143 <ul> |
|
144 <li>Perl 5.x</li> |
95 <li>GNU bash 2.x</li> |
145 <li>GNU bash 2.x</li> |
96 <li>perl 5.x</li> |
|
97 <li>GNU tar 1.13 or higher</li> |
146 <li>GNU tar 1.13 or higher</li> |
98 <li>GNU gzip 1.3 or higher</li> |
147 <li>GNU gzip 1.3 or higher</li> |
99 <li>running XEmacs 21 or Emacs 21 |
148 <li>XEmacs 21, or Emacs 21 with mule support (for ProofGeneral)</li> |
100 with mule support (for ProofGeneral)</li> |
|
101 </ul> |
149 </ul> |
102 |
150 |
103 <p>Then, an installation on Solaris is analogous to Linux:</p> |
151 <p>The rest of the installation is analogous to Linux (see |
|
152 above).</p> |
104 |
153 |
105 <ul> |
154 <ul> |
106 <li>Get the packages for <a href="http://www.polyml.org">Poly/ML</a>, |
|
107 <a href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> (including |
|
108 the Emacs <a href="http://x-symbol.sourceforge.net">X-Symbol</a> package) |
|
109 and Isabelle, |
|
110 either from our <a href="download.html">package page</a> or from the |
|
111 links below. When you download ProofGeneral, please |
|
112 <a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li> |
|
113 <li>Likewise download the compiled image(s) of your desired object logic(s)</li> |
|
114 <li>Unpack the archives to an appropriate location, e. g. |
155 <li>Unpack the archives to an appropriate location, e. g. |
115 <tt class="shellcmd">/usr/local</tt>: |
156 <tt class="shellcmd">/usr/local</tt>: |
116 <ul class="shellcmd"> |
157 <ul class="shellcmd"> |
117 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li> |
158 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.tar.gz"?></li> |
118 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li> |
159 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li> |
119 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_base.tar.gz"?></li> |
|
120 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_sparc-solaris.tar.gz"?></li> |
160 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_sparc-solaris.tar.gz"?></li> |
121 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_sparc-solaris.tar.gz"?></li> |
161 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_sparc-solaris.tar.gz"?></li> |
122 </ul> |
162 </ul> |
123 </li> |
163 </li> |
124 <li>Under most circumstances, the default settings of Isabelle should be reasonable for |
164 |
125 invoking Isabelle/ProofGeneral without further ado: |
165 <li>Invoke Isabelle/ProofGeneral as follows: |
126 <ul class="shellcmd"> |
166 <ul class="shellcmd"> |
127 <li>/usr/local/Isabelle/bin/Isabelle</li> |
167 <li>/usr/local/Isabelle/bin/Isabelle</li> |
128 </ul> |
168 </ul> |
129 Note that there is a separate option in |
|
130 the Proof General <em>Options</em> menu to enable X-Symbol. |
|
131 </li> |
|
132 <li>If Emacs appears to hang when the prover process is started, see the |
|
133 <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for |
|
134 advice. |
|
135 </li> |
169 </li> |
136 </ul> |
170 </ul> |
137 |
|
138 <p>For more information, see the file <a href="//dist/packages/Isabelle/INSTALL">INSTALL</a>.</p> |
|
139 |
|
140 <h2 id="install_darwin">MaxOS X / Darwin</h2> |
|
141 |
|
142 <p>Before you start, ensure the following for your system:</p> |
|
143 <ul> |
|
144 <li>running MacOS X 10.2.2 or higher</li> |
|
145 <li>running XEmacs 21 or Emacs 21 with mule support (for ProofGeneral) |
|
146 – for further reference, see the |
|
147 <a href="installation_macos_emacs.html">MacOS X Emacs hints</a> |
|
148 </li> |
|
149 </ul> |
|
150 |
|
151 <p>Then, an installation on Darwin is analogous to Linux:</p> |
|
152 |
|
153 <ul> |
|
154 <li>Get the packages for <a href="http://www.polyml.org">Poly/ML</a>, |
|
155 <a href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> (including |
|
156 the Emacs <a href="http://x-symbol.sourceforge.net">X-Symbol</a> package) |
|
157 and Isabelle, |
|
158 either from our <a href="download.html">package page</a> or from the |
|
159 links below. When you download ProofGeneral, please |
|
160 <a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li> |
|
161 <li>Likewise download the compiled image(s) of your desired object logic(s)</li> |
|
162 <li>Unpack the archives to an appropriate location, e. g. |
|
163 <tt class="shellcmd">/usr/local</tt>: |
|
164 <ul class="shellcmd"> |
|
165 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li> |
|
166 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li> |
|
167 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_base.tar.gz"?></li> |
|
168 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_ppc-darwin.tar.gz"?></li> |
|
169 <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_ppc-darwin.tar.gz"?></li> |
|
170 </ul> |
|
171 </li> |
|
172 <li>Under most circumstances, the default settings of Isabelle should be reasonable for |
|
173 invoking Isabelle/ProofGeneral without further ado: |
|
174 <ul class="shellcmd"> |
|
175 <li>/usr/local/Isabelle/bin/Isabelle</li> |
|
176 </ul> |
|
177 Note that there is a separate option in |
|
178 the Proof General <em>Options</em> menu to enable X-Symbol. |
|
179 </li> |
|
180 <li>If Emacs appears to hang when the prover process is started, see the |
|
181 <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for |
|
182 advice. |
|
183 </li> |
|
184 </ul> |
|
185 |
|
186 <h2 id="install_windows">Windows</h2> |
|
187 |
|
188 <p>Isabelle does not run nativly on Windows; in a restricted fashion, |
|
189 you may run Isabelle on Windows using the Cygwin environment. |
|
190 See <a href="installation_notes_cygwin.html">Installation notes for |
|
191 Cygwin/Windows</a>.</p> |
|
192 |
|
193 <p>For a serious apporach, you should consider a Windows/Linux dualboot |
|
194 installation.</p> |
|
195 |
171 |
196 </div> |
172 </div> |
197 <div class="hr"><hr/></div> |
173 <div class="hr"><hr/></div> |
198 <?include file="//include/footer.include.html"?> |
174 <?include file="//include/footer.include.html"?> |
199 </body> |
175 </body> |