Here is the latest pre-release of Proof General. For developers, it is also available as a complete archive, including forthcoming support for more proof assistants.

Pre-releases of Proof General may be buggy as we add new features and experiment with them. Nonetheless, we welcome bug reports. But please make sure you are using the current pre-release before reporting problems.

Pre-release: ProofGeneral-3.0pre991123

Check the file for a summary of changes since the last stable version, and the planned changes to come.

• gzip'ed tar file:
• Linux RPM package
  You probably don't need the .

Complete Archive of ProofGeneral-3.0pre991123

This archive is a snapshot from our CVS repository.

• gzip'ed tar file:

What's the difference from the working version above? The complete archive also includes:

• 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!

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.