Isabelle runs on common Unix platforms and Windows with Cygwin. We provide ready-to-use binary packages for the most common platforms.

A practically usable Isabelle system consists of the following components:

Optional extensions:

See below for further system-specific instructions. For more exotic platforms Isabelle needs to be compiled manually, see also INSTALL.


Installation of Isabelle/HOL on Linux (x86 and x86_64) works by downloading and unpacking the relevant packages. Here 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:

Failure on this is typically a problem with bad Emacs versions; the command line option -p specifies a different Emacs executable:

The X-Symbol package is already included in Proof General, but needs to be enabled separately; use the -x command line option, or the Options menu.

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

The above x86 binaries may be also used for 64bit Linux, but are restricted to 32bit mode; native x86_64 platform support requires manual compilation of Isabelle.

Warning: Pre-packaged versions of Isabelle, Proof General, and Poly/ML floating through the Net as deb, rpm, port etc. are often outdated and rarely work as advertized. Even XEmacs is better compiled manually these days -- the packages provided for SuSE, Ubuntu, and Debian are mostly broken.

Mac OS X (Darwin)

Isabelle works on Mac OS X 10.4 (Tiger) and 10.5 (Leopard) and requires the following preliminaries:

Then installation on Mac OS X is analogous to Linux, the following is for Intel Macs:

The same works for PowerPC Macs, by replacing x86 by ppc above.

Windows (Cygwin)

Isabelle also works on Windows thanks to the excellent Posix API emulation of Cygwin. After downloading and running setup.exe, the following Cygwin packages need to be installed:

Both of the above XEmacs packages are needed! Some further requirements (such as X11) are resolved via these as well.

Now installation on Cygwin is analogous to Linux. The following should be executed within the Cygwin shell:

After startx Proof General can be run from an xterm window like this:

Further Cygwin packages will be required for a fully operational Isabelle installation, most notably tetex. Note that Java is a native Windows application -- make sure that the Cygwin shell is able to find it in its PATH.