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), which includes files not needed for the running program.
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 adapting manual, in , or .
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 |
Emacs versions: This version has been tested with XEmacs version 21.4.12 and with GNU Emacs 21.2.1. XEmacs support is better tested, although use under GNU Emacs has certain advantages (e.g., nested comments!). Please check for detailed notes. Older releases of Emacs may work, but we recommend the use of these or newer versions because backwards compatibility across different Emacs versions is far too difficult to support. If you cannot upgrade your Emacs, consider using an older release of Proof General.
Prover versions: This version has been tested with Coq 7.4, Isabelle2003, Lego 1.3.1, and PhoX 0.8.
Bundled packages: Proof General is now bundled with several Emacs packages, to save the effort needed of installing them separately, and to solve compatibility problems. This includes X-Symbol, so you don't need to download it separately any more. If you want to override PG's preference for it's own packages, simply load your versions into memory before starting Proof General (e.g. with (require 'x-symbol) in your .emacs file).For install instructions, see the stable version download.
This tarball contains all of our development files, including some files not present in the released version of Proof General. Specifically:
Most people don't need this. Note that there are no pre-built documentation files in the developer's release (developers can run Make, by definition).