Proof General Documentation Wiki: Difference between revisions
Hoof Hearted (talk | contribs) (Created page with "{{Wiki |name=Proof General Documentation Wiki |URL=https://web.Archive.org/web/20060118152915/https://ProofGeneral.Inf.Ed.ac.uk/kit/wiki |logo=https://web.Archive.org/web/2006...") |
Hoof Hearted (talk | contribs) (added Category:Edinburgh using HotCat) |
||
| (3 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{Wiki | {{Wiki <!--see 'Template:Wiki' for full detail and hidden help advice--> | ||
|name=Proof General Documentation Wiki | |name = <s>Proof General Documentation Wiki</s> | ||
|URL=https://web.Archive.org/web/20060118152915/https://ProofGeneral.Inf.Ed.ac.uk/kit/wiki | |URL = https://web.Archive.org/web/20060118152915/https://ProofGeneral.Inf.Ed.ac.uk/kit/wiki | ||
|logo=https://web.Archive.org/web/20060116123403im_/http://ProofGeneral.Inf.Ed.ac.uk/wiki/classic/img/General.png | |logo = https://web.Archive.org/web/20060116123403im_/http://ProofGeneral.Inf.Ed.ac.uk/wiki/classic/img/General.png | ||
|recentchanges URL=No | |wide logo = y<!--insert 'y' when the logo is too wide AND / OR the title name is too long--> | ||
|wikinode URL=No | |recentchanges URL= No<!--https://YourWikiURL.org/wiki/Special:RecentChanges, if none, use 'No'--> | ||
|about URL=https://web.Archive.org/web/20060116144808/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/FAQ | |wikinode URL = No<!--https://YourWikiURL.org/wiki/WikiNode, if none, use 'No'--> | ||
|mobile URL=No | |about URL = https://web.Archive.org/web/20060116144808/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/FAQ | ||
|founder=unknown | |mobile URL = No | ||
|status=Dead | |founder = unknown<!--wiki founder(s) name(s); wikilink or hotlink if available; if unknown, use 'unknown'--> | ||
|language=English | |status = Dead | ||
|editmode=LoginToEdit | |language = English | ||
|engine=MoinMoin | |editmode = LoginToEdit | ||
|license= | |engine = MoinMoin | ||
|maintopic=Mathematics | |license = No license | ||
}} | |maintopic = Mathematics | ||
{{Size}} | |backupurl = <!--database dump backup file URL; found at '/Special:Statistics' on Wikia & some other MediaWiki sites; archived URL may also be used--> | ||
|backupdate = 20YY-MM-DD<!--YYYY-MM-DD, ISO 8601 extended date of backup URL; if unknown, dynamic or NO date, DELETE this field--> | |||
}}{{For|the replacement wiki powered by TWiki|PG Web}} | |||
{{Size <!--see 'Template:Size' for extensive full detail--> | |||
|pages= 375<!--plain numeric value for number of CONTENT pages (or Files on a commons wiki); NO thousands separators--> | |||
|statistics URL= https://web.Archive.org/web/20060104221027/http://ProofGeneral.inf.ed.ac.uk/cgi-bin/wiki.cgi/PageSize | |||
|wikiFactor= <!--(wF), preferred; see: Category:wikiFactor; if wF unknown leave void; archived wF value may be used--> | |||
|wikiFactor URL= <!--wF source; often 'PopularPages', 'Mostvisitedpages', 'PageHits'; leave void if unknown; archived URL if available--> | |||
}}(As of: 2006-01-04 – [[Archive.org]])<!--YYYY-MM-DD; manually add/amend ISO 8601 date when stats are verified and/or updated--> | |||
;''Welcome to Proof General Eclipse | ;''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. | Good interfaces and development tools are crucial if interactive proof systems are to be adopted by {{tag|Mathematics|mathematicians}} and computer programmers. Unfortunately, the development tools available for theorem provers are often quite rudimentary. The [https://ProofGeneral.github.io Proof General] project is an ongoing attempt to redress this. Proof General provides a generic interface to interactive theorem provers such as [[Archive.org:20060116145417/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/Isabelle|Isabelle]] or Coq. It is packed with [[Archive.org:20060116143645/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/ExcitingFeatures|exciting features]] (see some [[Archive.org:20060116123731/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/ScreenShots|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 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. | PG/Eclipse is still in development. A beta-release version is now available from the [[Archive.org:20060116130749/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/DownloadPage|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 [[Archive.org:20060116145914/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/FeatureRequests|feature requests]] for things you would like to see supported. Bugs should be reported on the [[Archive.org:20060116141831/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/KnownBugs|known bugs]] page. | ||
Documentation is coming: please see the UserDocumentation, SetupDocumentation or DeveloperDocumentation. There is also a page for | Documentation is coming: please see the [[Archive.org:20060116143318/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/UserDocumentation|user documentation]], [[Archive.org:20060116135122/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/SetupDocumentation|setup documentation]] or [[Archive.org:20060116135825/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/DeveloperDocumentation|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 [[Archive.org:20060116141947/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/ProofGeneralPublications|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. | 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. | ||
| Line 31: | Line 41: | ||
;''Related Work | ;''Related Work | ||
Proof General is not the only proof interface available! You may also be interested in the following projects: | Proof General is not the only proof interface available! You may also be interested in the following projects: | ||
*TexMacs | *[[Archive.org:20060116135158/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/TexMacs|TexMacs]] | ||
*Theorema | *[[Archive.org:20060116142930/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/Theorema|Theorema]] | ||
*PCoq | *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. | Proof General is developed at the [https://www.Ed.ac.uk/informatics/ University of Edinburgh Division of Informatics] by [[Archive.org:20060213065652/http://BigRed.HomeLinux.org/~danielw/|Daniel Winterstein]] and [https://www.Inf.Ed.ac.uk/people/staff/David_Aspinall.html David Aspinall]. Feel free to [[Archive.org:20060116134522/http://ProofGeneral.Inf.Ed.ac.uk/cgi-bin/wiki.cgi/ContactUs|contact us]] with any queries. | ||
[[Category:Edinburgh]] | |||
[[Category:Founded in 2004]] | |||
Latest revision as of 14:10, 4 July 2023
| https://web.Archive.org/web/20060116123403im_/http://ProofGeneral.Inf.Ed.ac.uk/wiki/classic/img/General.png | |
|---|---|
[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:
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.