Hints on Adding PGIP Support to a Theorem Prover

This page is intended as a rough HOWTO for adding PGIP support to a theorem prover.

Apart from hints below, the main resource is the PGIPCommentary which is a reference on the messages in PGIP and their meaning.

There are several tasks in adding PGIP support to a prover:

  1. Understand prover-side basics of PGIP: see PGIPBasicProverModel
  2. Support XML message passing over pipes or sockets
  3. Implemement PGIP message dispatch and reception
  4. Support parsing proof scripts to add PGIP markup
  5. Support interpreting PGIP prover control messages
  6. Add output markup to control display, error recognition

Support proof script parsing

In PG Kit, proofs are conducted by communicating PGIP messages. The broker plays a central role in the framework, like managing proof scripts and the connection between front-ends and provers. But all the broker's knowledge about proof scripts are from those XML elements defined in PGIP. The broker has no idea about a prover's proof language, therefore the work of parsing proof scripts need to be done by the prover itself.

On receiving a PGIP message wrapped using <parsescript>, the prover extracts out the proof script or maybe a segment of it, parses it, and replies using <parseresult>. Note that parseresults can be different because of the existence of following cases:

  • Parseable. In this case, the reply from the prover uses <parseable>;
  • Unparseable. In this case, if the prover wants this unparseable information to be displayed on the front-end, it can use <errorresponse> which contains <pgmltext>, otherwise it can use <unparseable>.

Both <parsescript> and <parseresult> have two optional attributes location_attrs and systemdata_attr. <parsescript> can use location_attrs to transmit the location information of a part of a script, while <parseresult> can use it to pass position information back to the display, particularly in the case of (re-)parsing only part of a script. systemdata_attr is used to describe the system-specific data, especially useful for "stateless" RPC.

Support PGIP control messages

The PGIP control messages we mean are those messages sent to a prover which in PGIP.rnc belong to <provercontrol>. A PGIP control message can be:
  • <proverinit>, which asks the prover to reset itself to its initial state;
  • <proverexit>, which asks the prover to exit. This control message can be used when users want to switch to another prover;
  • <startquiet>, which asks the prover to stop sending proof state displays, non-urgent messages. This message can be used when processing a proof development with a large number of proof commands, to avoid the display of intermediate proof states;
  • <stopquiet>, which asks the prover to turn on its noraml proof state and message displays;
  • <pgmlsymbolson> which asks the prover to activate the use of symbols in PGML output;
  • <pgmlsymbolsoff> which asks the prover to deactive the use of symbols in PGML output.

The key point of requiring provers to support PGIP control messages is understanding the messages and performing corresponding operations. Replies from provers in this case are not that important. Provers can resend startup PGIP messages for <proverinit> or just <ready> messages for all of them.

Adding output markup

The framework of PG Kit is component-oriented. Each component is comparatively independent. They know quite a little about other components. For example the broker, it doesn't know the concrete syntax of a prover's proof language. It can understand a prover only if the prover "talks" to it in PGIP. Requiring the prover to add output markup is just to ask the prover speak in PGIP. Two major rules of this addition need to be followed, which are:
  • using correct markup
    PGIP is a protocol. It has a set of rules for communication. For instance, if the incoming message is <askpgip>, the prover respones using <usespgip>. Some other pairs are like:
    <askguise> <-> <informguise>; <askids> <-> <showid>; <askprefs> <-> <hasprefs>; <parsescript> <-> <parseresult>;
    If errors occur, the prover replies using <errorresponse>
  • The prover should issue a <ready> message when it starts up, and each time it has completed processing a command from the interface.

But I really, really hate XML

In this case you could avoid adding XML parsing/printing support by instead using a PGIPFilter which will translate between a plain-text based implementation of the protocol and XML.

However, you must still make sure that the prover implements the PGIP abstraction correctly.

The disadvantage of this approach is that you need the external filter program; also you may lose some flexibility with symbol support.

Topic revision: r8 - 12 Sep 2006 - 16:51:53 - HuaYang
Main.AddingPGIPSupportHowTo moved from Main.AddingPGIPSupportHints on 22 Aug 2006 - 13:39 by DavidAspinall
 
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies