NOTE: The current pre-release is the same as version 3.2. It won't be updated with new features until 3.2 has been out for a while.

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.3pre010320

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

Here is the pre-release documentation: the user manual in , or , and the new separate "adapting" manual, in , or .

Pre-release: ProofGeneral-3.3pre010320

This version has been tested with XEmacs version 21.1.12 and (minimally) with FSF Emacs 20.7.1. We recommend the use of XEmacs; use under FSF Emacs can no longer be supported.

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

For install instructions, see the stable version download.

Complete Archive of ProofGeneral-3.3pre010320 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 the developers page) 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.