Proof General Documentation Wiki

https://web.Archive.org/web/20060116123403im_/http://ProofGeneral.Inf.Ed.ac.uk/wiki/classic/img/General.png
Proof General Documentation Wiki [No Recent changes] • [No WikiNode] • About • [No Mobile URL]
Founded by:	unknown
Status:	Dead
Language:	English
Edit mode:	LoginToEdit
Wiki engine:	MoinMoin
Wiki license:	No license
Main topic:	Mathematics

For the replacement wiki powered by TWiki, see: PG Web.

Wiki size:

375 article pages see stats

(As of: 2006-01-04 – Archive.org)

Welcome to Proof General Eclipse

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 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 exciting features (see some screenshots) and a wide range of bugs.

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 download page. 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 feature requests for things you would like to see supported. Bugs should be reported on the known bugs page.

Documentation is coming: please see the user documentation, setup documentation or developer documentation. There is also a page for known bugs, which will no doubt grow rapidly. For theoretical discussions (and to cite this project), see Proof General publications.

This site is a wiki, which means anyone can edit it. You (yes you) can edit any page. Just click on an Edit Page link (these are at the side and the bottom of every page) to go to a wiki-text editor where you can change or extend the page.

The idea is that - although most of the documentation will be written by the developers - where documentation is unclear, Proof-General's users can extend and improve the documentation. Hence the documentation will be better than if it were maintained by developers alone :). You can also use this site to post questions, requests and suggestions - just preface your comment with QUESTION:, REQUEST: or SUGGESTION: (include an email address if you wish to be contacted).

Related Work

Proof General is not the only proof interface available! You may also be interested in the following projects:

• TexMacs
• Theorema
• PCoq

Proof General is developed at the University of Edinburgh Division of Informatics by Daniel Winterstein and David Aspinall. Feel free to contact us with any queries.