Road map for future PGIP releases


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.


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


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.

Topic revision: r3 - 18 Jul 2007 - 12:22:20 - 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