Below is the latest pre-release of Proof General, made available for those who wish to test the latest features or bug fixes. For developers, this release is also available as a complete CVS snapshot (further below).

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 latest pre-release before reporting problems.

Please register if you haven't done so already.

Manual for ProofGeneral-3.2pre000609

The manual included with the pre-release may be updated from that of the .

You can see the current manual in or download the or the .

Pre-release: ProofGeneral-3.2pre000609

Check the file for a summary of changes since the last stable version, and notes about work-in-progress.

• gzip'ed tar file: ,
  or the same thing in a zip file: ,
• Linux RPM package
  You probably don't need the .

For install instructions, see the .

Complete Archive of ProofGeneral-3.2pre000609 for Developers

This archive is a snapshot from our CVS repository.

• gzip'ed tar file:

What's the difference from the user's pre-release above? The complete archive also includes:

• the low-level developer's todo files (see ) and the detailed ,
• developer's Makefile used to generate documentation files and the release itself,
• test files,
• image source files,
• the web pages,
• working instantiations of Proof General for new provers

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.