What is Isabelle?
Isabelle is a generic proof assistant. It allows mathematical
formulas to be expressed in a formal language and provides tools
for proving those formulas in a logical calculus. Isabelle was
originally developed at
the University
of Cambridge and Technische
Universität München, but now includes numerous
contributions from institutions and individuals worldwide. See
the Isabelle overview for a brief
introduction.
-
Now available: (December 2021)
+
Now available: (October 2022)
Hardware requirements:
- Small experiments: 4 GB memory, 2 CPU cores
- Medium applications: 8 GB memory, 4 CPU cores
- Large projects: 16 GB memory, 8 CPU cores
- Extra-large projects: 64 GB memory, 16 CPU cores
Some notable changes:
- - HTML presentation now includes links to formal entities.
-
- - Isar: local theory support for syntax and no_syntax commands.
-
- - Isabelle/jEdit: distribution of original jEdit editor with Isabelle/Scala
-modules and plugins.
-
- - HOL: new order prover.
-
- - HOL: many changes and improvements on bit operations and word types.
-
- - HOL: various library improvements (HOL-Library, HOL-Combinatorics,
-HOL-Analysis, HOL-Statespace)
-
- - Sledgehammer: update of ATPs and SMTs: E prover, veriT, Zipperposition,
-Vampire (now with Open-Source license).
- - Nitpick: external MiniSat solver for all supported Isabelle platforms.
-
- - ML: uniform treatment of external processes via Isabelle/Scala.
-
- - ML: advanced antiquotations for Type/Const constructors, and for inline
-instantiation of types, terms, facts.
-
- - Haskell: substantially improved Isabelle/Haskell library.
+ - HTML presentation is more robust and covers more files and links.
- - System: more predefined Isabelle symbols (blackboard-bold, Z notation).
-
- - System: support for Isabelle/Scala modules defined in user-space.
+ - Display of instantiation for schematic goals.
- - System: improved document preparation using Isabelle/Scala.
+ - PIDE: improved Isabelle/VSCode based on bundled VSCodium engine.
- - System: update to current Java 17 LTS.
+ - HOL: various improvements of theory libraries.
- - System: update to Poly/ML 5.9 with improved support for ARM64 on Linux.
+ - HOL: updates and improvements of Sledgehammer.
+
+ - HOL: improved simproc support for record types.
+
+ - ML: scalable type Bytes.T with support for XZ compression.
+
+ - System: bundled Node.js/Chromium/Electron platform (part VSCodium).
+
+ - System: Isabelle/Scala is based on Scala 3 (dotty compiler).
+
+ - System: tools to sync hg repositories, notably Isabelle + AFP.
+
+ - System: improved "isabelle log" tool with regex filtering.
See also the
cumulative NEWS.
Distribution & Support
Isabelle is distributed for free under a conglomerate of
open-source licenses, but the main code-base is subject to
BSD-style regulations. The application bundles include source and
binary packages and documentation, see the
detailed installation
instructions. A vast collection of Isabelle examples and
applications is available from
the Archive of Formal
Proofs.
Support is available by the
official documentation and
mailing lists:
Zulip Chat is a
real-time discussion platform to exchange ideas, ask questions,
and collaborate on Isabelle projects, with
minimalistic public
archive.
Stack
Overflow is a question-and-answer platform, with complex
review process but limited discussion facilities.
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 20.04 with &distname;. It can
+
The Docker image contains Ubuntu Linux 22.04 with &distname;. It can
be used, e.g. on another Linux host like this:
- docker pull makarius/isabelle:&distname;
- docker run makarius/isabelle:&distname;
That provides command-line access to the
regular isabelle tool wrapper, with indirection
through the Docker container infrastructure.
Linux
Requirements
- &distname;_linux.tar.gz
- Proper Window manager / Desktop environment that works
with Java/AWT/Swing
- TeXLive for Isabelle/LaTeX document preparation
Installation
The bundled archive contains everything required for Isabelle
on Linux. It can be unpacked into an arbitrary directory like
this:
- tar -xzf &distname;_linux.tar.gz
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)
+
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.
&distname;\Cygwin-Terminal allows to run Isabelle
command-line tools, as known from Unix.
&distname;\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 (10.13, 10.14, 10.15, 11.x, 12.x — 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:
- Open
&distname;.app
and Cancel the subsequent security dialog.
- Open Security & Privacy in system
preferences: section "Allow apps ..." at the bottom
should list the blocked application
(see screenshot).
- Click Open Anyway and provide further
confirmations as required.
Download for Linux (Intel)
Download for Windows
Download for macOS