Installation instructions

+ +

Prerequisites

+ +

Isabelle runs on common Unix platforms (Linux, Solaris, etc.). + Below we provide also some hints + on how to use Isabelle on other, not-quite-Unix platforms.

+ +

+ The packages available from our download page + expect the following software to be installed: +

+ +

bash 1.x or 2.x
Perl 5.x
optionally, XEmacs 21 or Emacs 21 with mule support (for ProofGeneral)
optionally, Java 1.1 or above (for theory graph browsing)

+ +

+ Our download page includes packages for a suitable implementation of Standard ML + (Poly/ML) and + ProofGeneral + (please register). The + Proof General distribution now already includes the X-Symbol package, + there is no need to download it separately. +

+ +

Installation

+ +

In fact, there is no + installation required. Users may just unpack all required packages within the + same directory. The default settings of Isabelle should be reasonable for + most circumstances.

+ +

A typical Linux/x86 site installation of Isabelle/HOL works as follows:

By using GNU tar, the archives are uncompressed and unpacked into the + /usr/local directory (this location may be changed to anything + appropriate): +
+ tar -C /usr/local -xzf .tar.gz
+ tar -C /usr/local -xzf ProofGeneral.tar.gz
+ tar -C /usr/local -xzf polyml_base.tar.gz
+ tar -C /usr/local -xzf polyml_x86-linux.tar.gz
+ tar -C /usr/local -xzf HOL_x86-linux.tar.gz
+
+
+ Users may now invoke Isabelle without further ado, e.g. run the main + executable /usr/local/Isabelle/bin/Isabelle to launch the Proof + General interface for Isabelle/Isar. Note that there is a separate option in + the Proof General Options menu to enable X-Symbol. +
If Emacs appears to hang when the prover process is started, see the + ProofGeneral FAQ for + advice. +

+ +

For more information, see the file INSTALL included in + .tar.gz.

+ +

Other platforms

+ +

Although Isabelle is natively designed for Unix environments, + it may also run under similar, Unix-like platforms. The + following installation instructions are hints contributed by + Isabelle users. Please feel free to contact us for any suggestions, + corrections or improvements.

+ +