General
Isabelle runs on common Unix systems (such as Linux or Mac OS), and Windows with Cygwin. Our packages include multi-platform binaries for a broad range of architectures. Pre-compiled logic images are available for download for the most common platforms.
A realistic Isabelle installation consists of the following parts:
- The main Isabelle source distribution.
- The Poly/ML compiler and runtime system (version 5.x). Recent Poly/ML 5.3.0 and 5.2.1 provide native multicore support for parallel processing of theories and proofs. Pre-compiled object logics (e.g. HOL, HOL-Nominal) only work for one particular Poly/ML instance, but users can also build heap images separately.
- The Proof General user interface with a working version of Emacs (either GNU Emacs 22, or XEmacs 21.4.x as last resort). Picking the right Emacs version is the greatest challenge in running Isabelle Proof General!
- A full LaTeX installation for Isabelle document preparation (optional).
- A Java runtime environment (version 1.5 or 1.6) for some extra Isabelle tools (graph browser etc.).
See below for further system-specific instructions. For more exotic platforms Isabelle logics need to be compiled manually using the Isabelle/build
script. This might also require editing of Isabelle/etc/settings
, e.g. to enable native 64bit mode on x86_64 platforms (this is only useful with more than 8GB of memory and more than 4 cores).
Warning: Pre-packaged versions of Isabelle, Poly/ML, and Proof General floating through the Net as deb, rpm, port etc. are often outdated and rarely work as advertized.
Linux
Installation of Isabelle/HOL on Linux (x86 and x86_64) works by downloading and unpacking the relevant packages. The Isabelle "bundle" already includes most required components. In the subsequent example the installation location is /usr/local, but any other directory works as well:
- tar -C /usr/local -xzf Isabelle2009-1_bundle.tar.gz
- tar -C /usr/local -xzf HOL_x86-linux.tar.gz
Normally, the default settings of Isabelle should be sufficient for invoking Isabelle Proof General like this:
- /usr/local/Isabelle/bin/isabelle emacs
- /usr/local/Isabelle/bin/isabelle emacs -p emacs22-gtk
The all-important X-Symbol package is already included in Proof General, but needs to be enabled separately: use the command line option -x true, or the Options menu in Proof General. X-Symbol mode is known to work with most variants of GNU Emacs 22.
If all fails, Isabelle may also be run without Proof General, via the plain tty interface as follows (using CTRL-D to exit):
- /usr/local/Isabelle/bin/isabelle tty
Mac OS X (Darwin)
Isabelle works well on Mac OS X 10.5 (Leopard), and 10.6 (Snow Leopard). Manual installation is analogous to Linux above and works via the Terminal application.
It is more convenient to use the following disk image that contains an application bundle with everything required for Isabelle on Intel Macs:
Isabelle.dmg.zip | 235.7 MB |
The Isabelle.app
bundle can be placed into the /Applications
directory and started as usual. The included Emacs is native on Mac OS, and supports X-Symbol mode via some special TrueType fonts that are installed automatically in the user's fonts directory on startup.
Note that the main Isabelle distribution is hidden inside the Isabelle.app
directory. This is relevant when building further images, e.g. like this in the Terminal application:
- /Applications/Isabelle.app/Isabelle/build FOL
x86_64
and old ppc
.
Windows (Cygwin)
Isabelle also works on Windows thanks to the excellent Posix API emulation of Cygwin. This provides half of a Linux/GNU operating system to be run inside Windows. Alternatively, one can install a full Linux system on the Windows partition via Wubi, and then run natively without Windows.
Cygwin installation works by executing running setup.exe (version 1.7). Isabelle requires the following Cygwin packages:
- make
- perl
- python
- tetex
- tetex-extra
- xemacs-mule-sumo
- xemacs-sumo
- xinit
- xpdf
Note that this selection has been carefully chosen in order to pull in a much larger collection via implicit dependencies. Now installation on Cygwin is analogous to Linux. The following should be executed within the Cygwin shell:
- tar -C /usr/local -xzf Isabelle2009-1_bundle.tar.gz
- tar -C /usr/local -xzf HOL_x86-cygwin.tar.gz
- /usr/local/Isabelle/bin/isabelle emacs -p xemacs