Version 3.0 of PGIP

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

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.