General

Isabelle runs on common Unix systems (such as Linux or Mac OS), and Windows with Cygwin. Our packages include multi-platform binaries for a broad range of architectures. Pre-compiled logic images are available for download for the most common platforms.

A realistic Isabelle installation consists of the following parts:

See below for further system-specific instructions. For more exotic platforms Isabelle logics need to be compiled manually using the Isabelle/build script. This might also require editing of Isabelle/etc/settings, e.g. to enable native 64bit mode on x86_64 platforms (this is only useful with more than 8GB of memory and more than 4 cores).

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

Linux

Installation of Isabelle/HOL on Linux (x86 and x86_64) works by downloading and unpacking the relevant packages. The Isabelle "bundle" already includes most required components. In the subsequent example the installation location is /usr/local, but any other directory works as well:

Normally, the default settings of Isabelle should be sufficient for invoking Isabelle Proof General like this:

This often fails due to bad versions of Emacs; the command line option -p specifies a different Emacs executable:

The all-important X-Symbol package is already included in Proof General, but needs to be enabled separately: use the command line option -x true, or the Options menu in Proof General. X-Symbol mode is known to work with most variants of GNU Emacs 22.

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 (Darwin)

Isabelle works well on Mac OS X 10.5 (Leopard), and 10.6 (Snow Leopard). Manual installation is analogous to Linux above and works via the Terminal application.

It is more convenient to use the following disk image that contains an application bundle with everything required for Isabelle on Intel Macs:

Isabelle.dmg.zip 235.7 MB

The Isabelle.app bundle can be 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 Isabelle.app directory. This is relevant when building further images, e.g. like this in the Terminal application:

Rebuilding logic images is also required for native x86_64 and old ppc.

Windows (Cygwin)

Isabelle also works on Windows thanks to the excellent Posix API emulation of Cygwin. This provides half of a Linux/GNU operating system to be run inside Windows. Alternatively, one can install a full Linux system on the Windows partition via Wubi, and then run natively without Windows.

Cygwin installation works by executing running setup.exe (version 1.7). Isabelle requires the following Cygwin packages:

Note that this selection has been carefully chosen in order to pull in a much larger collection via implicit dependencies. Now installation on Cygwin is analogous to Linux. The following should be executed within the Cygwin shell:

After executing startxwin.sh Proof General can be run from an xterm window like this: