Recent changes to PGIP

Some recent changes and outstanding requests for change are included in Trac.

Additional notes may be added below for items not included in Trac. The CVS change logs/diffs provide a low-level detailed view of what changed.

See PGIPOlderChanges for older changes.

Simplification of PGIP, version 2.1 (pre-1) [ongoing]

By popular demand, we have begun making some simplifications to PGIP, with the aim of cutting down the number of messages and some of the details they contain. This means that some messages will be less informative (or less constrained by the schema), and the exact correspondence with the old PGEmacs protocol is lost. But it should make the specification easier to understand and implement.


  • proveroutput: removed <proofstate> and <cleardisplay> messages.
    • proof state output can be distinguished by its content in PGML and destination window
    • windows can be cleared by sending a message with empty PGML
    • functionality lost: ability to clear all windows with a single message

  • <normalresponse> and <errorresponse> have been simplified:
    • removed messagecategory attribute (merge with displayarea in )
    • removed urgent flag (functionality currently lost: ability to "raise" a window to alert the user)
    • display area (i.e., window name) attribute moved to

  • <pgmltext> merged with <pgml>
    • area attribute added, with additional possibilities tracing and internal (from old messagecategory)
    • functionality lost: user-level debug messages (use tracing instead)
    • Note: systemid and version are not normally expected to be filled by prover (may be added by broker in relaying to display or other components)

Please check the latest CVS versions of the schemas for details. Some more changes are likely in the next few weeks, coinciding with some improvement in markup produced by Isabelle, as well as discussions about PlatoAndProofGeneral. This section will be updated as that happens to summarise changes since 2.1. Please bear with us as the documentation may lag for a while. If you have any suggestions now would be a good time to make them!

Major revision of PGML, version 2.0

The PGML schema has been completely rewritten, simplified and enhanced. It now provides support for:

  • pretty-print annotations, partly inspired by BoxML. PGML output is no longer assumed to be precise concrete syntax.
  • annotations for decoration, including fonts or colouring for information/warning/error on subterms.
  • annotations for actions: button, menu, or toggle (fold)
  • placement directives for subscript, superscript, above and below
  • a richer symbol configuration mechanism, encompassing (and extending) the symbol editor provided in PG Eclipse

PGML is still intended to be a lightweight markup mechanism rather than a complete page/math layout language. But it now also allows other XML formats to be embedded (e.g. MathML ).

The somewhat system-specific aspects relating to particular outputs of the prover state (, etc), have been removed. Nonetheless, provers should continue to provide this kind of lightweight semantic markup on displays, but using the general kind and param attributes of the element instead.

Remove individual elements for prover flags, harmonise as setproverflag.

[Rev 3.35] Remove deprecated elements: startquiet, stopquiet, pgmlsymbolson, pgmlsymbolsoff, in favour of setproverflag with attributes quiet or pgmlsymbols.

This reduces the number of cases in the prover protocol, while making prover flags easily extensible. Note that prover flags are intended as flags that have a known effect in the prover and are controlled by the interface, not usually the user. This is the opposite to prover preferences, which can be set by the user via the interface, but are usually not adjusted programmatically. No assumptions about particular preferences are made. Preferences are also more general than (only boolean) flags.

The known flags will be extended with categories for requesting meta-information in responses. The first of these is metainfo:thmdeps. When this flag is set, the prover should report theorem dependencies, if it can.

Unimplemented flags should generate an error response.

-- DavidAspinall - 21 Jun 2007

Topic revision: r7 - 11 Jul 2007 - 10:30:36 - 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