Preconditions and restrictions

Please notice before you go ahead:

Any suggestions and improvements concerning this hints are welcomed!

Acknowlegements

Thanks to Norbert Völker and Viorel Preoteasa whose efforts helped a lot to get Isabelle run this way.

Installing Cygwin

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, …).

To install it, get the installer from the Cygwin website 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.

By default, cygwin installs to c:\cygwin; 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 /opt/smlnj will be mapped to Windows path c:\cygwin\opt\smlnj.

After installation, open a Cygwin shell window (normally the installer makes a shortcut for you).

Getting and building SML/NJ

Now we are ready to get and build SML/NJ; before this, set the environment variable SMLNJ_CYGWIN_RUNTIME to 1:

This setting will tell the build process that it should not attempt to build SML/NJ natively for Win32 but for Cygwin instead (see further CYGWININSTALL).

So far, this setup was tested using the working version 110.53 of SML/NJ from http://smlnj.cs.uchicago.edu/dist/working/110.53/. SML/NJ provides a nice installer enabling you to download and build it. Read INSTALL to learn about the different possibilites to do this. The default packages should be sufficient.

In the following, it is assumed that you install SML/NJ to Cygwin path /opt/smlnj; if you choose an other location, some tweaking in the etc/settings file may be neccessary later.

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).

Installing Isabelle

Download the latest Isabelle and ProofGeneral release packages. Assuming that you are in the directory where you downloaded the files, install them into /opt by typing into the bash shell:

The location /opt again is just a proposal; if you choose other locations, some tweaking in the etc/settings file may be neccessary later.

Configuring Isabelle

Edit the file /opt/Isabelle/etc/settings; 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.

Take heed of the setting of ISABELLE_HOME_USER; by default, this is ~/isabelle. To detect which Windows path this will be mapped to, type into the Cygwin bash shell:

If you don't like this location to be the isabelle home directory, consider setting of ISABELLE_HOME_USER to another value; use cygpath --unix <winpath> to detect which Cygwin path a given Windows path is mapped to.

A typical change could look like this:

from
# Standard ML of New Jersey 110 or later
#ML_SYSTEM=smlnj-110
#ML_HOME="$ISABELLE_HOME/../smlnj/bin"
#ML_OPTIONS="@SMLdebug=/dev/null"
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
to
# Standard ML of New Jersey 110 or later
SMLNJ_CYGWIN_RUNTIME=1
ML_SYSTEM=smlnj-110
ML_HOME="$ISABELLE_HOME/../smlnj/bin"
ML_OPTIONS="@SMLdebug=/dev/null"
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")

Building logics

Now we can compile some logics. Start the cygwin shell (if not still running) and type:

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.

Running Isabelle with ProofGeneral

On Linux, Isabelle can be started by two scripts located in Isabelle/bin: Isabelle and isabelle. Isabelle attempts to start ProofGeneral with XEmacs, and isabelle starts it in an SML shell session. However Windows treats the two names as one. To get around this, just rename /opt/Isabelle/bin/isabelle to /opt/Isabelle/bin/Isabelle. This script will start Isabelle with ProofGeneral; the isabelle script in any case is available as isabelle-process.

Now everything should be ready. To test, start the cygwin shell and type

This will start the cygwin X server and an X shell window. In the X shell window, type

This will start the ProofGeneral interface for Isabelle. After a while an empty buffer Scratch.thy is created. You can turn on X-Symbol from the menu Proof-General, item Options.

Load one of your favorite theories and test your Isabelle installation by proving something.

To simplify starting ProofGeneral, consider writing a Windows command script, e. g.

@bash startx -geometry 30x4 -iconic -e Isabell

and assigning a shortcut in the start menu to it.

A note on Poly/ML

As indicated above, Isabelle does not run neatly with Poly/ML on Windows, since it is not clear how Poly/ML has to be compiled for Cygwin, and the native Windows port of PolyML does not provide some Posix signals Isabelle/ProofGeneral relies on.

If you know how to circumvent (fully or partially) any of these problems, please let us know.