|
16674
|
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 notes for Windows/Cygwin</title>
|
|
|
8 |
<?include file="//include/htmlheader.include.html"?>
|
|
|
9 |
</head>
|
|
|
10 |
|
|
|
11 |
<body class="dist">
|
|
|
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>Preconditions and restrictions</h2>
|
|
|
20 |
|
|
|
21 |
<p>Please notice before you go ahead:</p>
|
|
|
22 |
|
|
|
23 |
<ul>
|
|
|
24 |
<li>The ML system these notes apply to is <a href=
|
|
|
25 |
"http://www.smlnj.org/">Standard ML of New Jersey</a>; it is <em>not</em>
|
|
|
26 |
known yet how to get Isabelle run completely with <a href=
|
|
|
27 |
"www.polyml.org/">Poly/ML</a>. See <a href="#polyml">a note on Poly/ML</a>
|
|
|
28 |
down this page.</li>
|
|
|
29 |
|
|
|
30 |
<li>It is assumed you have some experience with an Unix operating system
|
|
|
31 |
(e.g. what a shell is for and how to use it).</li>
|
|
|
32 |
</ul>
|
|
|
33 |
|
|
|
34 |
<p>Any suggestions and improvements concerning this hints are welcomed!</p>
|
|
|
35 |
|
|
|
36 |
<h2>Acknowlegements</h2>
|
|
|
37 |
|
|
|
38 |
<p>Thanks to <a href=
|
|
|
39 |
"http://cswww.essex.ac.uk/Research/FSS/projects/isawin/">Norbert
|
|
|
40 |
Völker</a> and <a href=
|
|
|
41 |
"http://www.abo.fi/~viorel.preoteasa/isabelle/">Viorel Preoteasa</a> whose
|
|
|
42 |
efforts helped a lot to get Isabelle run this way.</p>
|
|
|
43 |
|
|
|
44 |
<h2>Installing Cygwin</h2>
|
|
|
45 |
|
|
|
46 |
<p>Cygwin is a POSIX emulation layer for Windows; it contains ports of a
|
|
|
47 |
large collection of common Unix software (shells, perl, gcc, X11, latex,
|
|
|
48 |
ImageMagick, …).</p>
|
|
|
49 |
|
|
|
50 |
<p>To install it, get the installer from the <a href=
|
|
|
51 |
"http://www.cygwin.com">Cygwin website</a> and run it. It will ask you which
|
|
|
52 |
packages to install, and then downloads and installs them. Please make sure
|
|
|
53 |
you install everything needed by Isabelle; it is hard to give a concise list
|
|
|
54 |
of packages here since the bundling of Cygwin packages may vary over time,
|
|
|
55 |
but installing the base packages, perl, make, xemacs and x-server should be a
|
|
|
56 |
good choice for the beginning.</p>
|
|
|
57 |
|
|
|
58 |
<p>By default, cygwin installs to <tt class="shellcmd">c:\cygwin</tt>; you may choose an
|
|
|
59 |
arbitrary location, but it is recommended that it does not include any space
|
|
|
60 |
or exotic characters. This directory will then become the root directory of
|
|
|
61 |
the Cygwin filesystem tree, i.e. the Cygwin path <tt class="shellcmd">/opt/smlnj</tt> will be
|
|
|
62 |
mapped to Windows path <tt class="shellcmd">c:\cygwin\opt\smlnj</tt>.</p>
|
|
|
63 |
|
|
|
64 |
<p>After installation, open a Cygwin shell window (normally the installer
|
|
|
65 |
makes a shortcut for you).</p>
|
|
|
66 |
|
|
|
67 |
<h2>Getting and building SML/NJ</h2>
|
|
|
68 |
|
|
|
69 |
<p>Now we are ready to get and build <a href=
|
|
|
70 |
"http://www.smlnj.org/">SML/NJ</a>; before this, set the environment variable
|
|
|
71 |
SMLNJ_CYGWIN_RUNTIME to 1:</p>
|
|
|
72 |
|
|
|
73 |
<ul class="shellcmd">
|
|
|
74 |
<li>export SMLNJ_CYGWIN_RUNTIME=1</li>
|
|
|
75 |
</ul>
|
|
|
76 |
|
|
|
77 |
<p>This setting will tell the build process that it should
|
|
|
78 |
<em>not</em> attempt to build SML/NJ natively for Win32 but for Cygwin
|
|
|
79 |
instead (see further <a href=
|
|
|
80 |
"http://smlnj.cs.uchicago.edu/dist/working/110.53/CYGWININSTALL">CYGWININSTALL</a>).</p>
|
|
|
81 |
|
|
|
82 |
<p>So far, this setup was tested using the working version 110.53 of SML/NJ
|
|
|
83 |
from <a href=
|
|
|
84 |
"http://smlnj.cs.uchicago.edu/dist/working/110.53/">http://smlnj.cs.uchicago.edu/dist/working/110.53/</a>.
|
|
|
85 |
SML/NJ provides a nice installer enabling you to download and build it. Read
|
|
|
86 |
<a href=
|
|
|
87 |
"http://smlnj.cs.uchicago.edu/dist/working/110.53/INSTALL">INSTALL</a> to
|
|
|
88 |
learn about the different possibilites to do this. The default packages
|
|
|
89 |
should be sufficient.</p>
|
|
|
90 |
|
|
|
91 |
<p>In the following, it is assumed that you install SML/NJ to Cygwin path
|
|
|
92 |
<tt class="shellcmd">/opt/smlnj</tt>; if you choose an other location, some tweaking in the
|
|
|
93 |
<a href="#config"><tt class="shellcmd">etc/settings</tt> file</a> may be neccessary later.</p>
|
|
|
94 |
|
|
|
95 |
<p>Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable must
|
|
|
96 |
be set to 1 (later on a convenient mechanism to make this the default is
|
|
|
97 |
proposed).</p>
|
|
|
98 |
|
|
|
99 |
<h2>Installing Isabelle</h2>
|
|
|
100 |
|
|
|
101 |
<p>Download the latest Isabelle and ProofGeneral <a href=
|
|
|
102 |
"download.html">release packages</a>. Assuming that you are in the directory
|
|
|
103 |
where you downloaded the files, install them into <tt class="shellcmd">/opt</tt> by typing
|
|
|
104 |
into the bash shell:</p>
|
|
|
105 |
|
|
|
106 |
<ul class="shellcmd">
|
|
|
107 |
<li>tar -C /usr/opt -xvzf <?value key="distname"?>.tar.gz</li>
|
|
|
108 |
<li>tar -C /usr/opt -xvzf ProofGeneral.tar.gz</li>
|
|
|
109 |
</ul>
|
|
|
110 |
|
|
|
111 |
<p>During extraction, one inconvenience may occur, see <a href=
|
|
|
112 |
"#inconvenience">below</a>.</p>
|
|
|
113 |
|
|
|
114 |
<p>The location <tt class="shellcmd">/opt</tt> again is just a proposal; if you choose other
|
|
|
115 |
locations, some tweaking in the <a href="#config"><tt class="shellcmd">etc/settings</tt>
|
|
|
116 |
file</a> may be neccessary later.</p>
|
|
|
117 |
|
|
|
118 |
<h2 id="config">Configuring Isabelle</h2>
|
|
|
119 |
|
|
|
120 |
<p>Edit the file <tt class="shellcmd">/opt/Isabelle/etc/settings</tt>; first, uncomment the
|
|
|
121 |
lines about SMLNJ. Also set the variable SMLNJ_CYGWIN_RUNTIME to 1, in order
|
|
|
122 |
the cygwin version of SMLNJ is used. As mentioned above, the path variables
|
|
|
123 |
for the ML system and ProofGeneral may need adjustions, depending on your
|
|
|
124 |
different installation locations.</p>
|
|
|
125 |
|
|
|
126 |
<p>Take heed of the setting of ISABELLE_HOME_USER; by default, this is
|
|
|
127 |
<tt class="shellcmd">~/isabelle</tt>. To detect which Windows path this will be mapped to,
|
|
|
128 |
type into the Cygwin bash shell:</p>
|
|
|
129 |
|
|
|
130 |
<ul class="shellcmd">
|
|
|
131 |
<li>cygpath --windows ~/isabelle</li>
|
|
|
132 |
</ul>
|
|
|
133 |
|
|
|
134 |
<p>If you don't like this location to be the isabelle home
|
|
|
135 |
directory, consider setting of ISABELLE_HOME_USER to another value; use
|
|
|
136 |
<tt class="shellcmd">cygpath --unix <winpath></tt> to detect which Cygwin path a given
|
|
|
137 |
Windows path is mapped to.</p>
|
|
|
138 |
|
|
|
139 |
<p>A typical change could look like this:</p>
|
|
|
140 |
|
|
|
141 |
<blockquote>
|
|
|
142 |
from<br />
|
|
|
143 |
<tt># Standard ML of New Jersey 110 or later<br />
|
|
|
144 |
#ML_SYSTEM=smlnj-110<br />
|
|
|
145 |
#ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
|
|
|
146 |
#ML_OPTIONS="@SMLdebug=/dev/null"<br />
|
|
|
147 |
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
|
|
|
148 |
"$HEAP_SUFFIX")<br /></tt>
|
|
|
149 |
</blockquote>
|
|
|
150 |
|
|
|
151 |
<blockquote>
|
|
|
152 |
to<br />
|
|
|
153 |
<tt># Standard ML of New Jersey 110 or later<br />
|
|
|
154 |
SMLNJ_CYGWIN_RUNTIME=1<br />
|
|
|
155 |
ML_SYSTEM=smlnj-110<br />
|
|
|
156 |
ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
|
|
|
157 |
ML_OPTIONS="@SMLdebug=/dev/null"<br />
|
|
|
158 |
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
|
|
|
159 |
"$HEAP_SUFFIX")</tt>
|
|
|
160 |
</blockquote>
|
|
|
161 |
|
|
|
162 |
<h2>Building logics</h2>
|
|
|
163 |
|
|
|
164 |
<p>Now we can compile some logics. Start the cygwin shell (if not still
|
|
|
165 |
running) and type:</p>
|
|
|
166 |
|
|
|
167 |
<ul class="shellcmd">
|
|
|
168 |
<li>cd /opt/Isabelle</li>
|
|
|
169 |
<li>build HOL</li>
|
|
|
170 |
<li>build ZF</li>
|
|
|
171 |
</ul>
|
|
|
172 |
|
|
|
173 |
<p>The compilation process may take some time (depending on how fast the
|
|
|
174 |
computer is). Before building a logic image the build program shows some
|
|
|
175 |
variables and expects user input – just hit enter.</p>
|
|
|
176 |
|
|
|
177 |
<h2>Running Isabelle with ProofGeneral</h2>
|
|
|
178 |
|
|
|
179 |
<p>On Linux, Isabelle can be started by two scripts located in
|
|
|
180 |
<tt class="shellcmd">Isabelle/bin</tt>: <tt class="shellcmd">Isabelle</tt> and <tt class="shellcmd">isabelle</tt>.
|
|
|
181 |
<tt class="shellcmd">Isabelle</tt> attempts to start ProofGeneral with XEmacs, and isabelle
|
|
|
182 |
starts it in an SML shell session. However Windows treats the two names as
|
|
|
183 |
one. To get around this, just rename <tt class="shellcmd">/opt/Isabelle/bin/isabelle</tt> to
|
|
|
184 |
<tt class="shellcmd">/opt/Isabelle/bin/Isabelle</tt>. This script
|
|
|
185 |
will start Isabelle with ProofGeneral; the <tt class="shellcmd">isabelle</tt>
|
|
|
186 |
script in any case is available as <tt class="shellcmd">isabelle-process</tt>.</p>
|
|
|
187 |
|
|
|
188 |
<p>Now everything should be ready. To test, start the cygwin shell and
|
|
|
189 |
type</p>
|
|
|
190 |
|
|
|
191 |
<ul class="shellcmd">
|
|
|
192 |
<li>startx &</li>
|
|
|
193 |
</ul>
|
|
|
194 |
|
|
|
195 |
<p>This will start the cygwin X server and an X shell window. In
|
|
|
196 |
the X shell window, type</p>
|
|
|
197 |
|
|
|
198 |
<ul class="shellcmd">
|
|
|
199 |
<li>/opt/Isabelle/bin/Isabelle &</li>.
|
|
|
200 |
</ul>
|
|
|
201 |
|
|
|
202 |
<p>This will start the ProofGeneral interface for Isabelle. After a
|
|
|
203 |
while an empty buffer <tt>Scratch.thy</tt> is created. You can turn on
|
|
|
204 |
X-Symbol from the menu Proof-General, item Options.</p>
|
|
|
205 |
|
|
|
206 |
<p>Load one of your favorite theories and test your Isabelle installation by
|
|
|
207 |
proving something.</p>
|
|
|
208 |
|
|
|
209 |
<p>To simplify starting ProofGeneral, consider writing a Windows command
|
|
|
210 |
script, e. g.</p>
|
|
|
211 |
|
|
|
212 |
<blockquote>
|
|
|
213 |
<tt>@bash startx -geometry 30x4 -iconic -e Isabell</tt>
|
|
|
214 |
</blockquote>
|
|
|
215 |
|
|
|
216 |
<p>and assigning a shortcut in the start menu to it.</p>
|
|
|
217 |
|
|
|
218 |
<h2 id="inconvenience">Inconveniencies with the current version of
|
|
|
219 |
Isabelle</h2>
|
|
|
220 |
|
|
|
221 |
<p>With the current Isabelle release (Isabelle 2004), there are two
|
|
|
222 |
inconveniencies:</p>
|
|
|
223 |
|
|
|
224 |
<ul>
|
|
|
225 |
<li>During extraction you will get a warning that file
|
|
|
226 |
<tt class="shellcmd">Real/HahnBanach/Aux.thy</tt> can not be created. This is because
|
|
|
227 |
<tt class="shellcmd">Aux</tt> is not allowed as a filename under Windows. If you do not want
|
|
|
228 |
to run the HahnBanach example, you might simply want to ignore this
|
|
|
229 |
warning.</li>
|
|
|
230 |
|
|
|
231 |
<li>The tool <tt class="shellcmd">isatool mkdir</tt> tries to detect the name of the current
|
|
|
232 |
user, to put it into the generated <tt class="shellcmd">root.tex</tt>. Alas, on Windows,
|
|
|
233 |
this leads to an unquoted <tt>\</tt> in the TeX file. So you either must
|
|
|
234 |
edit your <tt class="shellcmd">root.tex</tt> manually to fix this, or directly patch
|
|
|
235 |
<tt class="shellcmd">/opt/Isabelle/lib/Tools/mkdir</tt> by replacing
|
|
|
236 |
|
|
|
237 |
<blockquote>
|
|
|
238 |
<tt>AUTHOR=$("$AUTO_PERL" -e "@pw = getpwnam(\"$USER\"); print @pw[6]" | tr _ -)</tt>
|
|
|
239 |
</blockquote>with
|
|
|
240 |
|
|
|
241 |
<blockquote>
|
|
|
242 |
<tt>AUTHOR="default author name"</tt>
|
|
|
243 |
</blockquote>
|
|
|
244 |
</li>
|
|
|
245 |
</ul>
|
|
|
246 |
|
|
|
247 |
<p>To get around these inconveniencies, consider using a recent developer
|
|
|
248 |
snapshot of Isabelle; both will be fixed in the next Isabelle release.</p>
|
|
|
249 |
|
|
|
250 |
<h2 id="polyml">A note on Poly/ML</h2>
|
|
|
251 |
|
|
|
252 |
<p>As indicated above, Isabelle does <em>not</em> run neatly with <a href=
|
|
|
253 |
"http://www.polyml.org/">Poly/ML</a> on Windows, since it is not clear
|
|
|
254 |
how Poly/ML has to be compiled for Cygwin, and the native Windows port
|
|
|
255 |
of PolyML does not provide some Posix signals Isabelle/ProofGeneral relies on.</p>
|
|
|
256 |
|
|
|
257 |
<p>If you know how to circumvent (fully or partially) any of these problems,
|
|
|
258 |
please let us know.</p>
|
|
|
259 |
|
|
|
260 |
</div>
|
|
|
261 |
<div class="hr"><hr/></div>
|
|
|
262 |
<?include file="//include/footer.include.html"?>
|
|
|
263 |
</body>
|
|
|
264 |
|
|
|
265 |
</html>
|