function-package: Changed record usage to make sml/nj happy...
<?xml version='1.0' encoding='iso-8859-1' ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<!-- $Id$ -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Installation notes for Windows/Cygwin</title>
<?include file="//include/htmlheader.include.html"?>
</head>
<body class="dist">
<?include file="//include/header.include.html"?>
<div class="hr"><hr/></div>
<?include file="//include/navigation.include.html"?>
<div class="hr"><hr/></div>
<div id="content">
<h2>Preconditions and restrictions</h2>
<p>Please notice before you go ahead:</p>
<ul>
<li>The ML system these notes apply to is <a href=
"http://www.smlnj.org/">Standard ML of New Jersey</a>, which
provides explicit Cygwin support. Poly/ML is not covered
here.</li>
<li>It is assumed you have some experience with an Unix
operating system (e.g. what a shell is for and how to use
it).</li>
</ul>
<p>Any suggestions and improvements concerning this hints are welcomed!</p>
<h2>Acknowlegements</h2>
<p>Thanks to <a href=
"http://cswww.essex.ac.uk/Research/FSS/projects/isawin/">Norbert
Völker</a> and <a href=
"http://www.abo.fi/~viorel.preoteasa/isabelle/">Viorel Preoteasa</a> whose
efforts helped a lot to get Isabelle run this way.</p>
<h2>Installing Cygwin</h2>
<p>Cygwin is a POSIX emulation layer for Windows; it contains ports of a
large collection of common Unix software (shells, perl, gcc, X11, latex,
ImageMagick, …).</p>
<p>To install it, get the installer from the <a href=
"http://www.cygwin.com">Cygwin website</a> and run it. It will ask you which
packages to install, and then downloads and installs them. Please make sure
you install everything needed by Isabelle; it is hard to give a concise list
of packages here since the bundling of Cygwin packages may vary over time,
but installing the base packages, perl, make, xemacs and x-server should be a
good choice for the beginning.</p>
<p>By default, cygwin installs to <tt class="shellcmd">c:\cygwin</tt>; you may choose an
arbitrary location, but it is recommended that it does not include any space
or exotic characters. This directory will then become the root directory of
the Cygwin filesystem tree, i.e. the Cygwin path <tt class="shellcmd">/opt/smlnj</tt> will be
mapped to Windows path <tt class="shellcmd">c:\cygwin\opt\smlnj</tt>.</p>
<p>After installation, open a Cygwin shell window (normally the installer
makes a shortcut for you).</p>
<h2>Getting and building SML/NJ</h2>
<p>Now we are ready to get and build <a href=
"http://www.smlnj.org/">SML/NJ</a>; before this, set the environment variable
SMLNJ_CYGWIN_RUNTIME to 1:</p>
<ul class="shellcmd">
<li>export SMLNJ_CYGWIN_RUNTIME=1</li>
</ul>
<p>This setting will tell the build process that it should
<em>not</em> attempt to build SML/NJ natively for Win32 but for Cygwin
instead (see further <a href=
"http://smlnj.cs.uchicago.edu/dist/working/110.53/CYGWININSTALL">CYGWININSTALL</a>).</p>
<p>So far, this setup was tested using the working version 110.53 of SML/NJ
from <a href=
"http://smlnj.cs.uchicago.edu/dist/working/110.53/">http://smlnj.cs.uchicago.edu/dist/working/110.53/</a>.
SML/NJ provides a nice installer enabling you to download and build it. Read
<a href=
"http://smlnj.cs.uchicago.edu/dist/working/110.53/INSTALL">INSTALL</a> to
learn about the different possibilites to do this. The default packages
should be sufficient.</p>
<p>In the following, it is assumed that you install SML/NJ to Cygwin path
<tt class="shellcmd">/opt/smlnj</tt>; if you choose an other location, some tweaking in the
<a href="#config"><tt class="shellcmd">etc/settings</tt> file</a> may be neccessary later.</p>
<p>Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable must
be set to 1 (later on a convenient mechanism to make this the default is
proposed).</p>
<h2>Installing Isabelle</h2>
<p><a href="download.html">Download</a> the latest Isabelle and
ProofGeneral release packages. Assuming that you are in the
directory where you downloaded the files, install them into <tt
class="shellcmd">/opt</tt> by typing into the bash shell:</p>
<ul class="shellcmd">
<li>tar -C /usr/opt -xvzf <?value key="distname"?>.tar.gz</li>
<li>tar -C /usr/opt -xvzf ProofGeneral.tar.gz</li>
</ul>
<p>The location <tt class="shellcmd">/opt</tt> again is just a proposal; if you choose other
locations, some tweaking in the <a href="#config"><tt class="shellcmd">etc/settings</tt>
file</a> may be neccessary later.</p>
<h2 id="config">Configuring Isabelle</h2>
<p>Edit the file <tt class="shellcmd">/opt/Isabelle/etc/settings</tt>; first, uncomment the
lines about SMLNJ. Also set the variable SMLNJ_CYGWIN_RUNTIME to 1, in order
the cygwin version of SMLNJ is used. As mentioned above, the path variables
for the ML system and ProofGeneral may need adjustions, depending on your
different installation locations.</p>
<p>Take heed of the setting of ISABELLE_HOME_USER; by default, this is
<tt class="shellcmd">~/isabelle</tt>. To detect which Windows path this will be mapped to,
type into the Cygwin bash shell:</p>
<ul class="shellcmd">
<li>cygpath --windows ~/isabelle</li>
</ul>
<p>If you don't like this location to be the isabelle home
directory, consider setting of ISABELLE_HOME_USER to another value; use
<tt class="shellcmd">cygpath --unix <winpath></tt> to detect which Cygwin path a given
Windows path is mapped to.</p>
<p>A typical change could look like this:</p>
<blockquote>
from<br />
<tt># Standard ML of New Jersey 110 or later<br />
#ML_SYSTEM=smlnj-110<br />
#ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
#ML_OPTIONS="@SMLdebug=/dev/null"<br />
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
"$HEAP_SUFFIX")<br /></tt>
</blockquote>
<blockquote>
to<br />
<tt># Standard ML of New Jersey 110 or later<br />
SMLNJ_CYGWIN_RUNTIME=1<br />
ML_SYSTEM=smlnj-110<br />
ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
ML_OPTIONS="@SMLdebug=/dev/null"<br />
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
"$HEAP_SUFFIX")</tt>
</blockquote>
<h2>Building logics</h2>
<p>Now we can compile some logics. Start the cygwin shell (if not still
running) and type:</p>
<ul class="shellcmd">
<li>cd /opt/Isabelle</li>
<li>build FOL</li>
<li>build ZF</li>
<li>build HOL</li>
</ul>
<p>The compilation process may take some time (depending on how fast the
computer is). Before building a logic image the build program shows some
variables and expects user input – just hit enter.</p>
<h2>Running Isabelle with ProofGeneral</h2>
<p>Now everything should be ready. To test, start the cygwin shell and
type</p>
<ul class="shellcmd">
<li>startx &</li>
</ul>
<p>This will start the cygwin X server and an X shell window. In
the X shell window, type</p>
<ul class="shellcmd">
<li>/opt/Isabelle/bin/Isabelle &</li>.
</ul>
<p>This will start the ProofGeneral interface for Isabelle. After a
while an empty buffer <tt>Scratch.thy</tt> is created. You can turn on
X-Symbol from the menu Proof-General, item Options.</p>
<p>Load one of your favorite theories and test your Isabelle installation by
proving something.</p>
<p>To simplify starting ProofGeneral, consider writing a Windows command
script, e. g.</p>
<blockquote>
<tt>@bash startx -geometry 30x4 -iconic -e Isabelle</tt>
</blockquote>
<p>and assigning a shortcut in the start menu to it.</p>
</div>
<div class="hr"><hr/></div>
<?include file="//include/footer.include.html"?>
</body>
</html>