General
Isabelle supports the three main platform families: Linux, Mac OS X (Leopard or Snow Leopard), 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.
Both the x86 and x86_64 variants are supported routinely, but x86 is the default. Note that native x86_64 is only useful with 6GB of physical memory, or more.
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
- Isabelle2011_bundle_x86-linux.tar.gz
- Java Runtime Environment 1.6 from Oracle/Sun (not OpenJDK)
- GNU Emacs 23
- GNU make
- Perl 5.x with libwww
- Python 2.x
- LaTeX (optional)
- 32bit C/C++ standard libraries, which often need to be requested explicitly for some 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_bundle_x86-linux.tar.gz
In principle, invoking Isabelle Proof General now works like this:
- Isabelle2011/bin/isabelle emacs
- Isabelle2011/bin/isabelle emacs -p emacs23
The important Unicode token mode requires a suitable font with mathematical symbols (e.g. IsabelleText in Isabelle2011/lib/fonts). Assuming that the font has been installed properly on the system it can be enabled via Emacs option menus, or on the command line:
- Isabelle2011/bin/isabelle emacs -f IsabelleText
Mac OS X (10.5 or 10.6)
Requirements
- Isabelle2011.dmg
- LaTeX (optional), e.g. see MacTeX
Installation
The above disk image contains an application bundle with everything required for Isabelle on Intel Macs. It can be placed into the /Applications
folder and started as usual. The included GNU Emacs 23 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.app
folder. This is relevant when building further images, e.g. like this in the Terminal application:
- /Applications/Isabelle2011.app/Isabelle/build -m HOLCF HOL
Windows (Cygwin)
Requirements
- Isabelle2011_bundle_x86-cygwin.tar.gz
- Java Runtime Environment 1.6 from Oracle/Sun
-
Cygwin 1.7.x with the following packages (to be selected manually in setup.exe):
- libgmp3
- make
- perl
- python
- tetex-extra (optional)
- tetex (optional)
- xinit
- xemacs-mule-sumo
- xemacs-sumo
- 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_bundle_x86-cygwin.tar.gz
- Isabelle2011/bin/isabelle emacs -p xemacs
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.