General

Isabelle supports the three main platform families: Linux, Mac OS X (Leopard or Snow Leopard), and Windows (via Cygwin). Apart from the main Isabelle bundle that already includes various pre-compiled logic images and add-on tools for convenience, there are a few external requirements:

See below for further platform-specific instructions. Both the x86 and x86_64 variants are supported routinely, but x86 is the default. Note that native x86_64 is only useful with 6GB of physical memory, or more.

The raw source package is available here, but assembling a proper distribution from it is quite involved. Past releases are available from the archive. An arbitrary repository snapshot of Isabelle is also available (not for production use).

Warning: Pre-packaged versions of Isabelle, Poly/ML, and Proof General floating through the Net as deb, rpm, port etc. are often outdated and rarely work as advertised.

Linux

Isabelle2009-2_bundle_x86-linux.tar.gz 247.0 MB

The above archive contains almost everything required for Isabelle on Linux. It can be unpacked into an arbitrary directory, which is /usr/local in the subsequent example:

In principle, invoking Isabelle Proof General now works like this:

This often fails due to a bad version of Emacs. The included Proof General 3.7.1.1 interface requires GNU Emacs 22 or XEmacs 21.4.x. Note that GNU Emacs 23 does not work with this version of Proof General. The command line option -p specifies a different Emacs executable, e.g. like this:

The important X-Symbol mode of Proof General needs to be enabled separately: use the command line option -x true, or the Options menu in Proof General.

If all fails, Isabelle may also be run without Proof General, via the plain TTY interface as follows (using CTRL-D to exit):

Mac OS X (10.5 or 10.6)

Isabelle2009-2.dmg 311.6 MB

This disk image contains an application bundle with everything required for Isabelle on Intel Macs. It can placed into the /Applications directory and started as usual. The included Emacs is native on Mac OS, and supports X-Symbol mode via some special TrueType fonts that are installed automatically in the user's fonts directory on startup.

Note that the main Isabelle distribution is hidden inside the Isabelle2009-2.app directory. This is relevant when building further images, e.g. like this in the Terminal application:

See MacTeX for LaTeX-based Isabelle document preparation.

Mac OS X already includes Java 1.6 by default, but it may have to be activated manually using the Java configuration utility provided by Apple.

Windows (Cygwin)

Isabelle2009-2_bundle_x86-cygwin.tar.gz 246.9 MB

Isabelle requires Cygwin (version 1.7.x) in order to turn Windows into a system conforming to common Posix/GNU standards. Alternatively, one can install a full Linux/GNU system on the Windows partition via Wubi, and then run natively without Windows, see Linux above.

Cygwin installation works by executing setup.exe. The following Cygwin packages are required:

Note that this selection has been carefully chosen in order to pull in a much larger collection via implicit dependencies. The remaining installation is analogous to Linux.

The main Isabelle bundle above contains everything required for Isabelle on Cygwin. It can be unpacked into an arbitrary directory, which is /usr/local in the subsequent example, but any Windows path like 'C:\Users\Joe\Desktop' works as well. Note that the tar/gzip of Cygwin needs to be used here, not an archiving tools for Windows!

After executing startxwin from the Cygwin command line, Proof General can be run from an xterm window like this: It is also possible to use xemacs with native Windows GUI, but that does not support X-Symbol mode.