General

Isabelle supports the three main platform families: Linux, Windows, Mac OS X. The platform-specific Isabelle bundles already include the main add-on components. A few extra dependencies are explained below.

The raw Isabelle distribution archives are available for completeness, but assembling them by hand is not recommended! Past releases are available from the archive.

Warning: Pre-packaged versions of Isabelle and some add-on components that are floating through the Net as deb, rpm, port etc. are usually incomplete and outdated!

Linux

Requirements

Installation

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

Note that the target directory needs to be writable when Isabelle is started for the first time, to build the required logic image.

The Isabelle/jEdit Prover IDE can be invoked like this:

or explicitly:

Alternatively, it is possible to start Isabelle Proof General 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:

Isabelle logic images may be built explicitly like this:

Note that Isabelle/jEdit automatically builds its selected logic image on startup.

Windows

Requirements

Installation

The self-extracting archive contains everything required for Isabelle on Windows. It is unpacked to the user's desktop and can be moved to an arbitrary place later. Note that the target directory needs to be writable when Isabelle is started for the first time, to build the required logic image.

There is a desktop alias to the main Isabelle2013 executable that starts the Isabelle/jEdit Prover IDE.

Cygwin-Latex-Setup augments the Cygwin installation of Isabelle by major parts of TeX live, as required for typical applications of the Isabelle document preparation system.

Cygwin-Setup allows to modify the Cygwin installation of Isabelle, e.g. to add further packages manually.

Cygwin-Terminal allows to run command-line tools of Isabelle, as known from Unix.

Mac OS X (10.8, 10.7, partly 10.6)

Requirements

Installation

The above disk image contains an application bundle with everything required for Isabelle recent Macs (64-bit). The Isabelle application can be placed into the /Applications folder and started as usual. Note that the target directory needs to be writable when Isabelle is started for the first time, to build the required logic image.

The main Isabelle distribution is hidden inside the Isabelle2013.app folder. This is relevant when building logic images manually, e.g. like this in the Terminal application:

Note that Isabelle/jEdit automatically builds its selected logic image on startup.