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