Please notice before you go ahead: +
Thanks to +Norbert Vöker +and Viorel Preoteasa +whose efforts helped a lot to get Isabelle run this way.
+ +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).
+ +Now we are ready to get and build SML/NJ; +before this, set the environment variable SMLNJ_CYGWIN_RUNTIME to 1: + +
+ + export SMLNJ_CYGWIN_RUNTIME=1 + ++ +
+ (or + + setenv SMLNJ_CYGWIN_RUNTIME 1 + + for c shells). ++ +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 whole setup was tested using the latest 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 (lateron a convenient mechanism to make this the default +is proposed).
+ +Download the latest Isabelle and ProofGeneral release packages from +http://isabelle.in.tum.de/dist/packages.html. +Assuming that you are in the directory where +you downloaded the files, install them into /opt by typing into the +bash shell: + +
+ + tar -C /usr/opt -xvzf Isabelle2004.tar.gz+ +During extracting, one inconvenience may occur, see below. + +
+ tar -C /usr/opt -xvzf ProofGeneral-3.5.tar.gz + +
The location /opt again is just a proposal; if you choose other +locations, some tweaking in the etc/settings file +may be neccessary later.
+ +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 to which Windows path this will be mapped, +type into the Cygwin bash shell: + +
+ + cygpath --windows ~/isabelle + ++ +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") + +
Now we can compile some logics. Start the cygwin shell (if not still +running) and type: + +
+ + cd /opt/Isabelle+ + +
+ build HOL
+ build ZF + +
The compilation process may take quite a lot of time (depending also on +how fast the computer is). When starting building some logic the build +program shows some variables and expects the user input – just hit enter. + +
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 copy +/opt/Isabelle/bin/isabelle to /opt/Isabelle/bin/Isabell. +The script /opt/Isabelle/bin/Isabell will start Isabelle with ProofGeneral.
+ +How everything is ready to test some theory. Start the cygwin shell +(if not already running) and type + +
+ startx & ++ +This will start the cygwin X server and an X shell window. In the X shell window, +type + +
+ /opt/Isabelle/bin/Isabell &. ++ +This will start the ProofGeneral interface for Isabelle. After a while an empty buffer +scratch.thy is created. You can turn on X-Symbol and Electric Terminator +from the menu Proof-General &rarrow; Options. + +
Load one of your favorite theory 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. + +
With the current Isabelle release (Isabelle 2004), there are two inconveniencies: +
+ + AUTHOR=$("$AUTO_PERL" -e "@pw = getpwnam(\"$USER\"); print @pw[6]" | tr _ -) + ++ + with + +
+ + AUTHOR="default author name" + ++ +
To get around both inconveniencies, consider using a recent developer snapshot +of Isabelle; either, both inconveniencies won't be alive anymore in the next +Isabelle release.
+ +As indicated above, Isabelle does not run +neatlessly with Poly/ML on Windows, due to two +reasons: +
If you know how to circumvent (fully or partially) any of these problems, +please let us know.
+ diff -r 7f3ccb84e60d -r eb92bebb925e Admin/page/dist-content/packages.content --- a/Admin/page/dist-content/packages.content Fri May 06 11:33:19 2005 +0200 +++ b/Admin/page/dist-content/packages.content Fri May 06 15:00:08 2005 +0200 @@ -7,7 +7,7 @@ The following source and binary packages of provide everything required for easy installation of the full Isabelle -working environment on common Unix platforms. +working environment on common Unix platforms (e. g. Linux, Darwin, Solaris)@@ -128,16 +128,12 @@ Proof General FAQ for advice. -
For a complete system, we recommend to run some recent version of +Solaris, Darwin, or Linux.
-- -For a complete system we recommend to run some recent version of -Solaris, Darwin, or Linux. - -
+
Though not »officially supported«, Isabelle in most +cases should also run on Windows, using the +Cygwin POSIX emulation layer. Here +some notes about it.