PGIP Development

This page is intended for discussion on PGIP development. Once robust/tested, material here should be moved elsewhere, e.g.:

IDEA! Please refer to the version of the protocol under discussion by the CVS version of Kit/dtd/pgip.rnc you're looking at.

See also

Adding fine-grained specification of undo behaviour

See PGIPBasicProverModel (more to be said here).

See CoqHistoryMechanismNotes.

Adding proof-by-pointing style protocols

What we mean by PBP-style protocols is where this user interaction sequence happens:

  1. User selects (e.g. by mouse hover) a region from the input (proof script) or output (goals display)
  2. Interface sends selection to the prover (or agent acting for the prover)
  3. Prover offers some list of choices (or perhaps a single default) based on the selection
  4. User selects from list, causing a command to be sent back to the prover, possibly after inserting into the script.

It seems like this could be supported (from the prover's point of view) by adding a special kind of opcmd which returns some (ready-parsed) sequence of alternative commands for selection by the user.

Completing <lexicalstructure> configuration

The element allows to specify the lexical syntax of proof scripts for the purpose of syntax highlighting, etc. This is a thorny area: most generic solutions seem to eventually suppose programmability. For now we follow an Emacs-like scheme.

Completing menu configuration

There are some placeholder messages for configuring prover-dependent menus, or perhaps menus contributed by other PGIP components.

These should probably be completed and fully specified. But we may apply a wait-and-see approach to see whether they are really needed. We may get enough mileage from the help and setting menus which are already built in and configurable.

Refining meta information responses

The idea of the metainforesponse message is to return some meta-information after a proof step has been executed, which is (conceptually and perhaps actually) added to the PGIP markup on the proof script.

An example is dependency information: the prover can proactively tell the interface what other elements a recently processed step depends on. This enables the interface to display dependencies, or make use of them e.g. by allowing the user to safely move around parts of the script.

Adding prover-enabled dialogs

The opcmd mechanism allows some dialogs to be displayed to the user.

But it might be useful if we extended PGIP so that the prover could be programmed to offer the user choices via dialog and input boxes.

This needs careful thought for at least a couple of reasons:

  1. it requires more direct coupling with user-interaction than we assume: we would need to synchronise with user somehow.
  2. it is likely to cause stylistic chaos

Summary: it's probably best to wait until we have a compelling need.

Modularisation

It would be good to split up the big scheme into at least three subschemes, specifying the PGIP sub-protocols modularly:

  • the display protocol between broker and display,
  • the prover protocol between broker and prover,
  • the internal protocol between communicating brokers,
  • and of course the basic stuff which is common to all three.

The advantage is prover developers do not have to worry about all the funny display messages etc.

On locations in messages

At the moment, Isabelle doesn't add any location information to error messages --- but it should be modified to do this in the case of automatically loaded included files. (This would just reflect the information that is displayed in the error messages themselves, and parsed in Emacs by some regexps).

For scripts which are fed line-by-line to Isabelle, it seems easiest for the broker to add this information to the error message sent by Isabelle, since it knows where the error occurred. (Alternative would be to feed this in to Isabelle to get it back out again, but seems not much point!)

As well as file locations, we could add locations which specify objects (and source ids). The broker would have to do this. This would be useful for the graphical display (it doesn't know that files have lines). It would also be useful for the textual displays, even for normal responses. For example, the Eclipse front end has a view for proof state messages which has a history. It would be nice if browsing this history automatically moved the user to the location in the source file which corresponded.

In this last case, there is a risk that the object may no longer exist if it has been edited and reparsed --- but the display can set a marker in the source file which corresponds to the position at the time it received the message, instead. The marker may move around with the text (or may get deleted altogether, in which case we give up).

Clarification/documentation of message display model

We need to document the assumptions and behaviour that occurs in the present PG. Here are some notes about that to ponder, until we find a better place to put them.

Roughly, the UI design idea is that the user should normally only need to see the most recent message displayed to make sense (so we can have the two window interaction mode). But the markup allows different display areas to be specified: typically, the persistent display area used for goals, and the intermittent display area used for other messages.

Apart from these two, we also allow status line messages for brief informational messages (e.g. "File saved"): it shouldn't matter much if these are not seen by the user.

The existing PG uses a filtering strategy on possibly voluminous output from proof assistants. If no "urgent" messages (errors or warnings) are seen, then the system will wait for the message and then display the last proof state output before that. The idea here was to not bother repeatedly update the display with any intermittent proof state messages. But we needed to add a further optimisation, because in the case of a large queue of commands being sent to the prover, we could be more efficient to disable the prover from producing output until the last command was sent anyway. This is the purpose of the <startquiet/> and <stopquiet/> prover control messages.

Fresh parsley and other herbs: the object state model

It turns out that our UITP 2005 paper doesn't really define enough states for objects, at least from the display's point of view:

cst.jpg

The most precise distinction is as follows.

First, we have these states for parsing:

  1. unparsed
  2. being parsed
  3. unparseable
  4. parsed

and for proving, we have analogous states:

  1. unproved = parsed
  2. being proved
  3. unproveable
  4. proved

(At the moment, we don't bother record/indicate the unproveable state, but put unproveable=unproved again). Probably the display doesn't need to graphically indicate the "being parsed" state (because parsing should be quick).

The display might --- like Eclipse does (roughly) for Java code --- display the "unproveable" and "unparseable" states in a similar way, with wavy underlines.

This object state model concerns the display mainly: the original smaller set of distinctions (plus different methods of distinction) is fine for the broker. We leave it to the display to make the finer distinctions above. Specifically, the broker doesn't model these states for objects:

  • being parsed
  • unproveable

So it will not inform the display about changes for these transition.

The display may deduce that some proof command is unprovable by the location attribute in an error message specifying that object as the location of the error. The display may want to add an error marker in this case: although it should be careful to remove it at some point when it may be no longer relevant.

Some use cases for editing

Let's discuss SomeUseCasesForEditing somewhere else.

Notes about dependencies

We have some blackboard screenshots somewhere to write up!

Some interesting remarks made in a DReaM talk

  • Jacques/Ian: Does the statement of a theorem depend on its proof? Probably not (except maybe in logics where we may be interested in extracting proofs). But at the moment it's not possible to change a proof without outdating the theorem itself --- this would need prover support to do "proof patching" (non-DReaM usage) to replace proofs. Also note this would affect dependencies.

  • Remark by Ian/James that we might not have to rely on theorem prover for informing us of dependencies, we could experimentally discover them!! See related work on Searching for ML Type-Error Messages by Benjamin Lerner, Dan Grossman and Craig Chambers at http://gallium.inria.fr/ml2006/program.html

  • Alan (not related to dependencies): could we have the broker support some kind of translation between provers -- or even asserting (translated) statements in one prover that have been proved in another? To do this safely we would need a careful soundness argument.
Topic revision: r11 - 11 Jul 2007 - 11:43:47 - 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