*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

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