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.2pre000921

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

You can see the current documentation: the user manual in , or , and the new separate "adapting" manual, in , or ,

Pre-release: ProofGeneral-3.2pre000921

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

For install instructions, see the .

Complete Archive of ProofGeneral-3.2pre000921 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

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. Note that there are no pre-built documentation files in the developer's release.