PGIP Basic Model of Incremental Development

PGIP understands that the theorem prover may be in one of four possible states while incrementally processing a proof script. Commands issued to the prover can cause it to move between states. These commands are split into proper commands (shown in blue below), which can appear in scripts, and improper commands (in red italics), which should not.

Proper commands are categorised by the prover into OpenFile, ProofStep, etc, on parsing the proof script. Improper commands are implemented by the prover directly as PGIP control commands.

• PGIP abstraction of the prover's state:
  

PGIP's model of the prover state is abstracted from the way most of the LCF-style provers we use operate. Typically:

• Different types of proof command are available in the different states
• Local undo history for proofs is stored in the Proof Open state, but discarded when that state is left.

To support PGIP, a prover has to present this model to Proof General. Note that this does not mean that the prover must match the model exactly (e.g., internally it may not really have separate Top Level and File Open states).

Using this model internally also does not limit what the interface presents to the user. For example, Proof General can simulate a richer history behaviour than the prover allows by simulating undo-redo into proofs-in-progress. It does this simpy by caching responses from the prover.

If we simulate undo into proofs like this, when a forward step is taken which is different from one taken in the past, then Proof General will have to commit to undo to a point further away in the proof script and re-process up to the point of the change. This is potentially expensive which is why ProofGeneralEmacs did not implement it, although the behaviour that the user sees (undo makes large jumps over completed proofs) is counterintuitive at first sight.

Elaboration and configuration of the basic model

The basic model above is implemented by ProofGeneralKit, but we allow some extensions:

1. We allow nested proofs by successive ProofOpen commands, giving ProofOpen(depth) states
2. For efficiency, we allow the prover to implement richer history mechanisms

Exactly how this is specified/implemented is currently under discussion, see PGIPDevelNotes.

References

• AddingPGIPSupportHowTo
• PGIPCommentary
• See UITP03 [FIXME]