Proof General Kit with Emacs

Emacs users needn't be worried about the new implementation of Proof General, because it allows for a number of different front ends to be connected, including Emacs.

At the moment the implementation of the Emacs based interface is a minimal prototype which has been used to help develop and test PGIP. It is planned to enlarge this interface to proved an alternative to the classic ProofGeneralEmacs version. However, to avoid the version explosion and compatibility nightmare of maintenance, it is likely that only GNU Emacs will be supported in the new version.


There isn't a released package yet and there are no guarantees about what works and what doesn't. But you are welcome to try the code from our CVS repository:

cvs -d checkout Kit/src/pgemacs

Consult the README files within that directory.

NB: this version requires you to run the ProofGeneralBroker.

Topic revision: r3 - 31 Aug 2006 - 10:50:42 - DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies