General

Isabelle runs on common Unix systems (such as Linux or Mac OS), 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.

Linux

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

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 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):

The above x86 binaries also work 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 well on Mac OS X 10.4 (Tiger) and 10.5 (Leopard), although there are several installation options.

Option 1: Application bundle

The following disk image contains an application bundle (universal binary) with everything required for Isabelle/HOL:

Isabelle.dmg.gz 138.4 MB

The Isabelle.app bundle can be placed into the /Applications directory and started as usual. The included Emacs version is native on Mac OS, which means old-style X-Symbol mode does not work, but Unicode Tokens are available via the Options menu in Proof General.

Note that the main Isabelle distribution is hidden inside the app, which is relevant when installing further images. E.g. like this via the Terminal application:

Option 2: Manual installation with native Emacs

Manual installation is analogous to Linux and works via the Terminal application. The following example is for Intel Macs:

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

At that point, Isabelle can already be run in text mode, e.g. like this (using CTRL-D to exit):

or by using the text mode Emacs provided by Apple:

A more realistic working Isabelle environment can be based on Carbon Emacs, which merely needs to be placed into the /Applications directory and is then invoked from the terminal like this:

Aquamacs Emacs works as well, but the spaces within the file name /Applications/Aquamacs Emacs.app/Contents/MacOS/Aquamacs Emacs need to be eliminated first, by renaming this directory and file name manually.

Option 3: Manual installation with XEmacs

This alternative, more classic installation, requires the following preliminaries:

After compiling the all required parts of MacPorts, and unpacking the Isabelle tar.gz packages as for option 2 above, Isabelle Proof General can be invoked like this:

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:

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:

The regular Java distribution for Windows should also work as expected, even though it is not native on Cygwin.