General

Isabelle supports the three main platform families: Linux, Mac OS X, and Windows. The main Isabelle bundles already include pre-compiled logic images and add-on tools for convenience, with a few external requirements as explained below.

The raw Isabelle distribution archives are available here, but assembling them by hand is not recommended! 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!

Linux

Requirements

Installation

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. STIXGeneral). Assuming that the font has been installed properly on the system it can be enabled via Emacs option menus, for example.

Instead of Proof General / Emacs, the new Prover IDE based on Isabelle/Scala and jEdit can be invoked like this:

Mac OS X (10.5, 10.6, 10.7)

Requirements

Installation

The above disk image contains an application bundle with everything required for Isabelle on Intel Macs, both for classic Proof General or the new Isabelle/jEdit Prover IDE. The Isabelle application can be placed into the /Applications folder and started as usual.

The included GNU Emacs 23 for Proof General 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 Isabelle2012.app folder. This is relevant when building further logic images, e.g. like this in the Terminal application:

Windows (with Cygwin)

Requirements

Installation

The self-extracting archive contains everything required for Isabelle on Windows. It can be unpacked into an arbitrary directory, which reveals an Isabelle executable that starts the Isabelle/jEdit Prover IDE.

Cygwin-Terminal allows to run command-line tools of Isabelle, e.g. to build further logic images within the Isabelle2012 directory like this:

Cygwin-Setup allows to modify the Cygwin installation that is bundled with Isabelle. For example, the tetex-extra package may be installed; this is required for the Isabelle document preparation system.

Running classic Proof General / Emacs is also possible; it requires the following additional Cygwin packages:

After executing startxwin from the Cygwin terminal, Proof General 3.7.1.1 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.