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.

Versions

Tried on Windows 2000 and Windows XP Professional with

Building Isabelle

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.
  1. 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.
  2. Install the Cygwin version of SML/NJ (110.53) (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).
  3. Download and unpack Isabelle.
  4. 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.
  5. 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.

ProofGeneral

  1. Install the Cygwin version of XEmacs 21.4.13. Note that this might also require installing some additional Cygwin packages.
  2. Download and unpack a recent version of ProofGeneral. 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")
    (load proof-site-file)
  3. 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.
  4. 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:
    (custom-set-variables...
    '(isabelle-program-name "/cygdrive/c/thp/Isabelle/bin/isabelle")
    '(isa-isatool-command "/cygdrive/c/thp/Isabelle/bin/isatool"))

X-Symbol

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 xsymb0 and xsymb1 included in the X-Symbol package.

Warnings and Remarks

Isabelle Build
  1. 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.
  2. 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.
  3. I have not tried the Isabelle document generation tools on Windows. See the page by Viorel Preoteasa for information on this.
ProofGeneral
  1. 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) .
  2. When loading files in XEmacs, make sure you are specifying files via Unix-style paths.
  3. 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).
  4. 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 your machine.
  5. If you encounter problems with disabled toolbar buttons, try toggling the toolbar enabler, see ProofGeneral user options.

Alternatives

  1. 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
  2. IsaMorph provides a fully functioning Isabelle environment without requiring a permanent GNU/Linux installation.

Please contact me if you have comments, in particular suggestions for improvements.

Norbert Völker, 13 May 2007.
Created with Emacs Valid HTML 4.0!
This is a University of Essex, Department of Computer Science page.