Getting ProofPower

Contributing Documentation Download Examples Getting Home Mailing List Papers Patches Specifications

OpenProofPower 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.

Downloading OpenProofPower

The latest working version of the open source distribution is version 3.1w8. It is available here. This version works with recent versions of Poly/ML or Standard ML of New Jersey and should be compatible with most C/C++ developer kits (including those that default to 32-bit architecture and those like Apple's Xcode tools that default to 64-bit architecture). Some earlier versions (and sometimes sneak previews of later versions) are available here.

Browsing the Documentation

The documentation for OpenProofPower is available on-line here.

System Requirements

Poly/ML is the recommended Standard ML compiler and OpenProofPower is compatible with version 5.5.1, 5.5.2, 5.6 and 5.7. OpenProofPower has also been tested on versions 110.79 and 110.80 of Standard ML of New Jersey. You will need OpenMotif version 2.3 or later.

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 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 [rda at lemma-one dot com] .

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

Last updated: $Date: 2017/06/19 11:57:53 $