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:
- We allow nested proofs by successive ProofOpen commands, giving ProofOpen(depth) states
- For efficiency, we allow the prover to implement richer history mechanisms
Exactly how this is specified/implemented is currently under discussion, see
PGIPDevelNotes.
References