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: | NoLicense"NoLicense" is not in the list (Custom license, Attribution to contributing authors, Copyright to contributing authors, Site retains copyright, WTFPL, Licence Art Libre, Open Content License, Apache License, BSD Documentation License, FreeBSD Documentation License, ...) of allowed values for the "Wiki license" property. |
| Main topic: | Mathematics |
| Wiki size: | unknown size |
- 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 ExcitingFeatures (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 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 coming: 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.
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 ContactUs with any queries.