Here is the latest pre-release of Proof General. It is also available as a complete archive for developers, to test forthcoming support for new proof assistants.

Pre-release: ProofGeneral-3.0pre991116

This pre-release of Proof General may be buggy as new features are added and experimented with.
Check the file for a summary of changes since the last stable version, and the planned changes to come.
Please test with the current pre-release before reporting any problems in a pre-release.

• gzip'ed tar file:
• Linux RPM package
  The source RPM is .

Complete Archive of ProofGeneral-3.0pre991116

If you are interested in helping to develop the core of Proof General, we provide a complete archive of all the sources used to build the current Proof General pre-release. The difference from the working version distribution above is that we include:

• provisional instantiations of Proof General to new provers
  (mentioned in the file),
• the and the detailed ,
• developer's Makefile used to generate documentation files
  and the release itself from our CVS repository,
• some test files,
• sources for some of the images,
• the web pages.

Note: there are no pre-built documentation files in the developer's release, because developers should have the right tools!

• gzip'ed tar file:

You probably don't need to download this if you're only interested in hacking the Emacs lisp part of the program for a prover that is currently supported. But you may still like to check the latest .

We have a mailing list for developers, at proofgeneral-devel@dcs.ed.ac.uk.
To subscribe (or unsubscribe), send a message to majordomo@dcs.ed.ac.uk with the words "subscribe proofgeneral-devel" (or "unsubscribe proofgeneral-devel") in the message body.

If you are interested in developing the core of Proof General, we can make our CVS repository accessible to you. Please ask.