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.
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 .
This version has been tested with XEmacs version 21.4.8 and with GNU Emacs 21.2.1. XEmacs support is better tested. Older releases of Emacs may work, but we recommend the use of these or newer versions because backwards compatibility across different Emacs versions is too difficult to support. If you cannot upgrade your Emacs, consider using an older release of Proof General.
Check the file for a summary of changes since the last stable version, and notes about work-in-progress.
| gzip'ed tar file | |
| zip file | |
| RPM package | |
| individual files | http access to files in development release |
NB: we no longer distribute the source RPM, since you can build both source and "binary" RPMs direct from the tarball using "rpm -ta".
For install instructions, see the stable version download.
This archive is a snapshot from our CVS repository.
What's the difference from the user's pre-release above? The complete archive also includes:
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.