Proof General Kit

Proof General Kit is a new component-based architecture for the Proof General project, based around a uniform protocol for communication between interactive proof tools, called PGIP.

Software

Work which is currently in progress includes:

• An Eclipse plugin for Proof General.
  See the wiki for download and installation instructions.
  New! Easy installations are now available at our update site.
• PG Kit broker, the central middleware component of the PG Kit framework.
  Binaries are available here:
  • Linux/x86
  (NB: this is not currently required by the Eclipse plugin)
• With assistance from Isabelle developers at Munich: a PGIP-enabled version of Isabelle/Isar.
  This is now integrated into the Isabelle distribution (the CVS version of Isabelle 2007 is most up-to-date).

Schemas and documentation

• Recent versions of the RELAX NG schemas for PGIP and PGML.
  • Master source, in compact syntax: Kit/dtd/pgip.rnc (43k), Kit/dtd/pgml.rnc (7k).
  • The derived DTDs: Kit/dtd/pgip.dtd (35k), Kit/dtd/pgml.dtd (3k).
  • The derived XML Schema files: Kit/dtd/pgip.xsd (66k), Kit/dtd/pgml.xsd (13k).
  • Viewable (but badly laid out) HTML files: Kit/dtd/pgip.html (246k), Kit/dtd/pgml.html (43k).
• A draft commentary on PGIP, Kit/docs/commentary.pdf (229k).
  
• Further documentation and development notes can be found on the PG wiki, especially the PGIP page, and in the papers on the publications page.

Planning

The ideas behind the Proof General Kit are described in these papers:

• David Aspinall. Protocols for Interactive e-Proof. Draft version, see here.
• David Aspinall. Proof General Kit (white paper). Draft version, see here.
• David Aspinall. Plans for Eclipse Proof General, an Eclipse front end for Proof General (project partly sponsored by IBM award).

Click here to go back to the front page.