Notes on the Coq undo and syntax mechansims

REFACTOR reformat

From email discussion with PierreCourtieu :

On Fri, 25 Aug 2006 17:38:59 +0100 David Aspinall <David.Aspinall@ed.ac.uk> wrote:
> > Hi Pierre,
> > 
> > ...
>>> > >> Eventually, the way I would like this kind of thing to go is to make the 
>>> > >> configuration of such a table from the prover, so that the code can be 
>>> > >> maintained there.  There is already some provision for this kind of 
>>> > >> thing in PGIP.  Do you think that makes sense or is possible here?
>> > > 
>> > > Yes it make sense but this will be as hard to maintain for coq team as
>> > > it is for us now I am afraid.
> > 
> > Really -- because apart from key presses & documentation, the syntax at 
> > least would already be defined in Coq and could be used to generate the 
> > table entries, I would have thought?   This turns out to be a nightmare 
> > in Isabelle because there is no fixed syntax (nor parse trees) even for 
> > the "outer" proof scripts syntax.  But I know in Coq there is a parser 
> > module.

Well syntax is extensible, so the set of all keywords is spread all
over the source files. There is a basic syntax table that can be output
easily but not all of it.

> > OK, thanks.
> > 
>>> > >> You described to me last time how it works in PG 
>>> > >> but I wonder how it relates to the PGIP "prover model" described here:
>>> > >>
>>> > >>    http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGIPBasicProverModel
>> > > 
>> > > I don't see in the wiki how the provers gives information to the
>> > > interface on "how to come back here". But this should be part of the
>> > > protocol (is this part of the "meta information").
> > 
> > It's implicit in the protocol by the idea that we have different 
> > commands for exiting a proof (abort goal), and undoing steps inside a 
> > proof (undostep).  So at the moment PGIP expects to calculate the undo 
> > command itself to go to a particular position --- it was after all based 
> > on the way that PG worked.  But it needs extending to cover the case 
> > where the prover is helping out and maybe has a richer history mechanism 
> > than basic LCF style.

It is not possible with coq for two reason: one can define new commands
(in caml) and new tactics (in coq or caml) and so PG cannot know what
to do to come back there (unless replaying arbitrarily large parts of
the script).

> > I haven't understood a couple of things:
> > 
> > Can you backtrack to any position now with the Backtrack command, or 
> > will it sometimes be necessary to go further than the user wanted 
> > (aborting proofs)?

I am not sure of what you mean. closed proofs/sections and modules
cannot be reentered, you need to reset and replay them. This is a
limitation of coq which deletes (really) things after a Qed/End.

Apart from that Backtrack x y z can go anywhere back in a file. Provided
there was no suspend/resume (not allowed in PG). There is no need of
replaying any line of the script. It is so simple to backtrack now,
here is the core of find-and-forget (span is the span we want to go
back to):

  (let* 
            (proofdepth (coq-get-span-proofnum span)) ; proof stack depth to go back to
            (proofstack (coq-get-span-proofstack span)) ; list of open proofs to go back to
            (span-staten (coq-get-span-statenum span)) ; global state number to go back to
            (naborts (count-not-intersection current-proofstack proofstack)) ; list of proofs to abort
            )
    (setq ans
            (format "Backtrack %s %s %s . " 
                    (int-to-string span-staten)
                    (int-to-string proofdepth)
                    naborts))

that's all! No need to look at what is written in the buffer!!
The Information given by the prover (and stored in spans) is
sufficient. This way I don't need to know what is a command, what is
a tactic or whatever. Actually I need it to font-lock and indent, but
not for backtracking (which is critical).


> > Is it possible to go forwards as well (i.e. redo)?

no, scripts must be replayed. Coq lack such a mechanism, and I don't
know how PG (even via PGIP) could do so, storing environment seems
difficult. What do you mean actually?

>> > > The ideal would be that after each command, the prover send the exact
>> > > command one should need to come back to it. This is almost the case
>> > > with coqtop -emacs, except that when backtracking we still have the
>> > > number of proof aborts to compute.
> > 
> > Maybe this answers my question above but I'm not sure.  Probably I need 
> > to play with an example that has nested proofs.

When a proof is finished, the term defined by it is stored in the
global environment (changing the state number). So they are dealed with
exactly as normal Definitions.

All unfinished proofs names are stored in each span, so it is easy to
guess how many "abort" are needed. quoting coq.el (read with fixed
width font):
 
;; Simplified version of backtracking which uses state numbers, proof
;; stack depth and pending proofs put inside the coq (> v8.1) prompt.
;; It uses the new coq command "Backtrack". The prompt is like this:
;;      state                        proof stack
;;      num                           depth
;;       __                              _
;; aux < 12 |aux|SmallStepAntiReflexive| 4 < 
;; ^^^^^^   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^     ^
;; usual           pending proofs           usual 
;;                                          special char
;; exemple:
;; to go (back) from 12 |lema1|lema2...|leman| xx
;; to                8  |lemb1|lemb2...|lembm| 5
;; we must do "Backtrack 8 5 naborts" 
;; where naborts is the number of lemais that are not lembis


>> > > Actually IMHO the synchronizing system should not depend *at all* on
>> > > the syntax recognition of PG. Syntax recognition is for colorizing and
>> > > indenting (as these are not critical) only.
> > 
> > I agree to some extent, but the idea of PGIP is to "categorise" commands 
> > to explain the structure of the script to the interface (in PGIP we ask 
> > the prover to do this precisely and accurately by adding markup like 
> > <opengoal> <closegoal>,etc, rather than recognising with regexps).  It 
> > seems useful to have this structure even if it's not used for undo 
> > calculation.  For example, for folding, searching headers, etc.

I agree with that, and for indentation as well (which is some kind of
searching headers). But these are less critical and may be slightly
wrong/inaccurate/not up to date. Backtracking cannot be wrong at all,
or we may lose users instantly.


This topic: PG > PGIP > PGIPDevelNotes > CoqHistoryMechanismNotes
Topic revision: r1 - 27 Sep 2006 - 11:04:41 - DavidAspinall
 
This site is powered by the TWiki collaboration platformCopyright © 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