General
Isabelle supports the three main platform families: Linux, Mac OS X, and Windows (via Cygwin). The main Isabelle bundle already includes pre-compiled logic images and add-on tools for convenience, with a few external requirements as explained below.
The raw Isabelle source package is available here, but assembling a proper distribution from it is quite involved. Past releases are available from the archive. An arbitrary repository snapshot of Isabelle is also available (not for production use).
Warning: Pre-packaged versions of Isabelle, Poly/ML, and Proof General floating through the Net as deb, rpm, port etc. are usually incomplete and outdated!
Linux
Requirements
- 32 bit Isabelle2011-1_bundle_x86-linux.tar.gz or
64 bit Isabelle2011-1_bundle_x86_64-linux.tar.gz - GNU make
- Perl 5.x with libwww
- Python 2.x
- GNU Emacs 23 (optional, for Proof General)
- LaTeX (optional, for document preparation)
- 32bit C/C++ standard libraries, which often need to be requested explicitly for 64bit Linux distributions.
Installation
The bundled archive contains almost everything required for Isabelle on Linux. It can be unpacked into an arbitrary directory like this:
- tar -xzf Isabelle2011-1_bundle_x86-linux.tar.gz
In principle, invoking Isabelle Proof General now works like this:
- Isabelle2011-1/bin/isabelle emacs
- Isabelle2011-1/bin/isabelle emacs -p emacs23
The important Unicode token mode requires a suitable font with mathematical symbols (e.g. STIXGeneral). Assuming that the font has been installed properly on the system it can be enabled via Emacs option menus, for example.
Instead of Proof General / Emacs, the new Prover IDE based on Isabelle/Scala and jEdit can be invoked like this:
- Isabelle2011-1/bin/isabelle jedit
Mac OS X (10.5, 10.6, 10.7)
Requirements
- Isabelle2011-1.dmg
- Java for Mac OS X Lion (already included in Leopard and Snow Leopard)
- LaTeX (optional), e.g. see MacTeX
Installation
The above disk image contains an application bundle with everything required for Isabelle on Intel Macs, both for classic Proof General or the new Isabelle/jEdit Prover IDE. The Isabelle application can be placed into the /Applications folder and started as usual.
The included GNU Emacs 23 for Proof General supports Unicode symbols via the STIXGeneral font, which is installed automatically in the user's Library/Fonts folder on application startup.
Note that the main Isabelle distribution is hidden inside the Isabelle2011-1.app folder. This is relevant when building further images, e.g. like this in the Terminal application:
- /Applications/Isabelle2011-1.app/Isabelle/build -m HOLCF HOL
Windows (with Cygwin)
Requirements
- Isabelle2011-1_bundle_x86-cygwin.tar.gz
-
Cygwin 1.7.x with the following packages (to be selected manually in setup.exe):
- make
- perl
- python
- tetex-extra (optional, for document preparation)
- tetex-x11 (optional, for document preparation)
- xemacs-mule-sumo (optional, for Proof General)
- xemacs-sumo (optional, for Proof General)
- xinit
- xpdf
Installation
The bundled archive contains everything required for Isabelle on Cygwin. It can be unpacked into an arbitrary directory as follows. Note that the tar/gzip of Cygwin needs to be used here, not an archiving tools for Windows!
- tar -xzf Isabelle2011-1_bundle_x86-cygwin.tar.gz
- Isabelle2011-1/bin/isabelle emacs -p xemacs
Instead of Proof General / Emacs, the new Prover IDE based on Isabelle/Scala and jEdit can be invoked like this:
- Isabelle2011-1/bin/isabelle jedit
Sometimes Cygwin executables produce strange runtime exceptions and stack dumps. Often this can be amended via rebaseall as explained in the Cygwin/X FAQ, for example.