imported from old wiki, not really used here
Welcome to Proof General
Good interfaces and development tools are crucial if interactive proof systems are to be adopted by mathematicians and computer programmers. Unfortunately, the development tools available for theorem provers are often quite rudimentary. The
[http://proofgeneral.inf.ed.ac.uk Proof General] project is an ongoing attempt to redress this. Proof General provides a generic interface to interactive theorem provers such as ["Isabelle"] or Coq. It is packed with
ExcitingFeatures (see some
ScreenShots ) and a wide range of bugs.
Proof General in Eclipse (PG/Eclipse) marks an exciting new phase in the project. The new interface is not only much prettier than the old Emacs based system, but also offers more sophisticated functionality. It is built using a protocol for interactive proof sessions called
PGIP, and will work with any prover that implements this protocol. Currently, that means the latest version of Isabelle - but hopefully it will be relatively easy to adapt any interactive prover to use
PGIP.
PG/Eclipse is still in development. A beta-release version is now available from the
DownloadPage . Alternatively, the older emacs-based system is available from
http://proofgeneral.inf.ed.ac.uk/. The emacs system is considerably more stable at present (but we're working on the Eclipse version...). You can help guide the development of PG/Eclipse by adding to (or commenting on) the
FeatureRequests
for things you would like to see supported. Bugs should be reported on the
KnownBugs page.
Documentation is also in progress. Please see the
UserDocumentation ,
SetupDocumentation or
DeveloperDocumentation . There is also a page for
KnownBugs , which will no doubt grow rapidly. For theoretical discussions (and to cite this project), see
ProofGeneralPublications .
Please help us to improve the documentation of Proof General by editing these pages. You can also use this site to post (non-urgent) questions, requests and suggestions --- just preface your comment with QUESTION:, REQUEST: or SUGGESTION:.
Proof General is developed at the
[http://www.inf.ed.ac.uk University of Edinburgh's School of Informatics].
[http://bigred.homelinux.org/~danielw Daniel Winterstein] wrote the first Eclipse version and prepared this wiki.
[http://homepages.inf.ed.ac.uk/da David Aspinall] is the project leader.
Feel free to
ContactUs with any questions.