Road map for future PGIP releases

2.1

PGIP as it is now, in time for and compatible with Isabelle 2007, but with some simplifications to cut down on the number of messages and the message model. See PGIPRecentChanges.

Possibly refactored into several schemas: we'd like this so that prover developers only have to look at the part that concerns them. We need to solve technical problems with the HaXml/DTD/Broker toolchain.

Possibly with additions for compatibility with Coq and other provers with AlternatePGIPUndoModel.

2.2

New display protocol, prover part backwards compatible to 2.1 (and hence Isabelle2007)

3.0

Replace prover part with generic prover meta-model (general solution for AlternatePGIPUndoModel, among others), instantiation for old model backwards compatible with 2.0.

See PGIPVersionThree.