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.