Older changes to PGIP

This file provides some description of changes in the PGIP schema.

Names and types for blocks in document

The <openblock> element has two meanings: one for purely layout (optional name of sub-block has been added), and the other to indicate document replacement positions, using the metavarid attribute to name a position for communicating back to the prover. The new objtype attribute allows for interface-driven replacement, using the interface operations. This is a step towards unifying the facilities of PGML for output and the document text.

-- DavidAspinall - 16 Dec 2006

Unit type added to configuration types: <pgipnull>

The new unit type <pgipnull> has the unique element which is the empty string. The string type <pgipstring> now admits all non-empty strings.

These types are used for configuring user dialogs, at the moment, just for user preferences. The empty element can be used to represent the absence of a preference setting.

In future we need to also allow objtypes in dialogs, but perhaps only identifiers. A possible addition is <pgipid> with a given objtype (not yet added).

-- DavidAspinall - 04 Dec 2006

PGIP configuration specifies supported attributes as well as elements

<acceptedpgipelems> configures the PGIP commands which can be received by a component. The attributes attribute for <pgipelem> allows to give a list of attributes which are supported by the elements Only optionally-supported attributes need to be given, and only where they may alter the form of the message exchanges: an example is the <times> attribute mentioned below.

-- DavidAspinall - 02 Dec 2006

Multiplicity added to undo/redo commands: <times> attribute

This optional attribute allows a minor efficiency improvement in the protocol, if the proof assistant can undo several steps in one go.

-- DavidAspinall - 02 Dec 2006

Document comment markup added

A new PGIP mark-up element <doccomment> has been added.

This is used for marking up literate comments at the level of proof scripts. These document-level comments may have a semantical effect in the prover, although usually not during normal proof, but for other purposes (e.g. Java doc style comments). In script management, these comments are passed to the prover, but ordinary <comment> elements may not be.

It is safe to classify all comments as one thing or the other. Isabelle has a well-defined notion of document comments which have separate keywords and markup, so it is useful to reflect this in the interface.

Note that PGIP has its own notion of literate commands which are marked up by <litcomment>. These are not passed to the prover and should never be returned by a prover's implementation of <parseresult>. These elements are used to construct a master document format which embeds other information inside proof script files.

-- DavidAspinall - 22 Nov 2006

Retract file added

An operation <retractfile> to retract files has been added. This was present in Emacs Proof General but missed out from the PGIP operations before now. It is valid only in the top-level state of PGIP (see PGIPBasicProverModel). In Isabelle, this interfaces with the internal theory loader: a retraction operation removes a file (i.e. the theory it contains) from the proof context. In Isabelle, dependent files are automatically retracted and informfileretracted messages are sent to tell the interface.

For other provers, informfileretracted can be omitted and Proof General can send retraction commands for child files automatically (albeit after the parent has been removed). This behaviour for other provers isn't yet well exercised.

At each level in the PGIP model we have a subset of these operations available:

  • do: process a step at this level, possibly with history in prover;
  • undo, redo: history operations in prover;
  • abort: jump to parent level, discarding history of this level;
  • retract: undo a named target (perhaps using logical dependencies, then history effect is undefined).

-- DavidAspinall - 22 Nov 2006

Datatype fixes

For tools which use the schemas (xsd/rng files), the basic datatype choices are important. I've tuned these to use the three basic types more accurately:

  • text --- for element content that may contain nested nodes / mixed content
  • string --- for attributes or element content that we only want to extract literal strings from, preserving whitespace.
  • token --- for attributes or element content that we want to extract tokenised strings from, collapsing/normalising whitespace.

Note that the token type does allow spaces, it is different from NMTOKEN in DTDs. It is a reasonable choice for our own identifiers, although for prover identifiers we allow string because we can't expect/dictate that they will collapse multiple spaces. Because XML 1.0 parsers will collapse whitespace in attributes, token (or restrictions of) is the usual choice for attribute content. When string is used instead, the XML document must escape newlines, etc, for them to be preserved in attributes.

For more information, see the relax book here: http://books.xmlschemata.org/relaxng

-- DavidAspinall - 26 Oct 2006

PGIP document type: pgipdoc and metainfo elements

I've added a PGIP document type which looks like this:

   pgipdoc = element pgipdoc { (properscriptcmd, metainfo*)* }

That is, a document is a sequence of script commands, each of which may be followed by any number of meta-information elements. Meta information elements =metainfo= allow any content and have an optional name attribute. We may add other optional name attributes in future, as well as describing specific possible choices of meta-information.

The idea is that a pgipdoc element is reasonable model of a proof script in memory that might be used directly by displays. Parsing is allowed to return metainfo elements or they may get added by <metainforesponse> messages. The newobj message may need a bit of tweaking to handle this.

-- DavidAspinall - 26 Oct 2006

Topic revision: r2 - 30 Jun 2007 - 20:41:39 - 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