Getting ProofPower

Contributing Documentation Download Examples Getting Home Mailing List Papers Patches Specifications

The open source parts of ProofPower and all the documentation may be obtained from this site. The documentation covers the following packages:

PPDev - The ProofPower developer kit, mainly comprising SLRP, a parser generator for Standard ML.
PPTex - The ProofPower interface to TeX and LaTeX.
PPXpp - The X Windows/Motif front-end for ProofPower.
PPHol - The HOL specification and proof development system.
PPZed - The Z specification and proof development system.
PPDaz - The Compliance Tool for specifying and verifying Ada programs.

The PDF documentation for PPDaz is freely available to anyone who is interested and the PPDaz software is available under a free licence for non-profit use.

Downloading OpenProofPower

[New!] The latest stable version of the open source distribution is version 2.7.8. It is available here. Before downloading the distribution, you may like to read the description of the changes in this release and the read-me file Some earlier versions are available here.

Browsing the Documentation

The documentation for all the ProofPower products is available on line here.

Software Requirements

OpenProofPower has been built and tested by Lemma 1 using Poly/ML versions 4.1.3 and 4.2.0 Standard ML of New Jersey (SML/NJ) version 110.54 on x86 hardware under Linux and SPARC hardware under Solaris and also using Poly/ML on Apple PowerPC hardware under Mac OS X with Apple's X11 distribution and OpenMotif 2.2. For building and running ProofPower, Poly/ML is typically two to four times faster than SML/NJ and is the recommended compiler.

If you use SML/NJ, you must use version 110.54 or later. If you use Poly/ML, then you may use version 4.1.3 or version 4.2.0, but for version 4.2.0 you will need to apply a patch which you can find here. ProofPower will not work with the beta release of Poly/ML version 5.

If you are using Mac OS X, then there are some keyboard configuration files that you can download to make working with PPXpp (and other Motif applications) easier.

Fixes and Upgrades

Patches to fix problems or make minor upgrades for ProofPower are posted from time to time on this web-site. The available patches and information about how to use them are here.

Getting PPDaz

The PPDaz package is available in source form under license from Lemma 1 Ltd. Licenses are available free of charge for academic use , personal research and commercial evaluation. To obtain PPDaz print off and fill-in two copies of the appropriate licence and post them to:

Dr. R.D. Arthan,
Lemma 1 Ltd.
2nd Floor, 31A Chain Street
Reading
Berkshire
UK
RG1 2HX.

If you are signing on behalf of academic or commercial institution, please enclose a covering letter on your institution's headed notepaper. We will return the signed licence and instructions for downloading the software.

Getting Support

If you have any problems with ProofPower, please feel free to discuss them on the ProofPower mailing list.

If you're interested in a support contract, then please contact, Rob Arthan, by e-mail [rda at lemma-one dot com] , or by post at the address given above, or by phone on +44 118 958 4409.

Created by Rob Arthan [rda at lemma-one dot com]

Last updated: $Date: 2007/11/23 16:56:09 $