General
Isabelle runs on common Unix platforms and Windows with Cygwin. We provide ready-to-use binary packages for the most common platforms.
A practically usable Isabelle system consists of the following components:
- A suitable Standard ML environment, such as Poly/ML. The latest Poly/ML 5.2 works on many platforms and provides native multicore support for parallel processing.
- The Isabelle system itself (source distribution), including the desired object logics (e.g. HOL, HOL-Complex).
- The Proof General user interface with a working version of Emacs (e.g. GNU Emacs 21 or 22, or XEmacs 21.4.x with Mule/Sumo, but not XEmacs 21.5.x beta). Picking the right Emacs version is the greatest challenge in running Isabelle Proof General.
Optional extensions:
- Document preparation requires a full LaTeX installation.
- Graph browsing depends on a Java runtime environment (version 1.4 or later).
- The sledgehammer tool requires external automatic theorem provers, such as E prover.
See below for further system-specific instructions. For more exotic platforms Isabelle needs to be compiled manually, see also INSTALL.
Linux
Installation of Isabelle/HOL on Linux (x86 and x86_64) works by downloading and unpacking the relevant packages. Here the installation location is /usr/local, but any other directory works as well:
- tar -C /usr/local -xzf Isabelle2008.tar.gz
- tar -C /usr/local -xzf ProofGeneral.tar.gz
- tar -C /usr/local -xzf polyml_x86-linux.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 -p xemacs
Failure on this is typically a problem with bad Emacs versions; the command line option -p specifies a different Emacs executable:
- /usr/local/Isabelle/bin/Isabelle -p emacs22
The X-Symbol package is already included in Proof General, but needs to be enabled separately; use the -x command line option, or the Options menu.
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/isatool tty
The above x86 binaries may be also used for 64bit Linux, but are restricted to 32bit mode; native x86_64 platform support requires manual compilation of Isabelle.
Warning: Pre-packaged versions of Isabelle, Proof General, and Poly/ML floating through the Net as deb, rpm, port etc. are often outdated and rarely work as advertized. Even XEmacs is better compiled manually these days -- the packages provided for SuSE, Ubuntu, and Debian are mostly broken.
Mac OS X (Darwin)
Isabelle works on Mac OS X 10.4 (Tiger) and 10.5 (Leopard) and requires the following preliminaries:
- The X11 window system as distributed by Apple as installation option to Mac OS X.
- A version of GNU Emacs or XEmacs that works with X11. We recommend XEmacs 21.4.x from MacPorts, which may be installed from the shell as follows:
- sudo port install xemacs
Then installation on Mac OS X is analogous to Linux, the following is for Intel Macs:
- tar -C /usr/local -xzf Isabelle2008.tar.gz
- tar -C /usr/local -xzf ProofGeneral.tar.gz
- tar -C /usr/local -xzf polyml_x86-darwin.tar.gz
- tar -C /usr/local -xzf HOL_x86-darwin.tar.gz
The same works for PowerPC Macs, by replacing x86 by ppc above.
Windows (Cygwin)
Isabelle also works on Windows thanks to the excellent Posix API emulation of Cygwin. After downloading and running setup.exe, the following Cygwin packages need to be installed:
- make
- perl
- xemacs-mule-sumo
- xemacs-sumo
- xpdf
Both of the above XEmacs packages are needed! Some further requirements (such as X11) are resolved via these as well.
Now installation on Cygwin is analogous to Linux. The following should be executed within the Cygwin shell:
- tar -C /usr/local -xzf Isabelle2008.tar.gz
- tar -C /usr/local -xzf ProofGeneral.tar.gz
- tar -C /usr/local -xzf polyml_x86-cygwin.tar.gz
- tar -C /usr/local -xzf HOL_x86-cygwin.tar.gz
After startx Proof General can be run from an xterm window like this:
- /usr/local/Isabelle/bin/Isabelle -p xemacs
Further Cygwin packages will be required for a fully operational Isabelle installation, most notably tetex. Note that Java is a native Windows application -- make sure that the Cygwin shell is able to find it in its PATH.