Alternative Undo Models in PGIP

At present, the behaviour of undo inside the theorem prover is understood by the PGIPBasicProverModel. The idea is that a prover should present this model to the interface so that it can be controlled in a uniform way. Markup on the proof script indicates the structure of the script and the undo behaviour at the same time.

But a frustration is that mapping this behaviour onto the prover's underlying control structure may limit the ways it can be controlled (e.g., Matita can undo to any position, it does not discard state). We have argued in the past that limitations like this are a reasonable price to pay for genericity, but it would be good to do better.

Here are some notes on recent discussions about this (at MKM 07 and elsewhere).

-- DavidAspinall - 11 Jul 2007

Specifying a Prover Meta-Model

To generalise PGIPBasicProverModel, we might allow the prover to specify its own state transition model which describes the undo behaviour, and, ideally, also a model of static identifier scoping in the language.

This would form a ProverMetaModel . For more (but not yet the whole story), see notes in PGIPVersionThree.

Letting the Prover Tell Us What it Did

The idea here is that the interface controls the prover by sending an undo command, and then the prover responds to say what it actually did. Implications:

• There is no need at all for a meta-model or for the interface to "calculate" undo commands
• Prover and interface must communicate positions (with identifiers or line/characters).
• The prover must record these positions during script management
• The interface loses any predictability about the effect of an undo command. This is bad for advanced behaviours (think: programmatic control of the prover, which has already been done in PGIP), or for giving an indication to the user of what the effects of an undo command may be (e.g. to protect them against accidently undoing something that make take 10 minutes to re-check).

This scheme is implemented by Coq for at least one of its interfaces (FIXME: which one?) and was argued for by CezaryKaliszyk .

Getting the Prover to Tell Us What it will Do

The idea here is to add some additional markup to the proof script which indicates what the target position of an "undo to here" command would be at each position. The technical problem is that the target position depends on where you came from, as well as where you try to go to.

Roughly, we might have markup like this:

<comment id="1" undotarget="1">...</comment>
<opengoal id="2" undotarget="2">lemma foo: ...</opengoal>
<proofstep id="3" undotarget="4-5:3,*:2">apply...</proofstep>
<proofstep id="4" undotarget="5:4,*:2">apply...</proofstep>
<closegoal id="5" undotarget="2">qed</closegoal>
<comment id="6" undotarget="6">...</comment>

Something like this scheme is implemented by Coq for PGEmacs (see CoqHistoryMechanismNotes), but using a custom markup on the prompt which still requires some calculation in the interface.

This scheme doesn't require a meta-model, and doesn't sacrifice predictability in the interface. But, because we've concealed the underlying structure in the prover, things are less predictable, and the markup becomes more complex.