Isabelle supports the three main platform families: Linux, Mac OS X (Leopard or Snow Leopard), and Windows (via Cygwin). The main Isabelle bundle already includes pre-compiled logic images and add-on tools for convenience, with a few external requirements as explained below.

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 Isabelle 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 usually incomplete and outdated.




The bundled archive contains almost everything required for Isabelle on Linux. It can be unpacked into an arbitrary directory like this:

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

This often fails due to a bad version of Emacs. The command line option -p specifies an explicit Emacs executable, e.g. like this:

The important Unicode token mode requires a suitable font with mathematical symbols (e.g. IsabelleText in Isabelle2011/lib/fonts). Assuming that the font has been installed properly on the system it can be enabled via Emacs option menus, or on the command line:

Mac OS X (10.5 or 10.6)



The above disk image contains an application bundle with everything required for Isabelle on Intel Macs. It can be placed into the /Applications folder and started as usual. The included GNU Emacs 23 supports Unicode symbols via the STIXGeneral font, which is installed automatically in the user's Library/Fonts folder on application startup.

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

Windows (Cygwin)



The bundled archive contains everything required for Isabelle on Cygwin. It can be unpacked into an arbitrary directory as follows. 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:

Sometimes Cygwin executables produce strange runtime exceptions and stack dumps. Often this can be amended via rebaseall as explained in the Cygwin/X FAQ, for example.