General
Isabelle supports the three main platform families: Linux, Mac OS X (Leopard or Snow Leopard), and Windows (via Cygwin). Apart from the main Isabelle bundle that already includes various pre-compiled logic images and add-on tools for convenience, there are a few external requirements:
- GNU bash and Perl 5.x with libwww. These indispensable system tools are pre-installed on most operating system distributions, so manual intervention is rarely required.
- LaTeX for Isabelle document preparation (optional).
- Java Runtime Environment 1.6 for some extra Isabelle tools (graph browser etc.) and the Isabelle/Scala layer. Right now there are no critical applications depending on that.
See below for further platform-specific instructions. 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 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 often outdated and rarely work as advertised.
Linux
Isabelle2009-2_bundle_x86-linux.tar.gz | 247.0 MB |
The above archive contains almost everything required for Isabelle on Linux. It can be unpacked into an arbitrary directory, which is /usr/local in the subsequent example:
- tar -C /usr/local -xzf Isabelle2009-2_bundle_x86-linux.tar.gz
In principle, invoking Isabelle Proof General now works like this:
- /usr/local/Isabelle/bin/isabelle emacs
- /usr/local/Isabelle/bin/isabelle emacs -p emacs22-gtk
The important X-Symbol mode of Proof General needs to be enabled separately: use the command line option -x true, or the Options menu in Proof General.
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 (10.5 or 10.6)
Isabelle2009-2.dmg | 311.6 MB |
This disk image contains an application bundle with everything required for Isabelle on Intel Macs. It can 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 Isabelle2009-2.app
directory. This is relevant when building further images, e.g. like this in the Terminal application:
- /Applications/Isabelle2009-2.app/Isabelle/build -m HOL-Word HOL
See MacTeX for LaTeX-based Isabelle document preparation.
Mac OS X already includes Java 1.6 by default, but it may have to be activated manually using the Java configuration utility provided by Apple.
Windows (Cygwin)
Isabelle2009-2_bundle_x86-cygwin.tar.gz | 246.9 MB |
Isabelle requires Cygwin (version 1.7.x) in order to turn Windows into a system conforming to common Posix/GNU standards. Alternatively, one can install a full Linux/GNU system on the Windows partition via Wubi, and then run natively without Windows, see Linux above.
Cygwin installation works by executing setup.exe. The following Cygwin packages are required:
- libgmp3
- 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. The remaining installation is analogous to Linux.
The main Isabelle bundle above contains everything required for Isabelle on Cygwin. It can be unpacked into an arbitrary directory, which is /usr/local in the subsequent example, but any Windows path like 'C:\Users\Joe\Desktop' works as well. Note that the tar/gzip of Cygwin needs to be used here, not an archiving tools for Windows!
- tar -C /usr/local -xzf Isabelle2009-2_bundle_x86-cygwin.tar.gz
- /usr/local/Isabelle/bin/isabelle emacs -p xemacs