|
16673
|
1 |
<?xml version='1.0' encoding='iso-8859-1' ?>
|
|
|
2 |
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
|
|
|
3 |
<!-- $Id$ -->
|
|
|
4 |
<html xmlns="http://www.w3.org/1999/xhtml">
|
|
|
5 |
|
|
|
6 |
<head>
|
|
|
7 |
<title>Installation instructions</title>
|
|
|
8 |
<?include file="//include/htmlheader.include.html"?>
|
|
|
9 |
</head>
|
|
|
10 |
|
|
16674
|
11 |
<body>
|
|
16673
|
12 |
<?include file="//include/header.include.html"?>
|
|
|
13 |
<div class="hr"><hr/></div>
|
|
|
14 |
<?include file="//include/navigation.include.html"?>
|
|
|
15 |
<div class="hr"><hr/></div>
|
|
|
16 |
|
|
|
17 |
<div id="content">
|
|
|
18 |
|
|
|
19 |
<h2>General</h2>
|
|
|
20 |
|
|
|
21 |
<p>
|
|
|
22 |
Isabelle runs on common Unix platforms.
|
|
|
23 |
For Linux, Solaris and MaxOS / Darwin, we provide ready-to-install bundles;
|
|
|
24 |
for other Unices, Isabelle has to be built from scratch.
|
|
|
25 |
</p>
|
|
|
26 |
|
|
|
27 |
<p>
|
|
|
28 |
A usable Isabelle system consists of the following components:
|
|
|
29 |
</p>
|
|
|
30 |
|
|
|
31 |
<ul>
|
|
|
32 |
<li>a suitable ML environment for Standard ML</li>
|
|
|
33 |
<li>the Isabelle system itself, including the desired object logic(s)
|
|
|
34 |
(e. g. HOL)</li>
|
|
|
35 |
<li>the ProofGeneral user interface</li>
|
|
|
36 |
</ul>
|
|
|
37 |
|
|
|
38 |
<p>Optionally, theory graph browsing may be used if a Java JRE 1.1 or above
|
|
|
39 |
is installed.</p>
|
|
|
40 |
|
|
|
41 |
<p>For operating-system-specific instructions:</p>
|
|
|
42 |
|
|
|
43 |
<ul>
|
|
|
44 |
<li><a href="#install_linux">Linux (x86)</a></li>
|
|
|
45 |
<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>
|
|
|
49 |
|
|
|
50 |
<h2 id="install_linux">Linux</h2>
|
|
|
51 |
|
|
|
52 |
<p>Commonly, an installation of Isabelle could work as follows:</p>
|
|
|
53 |
|
|
|
54 |
<ul>
|
|
|
55 |
<li>Ensure that your system has a running XEmacs 21 or Emacs 21
|
|
|
56 |
with mule support (for ProofGeneral)</li>
|
|
|
57 |
<li>Get the packages for <a href="http://www.polyml.org">Poly/ML</a>,
|
|
|
58 |
<a href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> (including
|
|
|
59 |
the Emacs <a href="http://x-symbol.sourceforge.net">X-Symbol</a> package)
|
|
|
60 |
and Isabelle,
|
|
|
61 |
either from our <a href="download.html">package page</a> or from the
|
|
|
62 |
links below. When you download ProofGeneral, please
|
|
|
63 |
<a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li>
|
|
|
64 |
<li>Likewise download the compiled image(s) of your desired object logic(s)</li>
|
|
|
65 |
<li>Unpack the archives to an appropriate location, e. g.
|
|
|
66 |
<tt class="shellcmd">/usr/local</tt>:
|
|
|
67 |
<ul class="shellcmd">
|
|
|
68 |
<li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li>
|
|
|
69 |
<li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
|
|
|
70 |
<li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_base.tar.gz"?></li>
|
|
|
71 |
<li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_x86-linux.tar.gz"?></li>
|
|
|
72 |
<li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_x86-linux.tar.gz"?></li>
|
|
|
73 |
</ul>
|
|
|
74 |
</li>
|
|
|
75 |
<li>Under most circumstances, the default settings of Isabelle should be reasonable for
|
|
|
76 |
invoking Isabelle/ProofGeneral without further ado:
|
|
|
77 |
<ul class="shellcmd">
|
|
|
78 |
<li>/usr/local/Isabelle/bin/Isabelle</li>
|
|
|
79 |
</ul>
|
|
|
80 |
Note that there is a separate option in
|
|
|
81 |
the Proof General <em>Options</em> menu to enable X-Symbol.
|
|
|
82 |
</li>
|
|
|
83 |
<li>If Emacs appears to hang when the prover process is started, see the
|
|
|
84 |
<a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for
|
|
|
85 |
advice.
|
|
|
86 |
</li>
|
|
|
87 |
</ul>
|
|
|
88 |
|
|
|
89 |
<p>For more information, see the file <a href="//dist/packages/Isabelle/INSTALL">INSTALL</a>.</p>
|
|
|
90 |
|
|
|
91 |
<h2 id="install_solaris">Solaris</h2>
|
|
|
92 |
|
|
|
93 |
<p>Before you start, ensure the following for your system:</p>
|
|
|
94 |
<ul>
|
|
|
95 |
<li>GNU bash 2.x</li>
|
|
|
96 |
<li>perl 5.x</li>
|
|
|
97 |
<li>GNU tar 1.13 or higher</li>
|
|
|
98 |
<li>GNU gzip 1.3 or higher</li>
|
|
|
99 |
<li>running XEmacs 21 or Emacs 21
|
|
|
100 |
with mule support (for ProofGeneral)</li>
|
|
|
101 |
</ul>
|
|
|
102 |
|
|
|
103 |
<p>Then, an installation on Solaris is analogous to Linux:</p>
|
|
|
104 |
|
|
|
105 |
<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.
|
|
|
115 |
<tt class="shellcmd">/usr/local</tt>:
|
|
|
116 |
<ul class="shellcmd">
|
|
|
117 |
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li>
|
|
|
118 |
<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>
|
|
|
121 |
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_sparc-solaris.tar.gz"?></li>
|
|
|
122 |
</ul>
|
|
|
123 |
</li>
|
|
|
124 |
<li>Under most circumstances, the default settings of Isabelle should be reasonable for
|
|
|
125 |
invoking Isabelle/ProofGeneral without further ado:
|
|
|
126 |
<ul class="shellcmd">
|
|
|
127 |
<li>/usr/local/Isabelle/bin/Isabelle</li>
|
|
|
128 |
</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>
|
|
|
136 |
</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 |
|
|
|
196 |
</div>
|
|
|
197 |
<div class="hr"><hr/></div>
|
|
16674
|
198 |
<?include file="//include/footer.include.html"?>
|
|
16673
|
199 |
</body>
|
|
|
200 |
|
|
|
201 |
</html>
|