Version 3.0 of PGIP

Here are some collected ideas for the next major version change in PGIP.


The general aims of the revisions are:

  • To make the protocol more understandable.
  • To make it adaptable to more provers and displays.

To further the first aim, we should make use of existing XML standards where these exist. (Some of these did not exist or were not established when the PGIP work started back in 1899. We still had gaslights back then!)

Prover Protocol

On the prover side, the main aim is to relax the prescriptive prover state model, and at the same time keep the generic and uniform nature.

Simplification of prover state (and document structure) model

See PGIPBasicProverModel: it seems that we could treat the states uniformly (but still distinguish them), potentially offering these operations in each state:

   open               e.g. theory, lemma
    dostep            e.g. ...
    undostep          <improper>
   close-finish       e.g. end, qed
   close-postpone     e.g. end (but note for interface), sorry
   close-giveup       e.g. end (*remove* from theory db maybe), oops
   abort              <improper>

documents only contain proper elements, as:

        open dostep* (close-f | close-p | close-g)

All of the close operations "colour something blue". The abort operation undoes the open discarding the internal history and so leaves us where we started. We might have rules about nesting: we're not allowed to close-finish anything with close-postpone inside. Close-giveup never contributes to future dependencies so it can't cause harm.

What happened to retract? It is an undostep with a named target, so it doesn't need to be the previous thing done. So we also have:

  retract      <improper>
  redo         <improper>

Maybe we can specify which operations are available in which state and which states have a history (so support undo/redo). Or maybe we can be simple and just insist that the provers do something reasonable to match a fixed model (the original PGIP idea).

This doesn't consider nested proofs (i.e. sub-lemmas) yet. We should consider what behaviour existing provers have here, and what the best (simplest) thing for future provers would be.

Complication of object state model

The current object state model is:

 objstate = unparseable | parsed | being_processed | processed | outdated
this suffices for the broker to calculate undo/redo commands, but we noticed that it isn't quite enough for representing the precise status of objects in the display or broker.

A new, complete enumeration of object states is:

  unparsed | being_parsed | unparseable | parsed
  being_processed | unprocessable | processed |
  being_outdated | unoutdatable | outdated  
These seem to encompass all the needed states in the Broker/display. They can be represented by four underlying kinds of state:
  unparsed | parsed | processed | outdated
together with "busy" flag for the being cases and an "error" flag for the unX cases. That is, except the initial unparsed state we have have a three-state flag:
  completed | busy | error
Busy states are transient. Error states are stable but perhaps only relevant for the display: the broker retains the previous state for calculating the next state transitions. However, the broker could cache error messages in case of repeated attempts to process or parse the same piece of text. Moreover, the display may also want to record the previous state so that it can refine the UI actions available to the user. (TODO: think about the cases here in more detail).

We haven't considered the unoutdatable state yet, but it actually occurs in Isabelle for so-called "completed" theories: the ones which are built into the heap image. Are there any other cases where an outdate request may fail?

The user will not care or will be confused by all these distinctions so some of the states will not need UI distinction. E.g., all of the being states are represented as being busy (traditionally: pink colour); the un states may be represented as in an error condition (e.g. wavy underlines, or an error marker).

TODO: add state transition diagram

Maybe we can move to this a bit sooner than major revision change, since the objstate part of the protocol is not used in any released software yet?

informfile messages unified

We can use an objstate in the informfile messages to unify the different cases, at the expense of the prover now needing to represent (a small subset of) objstates.

DOM-style API for documents

Idea: combine the display protocol with a DOM-style API for manipulating proof script documents.

Name spaces and mixed-schema messages

We need to allow interoperability with other XML formats, e.g. prover-specific formats, MathML , OMDoc, etc. We should introduce a namespace to separate our elements so we can embed other document types.

XML schema datatypes instead of PGIP types

We could consider replacing our type language with (a subset of) the XML schema datatype language, embedding in a similar way to the way that RELAX does.

Advantage: standard type language and interoperability with tools for manipulating forms, for example.

Disadvantage: we would need to deal with its complexity somewhere. But hopefully only in the Broker: provers can just use string conversion functions and ignore types.

Display Protocol

The display protocol will use Xupdate pervasively, to synchronise changes in the edited text, for the provers messages, for changes in the state of the provers etc. This will make the broker play better with web-based applications ("web-enabling"). It also makes the conceptual role of the broker clearer: it provides a stateless access to inherently state-based theorem provers.

Here is a more detailed exposition.

-- ChristophLueth - 01 Jul 2007

Edit | Attach | Print version | History: r7 < r6 < r5 < r4 < r3 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r6 - 03 Jul 2007 - 21:02:16 - ChristophLueth
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