General

Isabelle supports the three main platform families: Linux, Windows, macOS. The platform-specific application bundles include sources, documentation, and add-on components. A few extra dependencies are explained below. There is also a self-contained Docker image (without GUI support).

Individual Isabelle distribution files are available for reference: in practice it is sufficient to download the main "apps" below. Past releases are available from the distribution archive. Further technical background information may be found in the Isabelle System Manual.

Docker: Headless Ubuntu Linux

Requirements

Installation

The Docker image contains Ubuntu Linux 22.04 with Isabelle2024. It can be used, e.g. on another Linux host like this:

That provides command-line access to the regular isabelle tool wrapper, with indirection through the Docker container infrastructure.

The default platform is Intel x86_64, but ARM is supported as well (e.g. for Apple M1):

Linux

Requirements

Installation

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

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

Other Isabelle command-line tools can be invoked from the terminal like this:

Windows (10, 11)

Requirements

Installation

The self-extracting archive contains everything required for Isabelle on Windows PCs. It can be unpacked into an arbitrary directory. The installer starts the Isabelle/jEdit Prover IDE automatically for the first time. It also creates a desktop alias to the main executable for later use.

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

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

Note: The Isabelle application lacks developer signatures and certificates, so Microsoft rejects it by default. Running it for the first time requires some careful clicks in the proper spots.

Note: The Windows 10 Defender may prevent external provers from working properly (e.g. for sledgehammer or the smt proof method). In that case the whole Isabelle application directory should be excluded from Virus & threat protection.

macOS (11, 12, 13, 14 — Intel or Apple Silicon)

Requirements

Installation

The bundled archive contains everything required for Isabelle on Macintosh computers. The Isabelle application can be placed into the /Applications folder and started as usual.

Note: The Isabelle application lacks developer signatures and certificates, so Apple rejects it by default. See also the document Safely open apps on your Mac, notably the last section "How to open an app that hasn’t been notarized or is from an unidentified developer". In short, it should work with the default security settings as follows:

  1. Open Isabelle2024.app and Cancel the subsequent security dialog.
  2. Open Security & Privacy in system preferences: section "Allow apps ..." at the bottom should list the blocked application (see screenshot).
  3. Click Open Anyway and provide further confirmations as required.