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.

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.

- AddingPGIPSupportHowTo
- PGIPCommentary
- See UITP03 [FIXME]

Edit | Attach | Print version | History: r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions

Topic revision: r2 - 22 Aug 2006 - 13:41:13 - DavidAspinall

Copyright © 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

Ideas, requests, problems regarding TWiki? Send feedback

This Wiki uses Cookies