PGIP, the Proof General Interaction Protocol

PGIP is a protocol for conducting interactive proof and a framework for connecting theorem provers to interfaces and other components. It is being used for the next generation of Proof General interfaces in the Proof General Kit project.

Structure of PGIP

The protocol is based on XML messages which are passed in an RPC-like exchange between different software components. The protocol has several subsets:

• The prover protocol, for connecting the theorem prover
  See AddingPGIPSupportHowTo for hints about adding PGIP support to a new theorem prover.

• Proof script document markup, which used inside the prover protocol.
  The markup of a proof script provides surface information about its structure gained by (native) parsing.
  Additional "meta-information" can be attached during parsing or at later stages, which describes things like dependency relations.
  See PGIPDocumentMarkup for more details.

• The display protocol, for connecting the interfaces.
  This presents the marked up proof script to the display and enables editing and state changing on it. It's like a very simple and specific DOM-style API.
  See PGIPDisplaysHowTo for hints on implementing a PGIP-enabled interface component.

• A small number of configuration messages, for describing available components.

• PGML, a simple markup language used for annotating concrete output syntax from the prover.
  The primary use of PGML is for displaying mathematical symbols accurately.
  Symbol names are taken from LaTeX (similarly to Isabelle).
  See the PGML page for more details.

Specification of PGIP

The syntax of the XML messages and markup is defined by a RELAX NG schema in compact notation, available at:

http://proofgeneral.inf.ed.ac.uk/Kit/dtd/pgip.rnc

or (for the latest version) in the ProofGeneralCVSRepository at Kit/dtd/pgip.rnc.

The meaning of markup and messages exchanged and the protcol itself is elaborated in the PGIPCommentary.

Implementations of PGIP

Please see ProofGeneralKit for the wiki page with details of our implementation of the PGIP protcol and links to some of the available software which uses it. The protocol is designed to use a fixed middleware component (the ProofGeneralBroker of Proof General Kit), together with provers and interfaces which each need to support only their own part of the protocol.

Development of PGIP

We regard this protocol as under development. We hope to keep it as small, simple and lightweight as possible, while supporting the features that we need. With this concern in mind, we are open to suggestions for extensions or improvements to the protocol.

Please see:

• PGIPRoadMap for evolution plan
• PGIPRecentChanges for recent changes
• PGIPDevelNotes for some development notes

According to http://acronymfinder.com, Acronym:PGIP stands for Proof General Interface Protocol. This was our interpretation of the protocol in early versions. Now it has been extended to allow more programmatic usage, we prefer Proof General Interaction Protocol.