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.
The full collection of Isabelle distribution archives is available for reference. Past releases are available from the archive. Further technical background information may be found in the Isabelle System Manual.
Linux
Requirements
- &distname;_linux.tar.gz
- Perl 5.x with libwww
- 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:
- &distname;/&distname;
Other Isabelle command-line tools can be invoked from the terminal like this:
- &distname;/bin/isabelle
Windows (7, 8, 8.1, 10)
Requirements
- &distname;.exe
- MikTeX for Isabelle/LaTeX document preparation
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 special certificates and signatures, so Microsoft tends to reject it by default. Running it for the first time might require 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.10, 10.11, 10.12, 10.13, 10.14)
Requirements
- &distname;_macos.tar.gz
- MacTeX for Isabelle/LaTeX document preparation
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.
The main Isabelle distribution is hidden inside the
&distname;.app
folder. This is relevant when
invoking Isabelle command-line tools, e.g. like this in the
Terminal application:
- /Applications/&distname;.app/Isabelle/bin/isabelle
Note: The Isabelle application lacks special certificates and signatures, so Apple tends to reject it by default. Running it for the first time might require a right-click or control-click on the application icon to open it explicitly.
+Note: macOS 10.15 Catalina rejects unsigned apps and + command-line tools outright. It is possible to run Isabelle + nonetheless, by disabling Gatekeeper temporarily like + this: + +
-
+
- sudo spctl --master-disable +
- open /Applications/&distname;.app +
- sudo spctl --master-enable +
Docker: Headless Ubuntu Linux
Requirements
- Docker container for the host operating system
- Docker image for Isabelle
Installation
The Docker image contains Ubuntu Linux 18.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.