Development of Proof General

Please see http://proofgeneral.inf.ed.ac.uk/devel for the main development page.

New development is centred around a common protocol for interactive proof. Please see:

• PGIP
• ProofGeneralKit

For the time being development and maintenance of the existing system will continue, although we plan a new version of the Emacs based system which uses the new infrastructure. See NewProofGeneralEmacs. Most features can be ported over (especially if they fit within PGIP facilities), so please do not be put off contributing improvements or fixes! See:

• PGEmacsWantedFeatures
• PGEmacsDebuggingTips