|
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>
|
|
17661
|
22 |
Isabelle runs on common Unix platforms. We provide
|
|
|
23 |
ready-to-use binary packages for Linux/x86, MaxOS X /
|
|
|
24 |
Darwin, and Solaris. For other platforms, Isabelle logics
|
|
|
25 |
need to be compiled separately (see also <a
|
|
17671
|
26 |
href="//dist/Isabelle/INSTALL">INSTALL</a>).
|
|
16673
|
27 |
</p>
|
|
|
28 |
|
|
|
29 |
<p>
|
|
17661
|
30 |
A practically usable Isabelle system consists of the
|
|
|
31 |
following components:
|
|
16673
|
32 |
</p>
|
|
|
33 |
|
|
|
34 |
<ul>
|
|
|
35 |
<li>a suitable ML environment for Standard ML</li>
|
|
17661
|
36 |
<li>the Isabelle system itself, including the desired object logics
|
|
|
37 |
(e. g. HOL, HOL-Complex)</li>
|
|
16673
|
38 |
<li>the ProofGeneral user interface</li>
|
|
|
39 |
</ul>
|
|
|
40 |
|
|
|
41 |
<p>Optionally, theory graph browsing may be used if a Java JRE 1.1 or above
|
|
|
42 |
is installed.</p>
|
|
|
43 |
|
|
|
44 |
<p>For operating-system-specific instructions:</p>
|
|
|
45 |
|
|
|
46 |
<ul>
|
|
|
47 |
<li><a href="#install_linux">Linux (x86)</a></li>
|
|
17661
|
48 |
<li><a href="#install_darwin">MacOS X / Darwin (ppc)</a></li>
|
|
16673
|
49 |
<li><a href="#install_solaris">Solaris (sparc)</a></li>
|
|
|
50 |
</ul>
|
|
|
51 |
|
|
|
52 |
<h2 id="install_linux">Linux</h2>
|
|
|
53 |
|
|
17661
|
54 |
<p>Installation of Isabelle/HOL on common Linux/x86 platforms
|
|
|
55 |
works as follows:</p>
|
|
16673
|
56 |
|
|
|
57 |
<ul>
|
|
17661
|
58 |
<li>For ProofGeneral, ensure that your system has a
|
|
|
59 |
working installation of XEmacs 21, or Emacs 21 with
|
|
|
60 |
mule support. The XEmacs 21.1.x and 21.4.x versions
|
|
|
61 |
are known to work reasonably well, but the beta branch
|
|
|
62 |
of XEmacs 21.5.x usually fails!</li>
|
|
|
63 |
|
|
|
64 |
<li>Get the packages for <a
|
|
|
65 |
href="http://www.polyml.org">Poly/ML</a>, <a
|
|
|
66 |
href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a>
|
|
|
67 |
and Isabelle – all of this is available from the
|
|
17685
|
68 |
Isabelle <a href="download.html">download</a> page.
|
|
17661
|
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 |
|
|
16673
|
76 |
<li>Unpack the archives to an appropriate location, e. g.
|
|
|
77 |
<tt class="shellcmd">/usr/local</tt>:
|
|
|
78 |
<ul class="shellcmd">
|
|
17671
|
79 |
<li>tar -C /usr/local -xzf <?downloadLink target="//dist/Isabelle2005.tar.gz"?></li>
|
|
17685
|
80 |
<li>tar -C /usr/local -xzf <?downloadLink target="//dist/contrib/ProofGeneral.tar.gz"?></li>
|
|
17671
|
81 |
<li>tar -C /usr/local -xzf <?downloadLink target="//dist/contrib/polyml_x86-linux.tar.gz"?></li>
|
|
|
82 |
<li>tar -C /usr/local -xzf <?downloadLink target="//dist/HOL_x86-linux.tar.gz"?></li>
|
|
16673
|
83 |
</ul>
|
|
|
84 |
</li>
|
|
17661
|
85 |
|
|
|
86 |
<li>Under most circumstances, the default settings of
|
|
|
87 |
Isabelle should be reasonable for invoking
|
|
|
88 |
Isabelle/ProofGeneral without further ado:
|
|
16673
|
89 |
<ul class="shellcmd">
|
|
|
90 |
<li>/usr/local/Isabelle/bin/Isabelle</li>
|
|
|
91 |
</ul>
|
|
17661
|
92 |
|
|
|
93 |
Failure on this is typically a problem with unstable
|
|
|
94 |
XEmacs versions; consider command line option
|
|
|
95 |
<code>-p</code> to specify a different xemacs
|
|
|
96 |
executable.
|
|
|
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.
|
|
16673
|
102 |
</li>
|
|
17672
|
103 |
|
|
|
104 |
<li>Isabelle may also be run without ProofGeneral, as a
|
|
|
105 |
plain shell process as follows:
|
|
|
106 |
<ul class="shellcmd">
|
|
|
107 |
<li>/usr/local/Isabelle/bin/isabelle-process -I</li>
|
|
|
108 |
</ul>
|
|
|
109 |
Type CTRL-D to exit.
|
|
|
110 |
|
|
|
111 |
If the above does not work at all, maybe you are
|
|
|
112 |
suffering from a known problem of Poly/ML on certain
|
|
|
113 |
Linux versions, see also <a
|
|
|
114 |
href="http://www.polyml.org/linuxsegfault.html">Segmentation
|
|
|
115 |
faults with Linux</a> on the Poly/ML site.
|
|
17678
|
116 |
</li>
|
|
|
117 |
</ul>
|
|
16673
|
118 |
|
|
17661
|
119 |
<h2 id="install_darwin">MaxOS X / Darwin</h2>
|
|
|
120 |
|
|
|
121 |
<p>Ensure that your system provides the following:</p>
|
|
|
122 |
<ul>
|
|
|
123 |
<li>MacOS X 10.2.2 or higher</li>
|
|
|
124 |
|
|
|
125 |
<li>XEmacs 21, or Emacs 21 with mule support (for
|
|
|
126 |
ProofGeneral) – for further reference, see the
|
|
|
127 |
<a href="installation_macos_emacs.html">MacOS X Emacs
|
|
|
128 |
hints</a>. </li>
|
|
|
129 |
</ul>
|
|
|
130 |
|
|
|
131 |
<p>Then installation on MacOS X / Darwin is analogous to
|
|
|
132 |
Linux, but note that some GNU executables are named
|
|
|
133 |
differently.</p>
|
|
|
134 |
|
|
|
135 |
<ul>
|
|
|
136 |
<li>Unpack the archives to an appropriate location, e. g.
|
|
|
137 |
<tt class="shellcmd">/usr/local</tt>:
|
|
|
138 |
<ul class="shellcmd">
|
|
17671
|
139 |
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/Isabelle2005.tar.gz"?></li>
|
|
|
140 |
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/ProofGeneral.tar.gz"?></li>
|
|
|
141 |
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/polyml_ppc-darwin.tar.gz"?></li>
|
|
|
142 |
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/HOL_ppc-darwin.tar.gz"?></li>
|
|
17661
|
143 |
</ul>
|
|
|
144 |
</li>
|
|
|
145 |
|
|
|
146 |
<li>Invoke Isabelle/ProofGeneral as follows:
|
|
|
147 |
<ul class="shellcmd">
|
|
|
148 |
<li>/usr/local/Isabelle/bin/Isabelle</li>
|
|
|
149 |
</ul>
|
|
|
150 |
</li>
|
|
|
151 |
|
|
|
152 |
</ul>
|
|
16673
|
153 |
|
|
|
154 |
<h2 id="install_solaris">Solaris</h2>
|
|
|
155 |
|
|
17661
|
156 |
<p>Ensure that the following tools are available on your system:</p>
|
|
16673
|
157 |
<ul>
|
|
17661
|
158 |
<li>Perl 5.x</li>
|
|
16673
|
159 |
<li>GNU bash 2.x</li>
|
|
|
160 |
<li>GNU tar 1.13 or higher</li>
|
|
|
161 |
<li>GNU gzip 1.3 or higher</li>
|
|
17661
|
162 |
<li>XEmacs 21, or Emacs 21 with mule support (for ProofGeneral)</li>
|
|
16673
|
163 |
</ul>
|
|
|
164 |
|
|
17661
|
165 |
<p>The rest of the installation is analogous to Linux (see
|
|
|
166 |
above).</p>
|
|
16673
|
167 |
|
|
|
168 |
<ul>
|
|
|
169 |
<li>Unpack the archives to an appropriate location, e. g.
|
|
|
170 |
<tt class="shellcmd">/usr/local</tt>:
|
|
|
171 |
<ul class="shellcmd">
|
|
17671
|
172 |
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/Isabelle2005.tar.gz"?></li>
|
|
|
173 |
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/ProofGeneral.tar.gz"?></li>
|
|
|
174 |
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/polyml_sparc-solaris.tar.gz"?></li>
|
|
|
175 |
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/HOL_sparc-solaris.tar.gz"?></li>
|
|
16673
|
176 |
</ul>
|
|
|
177 |
</li>
|
|
17661
|
178 |
|
|
|
179 |
<li>Invoke Isabelle/ProofGeneral as follows:
|
|
16673
|
180 |
<ul class="shellcmd">
|
|
|
181 |
<li>/usr/local/Isabelle/bin/Isabelle</li>
|
|
|
182 |
</ul>
|
|
|
183 |
</li>
|
|
|
184 |
</ul>
|
|
|
185 |
|
|
|
186 |
</div>
|
|
|
187 |
<div class="hr"><hr/></div>
|
|
16674
|
188 |
<?include file="//include/footer.include.html"?>
|
|
16673
|
189 |
</body>
|
|
|
190 |
|
|
|
191 |
</html>
|