[Isabelle logo]

Isabelle Distribution Area
 

 
Isabelle Packages

 

The following source and binary packages of Isabelle_09-Apr-2001 provide everything required for easy installation of the full Isabelle working environment on common Unix platforms.

A minimal Isabelle installation requires only bash and perl (usually provided by the operating system), and a suitable implementation of Standard ML (e.g. Poly/ML as provided below). A comfortable Isabelle working environment demands further user interface support, as provided by Proof General together with the (optional) X-Symbol package. Both of these should be used with a recent version of XEmacs-21.

Packages

We provide a complete set of packages for Isabelle, Proof General and X-Symbol. While XEmacs-21 is not included here, most operating system distributions already provide a suitable package, although not installed by default.

Some packages are platform dependent. Everything is included below for Linux/x86 and Solaris/Sparc systems. Other Unix platforms work as well, but require manual compilation of Isabelle logic images using a suitable Standard ML system.

Isabelle system
  Isabelle main system   Isabelle_09-Apr-2001.tar.gz   4035 K  
  Isabelle pdf documentation   Isabelle_09-Apr-2001_pdf.tar.gz   3896 K  
Poly/ML compiler and runtime system
  Poly/ML base system   polyml_base.tar.gz   2 K  
  Poly/ML binary modules   polyml_x86-linux.tar.gz   1111 K  
  polyml_sparc-solaris.tar.gz   2133 K  
Precompiled Isabelle logics
  HOL   HOL_x86-linux.tar.gz   4922 K  
  HOL_sparc-solaris.tar.gz   5498 K  
  HOL-Real   HOL-Real_x86-linux.tar.gz   5218 K  
  HOL-Real_sparc-solaris.tar.gz   5847 K  
  ZF   ZF_x86-linux.tar.gz   3983 K  
  ZF_sparc-solaris.tar.gz   4430 K  
Proof General system
  Proof General   ProofGeneral.tar.gz   676 K  
  X-Symbol package   x-symbol.tar.gz   449 K  

Installation

Installation is very easy. Basically, just unpack all required packages within the same directory. There is no manual configuration required of any of these components, if used according to the default settings of Isabelle.

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 Isabelle_09-Apr-2001.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
   tar -C /usr/local -xzf ProofGeneral.tar.gz
   tar -C /usr/local -xzf x-symbol.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.

last update at 04/09/2001