Interface Concepts (Glossary)

please help extend this glossary

This page introduces some of the terminology used in the Proof General documentation.

Theorem Prover

A tool for constructing machine-assisted formal proofs. See SupportedProvers for details on the provers supported by Proof General.

Script Management (aka Proof Scripting)

Interactive increpemental processing of proofs, similar in spirit to interactive step-debugging. Usually tailored to linear scripts. Definitions and proofs are contained in ProofScripts which are held in files. These scripts can be interactively 'executed', by sending them to the prover line by line. Proof General has tape-recorder style buttons which can be used to move the point of next-execution through a script. This is called proof scripting. It helps you to develop and debug proofs.

Locked Region

As you process a script, it becomes locked. Locked regions cannot usually be edited. This is a feature of Script Management that protects against breaking a proof by editing earlier sections/theories. To unlock locked regions, use the ''goto'', ''undo'', ''retract script'' or ''restart prover'' commands as appropriate.

Advanced users who want to allow editing of locked regions (risking loss of synchronisation) can set an interface option to allow this.

PGIP

The communication protocol used by Proof General to work with the prover. This was designed by abstracting from the protocol used in the original ProofGeneralEmacs, and unifying differences exhibited by different theorem provers. See: PGIP.