Isabelle on Windows/Cygwin
Before you start
These notes show how to get a
restricted version of Isabelle working on Windows machines using the
Cygwin Unix emulation package. It is
assumed that users are familiar with Cygwin (or similar Unix shells) and the components of
a standard Isabelle environment, ie. Isabelle, SML, (X)Emacs and ProofGeneral.
Tried on Windows 2000 and Windows XP Professional with
- Isabelle 2005,
- Standard ML of New Jersey
version 110.53 (Cygwin),
- ProofGeneral 3.6pre051004,
- XEmacs 21.4.13 (Cygwin, non Mule).
I have installed Isabelle on my machine in the directory /cygdrive/c/thp/Isabelle.
Please change Isabelle related paths in the instructions below according to where
Isabelle is on your machine.
- Install Cygwin. Make sure
to include at least the whole base package as well as make and perl.
You will also need at least the default selections in the Graphics package.
- Install the Cygwin version of
(NOT the Windows version). Do not forget to set the environment
variable SMLNJ_CYGWIN_RUNTIME to 1. You can do this for example
in your Cygwin shell initialisation file (i.e. ~/.bashrc or equivalent).
- Download and unpack
- Adjust file /cygdrive/c/thp/Isabelle/etc/settings.
Uncomment the section dealing with SML/NJ and set ML_HOME
appropriately, for example: ML_HOME="/cygdrive/c/thp/smlnj/bin". You
might also want to adjust ISABELLE_HOME_USER.
- Build object logics as usual by changing to the Isabelle directory
and calling ./build XYZ where XYZ
is the name of the object logic.
You can also build targets, for example:
./build -m HOL-Complex.
- Install the Cygwin version of
Note that this might also require installing some additional Cygwin packages.
- Download and unpack a recent version
Find your XEmacs intialization file init.el
which is by default located in directory ~/.xemacs.
Insert in file init.el the equivalent of:
(setq proof-site-file "/cygdrive/c/thp/ProofGeneral/generic/proof-site.el")
- Start XEmacs and load an Isabelle theory file.
When ProofGeneral comes up for the
first time, you need to navigate to the file
/cygdrive/c/thp/Isabelle/bin/isatool when prompted.
- Customize PG so that the Isatool and Isabelle program
names point to the right files in the Isabelle bin directory.
Do not forget to save these settings. The menu is:
ProofGeneral -> Advanced -> Customize -> Isabelle -> (Isa Isatool Command/ Program Name).
You might want to check the file custom.el
for the customized variable settings. On my machine, they are:
ProofGeneral can display special Isabelle symbols with the
help of X-Symbol. Unfortunately, the native Windows display of
XEmacs/Cygwin does not work with
the Unix fonts
included in the X-Symbol package.
Warnings and Remarks
- Avoid blanks and special characters
in the name of the Isabelle and SML/NJ home directories.
Use absolute cygwin paths when navigating to the Isabelle build directory.
Cygwin symbolic links are ok as long as you restrict yourself to tools that understand them.
- If you are getting strange error messages "(.../etc/settings: Line 7: command not found") when running the build script, this indicates binary mode/text mode file problems.
This can be caused by older versions of Winzip, and you can try unpacking the archive with the Cygwin tar tool instead. If this does not work, apply "conv --dos2unix" to the offending script files.
- I have not tried the Isabelle document generation tools on Windows. See the page by
Viorel Preoteasa for information
- It is recommended to start XEmacs-Cygwin consistently from Cygwin shell. Starting it
outside of a shell (i.e. by clicking on its icon in the desktop) might result in XEmacs looking
for its initialization files in a different place, because your "Windows home directory" setting
(where the Windows Command Shell starts off) might be different from your "Cygwin
home directory" setting (typically /home/userName) .
- When loading files in XEmacs, make sure you are specifying files via Unix-style paths.
- There seem to be problems with certain XEmacs/PG combinations, for example
XEmacs 21.4.17 (Mule, Cygwin)
does not work with PG 3.6pre050325 (Error message "Wrong type argument: stringp, nil"
when trying to start Isabelle).
- It should also be possible to start PG via the
/cygdrive/c/thp/Isabelle/bin/Isabelle script. Be careful that this does not pick
up the wrong XEmacs if you have several versions on
- If you encounter problems with disabled toolbar buttons, try toggling
the toolbar enabler, see ProofGeneral user options.
- If you have network access to Isabelle running on a remote Unix machine,
you can make the user interface available on your Windows desktop, either by
- getting a local PG to connect to the remote Isabelle process (see PG manual) or
- displaying a remote PG on your desktop by running an X-server locally (requires a fast network).
provides a fully functioning Isabelle environment without requiring
a permanent GNU/Linux installation.
Please contact me if you have comments, in particular suggestions
Norbert Völker, 13 May 2007.
This is a University of Essex, Department
of Computer Science page.