From 8c8022663ef3cd5dbbee064cbd9ffd5be7d7eb4d Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 24 Sep 2003 22:36:42 +0000 Subject: Updated from Kit repo --- html/Kit/dtd/pgip.dtd | 733 ++++++++++++++++++++++++++++++++------------------ html/Kit/dtd/pgml.dtd | 147 ++++++---- 2 files changed, 571 insertions(+), 309 deletions(-) diff --git a/html/Kit/dtd/pgip.dtd b/html/Kit/dtd/pgip.dtd index cb28e77d..8210331d 100644 --- a/html/Kit/dtd/pgip.dtd +++ b/html/Kit/dtd/pgip.dtd @@ -1,376 +1,593 @@ - + - + +%pgml; + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - The kitconfig messages are sent by the Prover, in response to - proverconfig messages. These messages describe the Prover's - preferences and object structure. + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - - - - - - - - + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + - - - + %name_attr;> - - + - - + + path CDATA #IMPLIED + name CDATA #IMPLIED> - - - + path CDATA #IMPLIED + name CDATA #IMPLIED> - - - - + - - - - - + + + + + + + + + + + + + - + + + + %name_attr;> - - - + - - - + + + + + + + + + - - - - - - + + + + - + %name_attr;> - + + - - + - + - + - - + - - - + - - + - - + + + + + + + - + + - - + + - + - - + - + - + + + - - Messages to the prover: + - : open a goal: text is theorem to be proved, in ambient context. - : a specific proof command (perhaps configured via opcmd) - : undo the last proof step issued in currently open goal - : give up on currently open proof, close proof state & discard history - : complete & close currently open proof (succeeds iff goal proven) - : close currently open proof, record as proof obligation - : forget a theorem (or named target), outdating dependent theorems - : re-open previously postponed proof, outdating dependent theorems + - Notes: - 1. As a later option, the prover provide a way to retain undo history - across different proofs. For now we assume it does not, so we must - replay a partial proof for a goal which is postponed. + - 2. We assume theorem names are unique amongst theorems and - open/goals within the currently open theory. Individual proof steps - may also have anchor names which can be passed to forget. + + - 3. The interface manages outdating of the theorem dependencies - within the open theory. By constrast, theory dependencies are - managed by the prover and communicated to the interface. + - FUTURE TODO: expand this model to allow nested proofs. ---> + + - - - - - - - - + + - - - - + + - + + - - Command messages sent to the prover: + + - : load a file possibly containing a theory definition - : begin construction of a new theory, with optional ancestors - : complete construction of the currently open theory, - saving it in the promised file. - : retract a theory. Applicable to open & closed theories. + - : lock a filename for constructing a proof text - in the interface. The prover may check that the - opened file does not already correspond to a processed - theory. + - : unlock a filename, possibly suggesting to the prover it has been - processed completely (but incrementally via interface). - A paranoid prover might want to check the file - nonetheless. + - PGIP supposes that the interface has only partial knowledge about - theories, and so the interface relies on the prover to send hints. - Specifically, these messages may be sent *from* the prover: + - : inform the interface that a theory has been read. - : inform the interface of a removed theory. + - When the interface asks for a theory to be loaded, there may be - a number of responses from the prover, - and similarly for retraction. ---> + + + + + + + + + - - - - - + + - - + + - - - + + - - + + + + + - - + + - - + - + - + + - + - + + + + + + - - 2. The model only allows a single open theory. Although PGIP - assumes this, it may be possible for the interface to provide - extra structure and maintain an illusion of more than one open - theory. But we do not expect the prover to implement this - directly. (Later on we might allow the prover to do so and provide - extra efficiency help, e.g. to avoid too much proof replaying.). + - TODO: extend the above with standard theory operations, perhaps. - (or these may be configurable) - --> + + + + - + - - + - - + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + diff --git a/html/Kit/dtd/pgml.dtd b/html/Kit/dtd/pgml.dtd index d484c100..fbdd9f7d 100644 --- a/html/Kit/dtd/pgml.dtd +++ b/html/Kit/dtd/pgml.dtd @@ -1,75 +1,120 @@ - + - - - + - - +RELAX NG Schema for PGML, the Proof General Markup Language +Authors: David Aspinall, LFCS, University of Edinburgh + Christoph Lueth, University of Bremen +Version: pgml.dtd,v 1.12 2003/09/23 23:17:18 da Exp - - +Status: Complete but experimental version. - - +For additional commentary, see the Proof General Kit white paper, +available from http://www.proofgeneral.org/kit - - +Advertised version: 1.0 - +--> + + + + + + + + + + + + + + + + + + + + + + + name CDATA #IMPLIED + kind CDATA #IMPLIED> - + + name CDATA #IMPLIED + kind CDATA #IMPLIED> - + + name CDATA #IMPLIED + kind CDATA #IMPLIED> - - + + - + + name CDATA #IMPLIED + kind CDATA #IMPLIED> + + - - + + - - - - + + + + + + + - + + + + + + + + + + + + - - + - + + + -- cgit v1.2.3