Retracting, editing, then re-evaluating/proving sometimes results in definitions that do not match the contents of the file

[coquser]

I'm not sure whether this is a bug in Coq, or in Proof General.

Given the following file*:

Require Import Program Omega Bool.

Lemma bar : 128 * 128 + 128 = 16512.
  compute; trivial.
Qed.

Lemma baz : 128 * 128 + 128 = 16512.
  compute; trivial.
Qed.

Lemma qux : 128 * 128 + 128 = 16512.
  compute; trivial.
Qed.

Lemma foo : forall x : Type, x = x.
  auto.
Qed.
Print foo.
Print foo.

Tell Coq to evaluate the entire thing, then, after it evaluates the [Require Import], tell it to not evaluate [foo] (ctrl + c, ctrl + enter on the [Lemma foo] line), then quickly change [Type] to [nat] before it finishes the proof of [qux], and then tell it to evaluate down to [Print foo], again. When I [Print foo], it shows the original definition (with [Type]), rather than the new definition (with [nat]).

*This will only work on a sufficiently slow computer with a sufficiently fast person. You may need to add more filler theorems, or increase the size of the numbers, so that it slows down enough to change the word before it gets there. I'm doing this in emacs (GNU Emacs 23.1.50.1 (i386-mingw-nt6.1.7601) of 2009-11-03 on LENNART-69DE564 (patched)) running Proof General (Version 4.1), and I have an HP running Windows 7 x64 with 4 GB of RAM and an AMD Turion(tm) X2 Ultra Dual-Core Mobile ZM-87 2.40 GHz.

[coquser]

Hi,

my first guess is that this is an error in proof general's parser cache. Could you try the following?

1. To make sure it is a proof general bug: Look into buffer *coq* after you reproduced the problem. Search for foo there and see if proof general sent Type or nat to coq.

2. M-x customize-variable proof-use-parser-cache, set it to off (nil) and set for the current session. Then try to reproduce your problem.

Bye,

Hendrik

[coquser]

OK... tried it myself:

1. it is a PG problem, *coq* contains the wrong text

2. problem persists when proof-use-parser-cache is off

I used 8 of those lemmas to have enough time. What I see is even more strange:

First I do C-c C-b with follow-mode off. This colors everything in pink, the whole buffer is in the queue region. The locked region starts to grow slowly.

Then I do C-c RET on foo. But now not only foo moves out of the queue region, pink completely disappears, suggesting that the queue region is empty.

Nevertheless the locked region continues to grow and eventually covers the whole file, without that I reassert foo again.

This suggests that the original span for foo is never removed from proof-action-list. A simple

(mapc

'(lambda (action)

(message "AL : %s" (cadr action)))

proof-action-list)

inserted in proof-shell-exec-loop confirms this. So the problem seems to be that items are not taken off proof-action-list when shortening the queue region.

Bye,

Hendrik

[coquser]

When I reported this to Coq (​https://coq.inria.fr/bugs/show_bug.cgi?id=2833), the marked it as "resolved, won't fix", and said: You cannot tell ProofGeneral to "not evaluate" a command that has been put in the queue. The bug is that from a user perspective, one can think that hitting ctrl-c ctrl-enter at that moment does that, but it doesn't. Indeed the queue seems to be emptied (the queud region becomes white again) but it is not.

This misleading display is deeply linked to the proofgenral achitecture. I don't think it is worth fixing it. Plese just keep in mind it is not possible to remove things from the queue (unless you interrupt coq with ctrl-c ctrl-c). You can only backtrack after the commands are finished.

Best regards, Pierre

[coquser]

You cannot tell ProofGeneral to "not evaluate" a command that has been put in the queue. The bug is that from a user perspective, one can think that hitting ctrl-c ctrl-enter at that moment does that, but it doesn't. Indeed the queue seems to be emptied (the queud region becomes white again) but it is not.

I don't agree here with Pierre. It should be quite easy to remove elements from proof-action-list. The question is of course, if one really wants to implement this for the rare case that some user quickly changes his mind.

This misleading display is deeply linked to the proofgenral achitecture. I don't think it is worth fixing it. Plese just keep in mind it is not possible to remove things from the queue (unless you interrupt coq with ctrl-c ctrl-c). You can only backtrack after the commands are finished.

Again, I don't agree. The UI should be consistent. Either it changes the color and correctly removes the stuff from the queue region or it should not change the color and prevent the user from changing text in the queue region.

Hendrik

[David Aspinall]

Thanks for the bug report and investigations.

I agree with Hendrik that this is a bug that ought to be fixed because it leads to inconsistency.

But Pierre is right that this use case goes beyond the original PG simplistic queue management, which originally did not allow any UI steps forward/back once a queue was in progress, except to interrupt. Later I relaxed this to allow advancing the queue (it's easy to add more items), but I thought retraction was still forbidden (it's a bit trickier to do removal from the queue, even if only to avoid the item currently being processed).

So I am surprised that C-c C-RET is allowed in the above case, I thought it would trigger a UI beep/busy message.

Maybe some recent changes elsewhere for the multiple file handling inadvertently opened up this behaviour? It might be worth checking what happens in PG 4.0.

[coquser]

So I am surprised that C-c C-RET is allowed in the above case, I thought it would trigger a UI beep/busy message.

OK, then I suggest to fix this problem by forbidding C-c C-RET in the queue region.

Hendrik

[coquser]

It might be worth checking what happens in PG 4.0.

4.0 does not have this problem, but 4.1 does.

Hendrik

[coquser]

The error was introduced with commit "Fix for Trac #397. Needs some exercise." (​http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/ProofGeneral/rev/82279241c069) where the call to proof-shell-ready-prover was moved. As I learned now, proof-activate-scripting used to have the undocumented feature of aborting proof-retract-until-point if proof-shell-busy is not nil.

I am quite happy that the patch that I proposed for #397 would not have introduced this problem. But I was not aware of this when I tried to analyze the differences between Davids and my patch. ;-)

As the undocumented feature was a bad idea, I fixed this by adding a separate call to proof-shell-ready-prover to proof-retract-until-point.

[BTW, there are more issues with rce2log: (1) it is not in PATH in Debian any more (hidden in /usr/share/cvs/contrib), (2) the generated ChangeLog? does not contain the commit mentioned above.]

Hendrik

[David Aspinall]

Thanks for the analysis and fix. I think this undocumented behaviour fell between the gaps when the queuemode flags were being added.

It looks as if the single proof-activate-scripting call already in proof-retract-until-point ought to be able to do the job if the 'retract flag is added (not sure why it isn't set there). But that might require adding the failure points more clearly in proof-shell-ready-prover (e.g. don't allow retract if retract is in progress).

On the rcs2log, I added a path setting to Makefile.devel. When I run make ChangeLog with no ChangeLog? file, I do see the commit mentioned above (2011-04-26).

[coquser]

It looks as if the single proof-activate-scripting call already in proof-retract-until-point ought to be able to do the job if the 'retract flag is added (not sure why it isn't set there).

I don't believe this. The call to proof-shell-ready-prover is inside the unless in proof-activate-scripting, it is not executed, when you retract in the current scripting buffer.

On the rcs2log, I added a path setting to Makefile.devel.

Actually, I wanted to say "It's not in PATH in Debian TESTING WHEEZY any more..." In Debian stable squeeze its of course /usr/bin.

When I run make ChangeLog with no ChangeLog? file, I do see the commit mentioned above (2011-04-26).

Interesting, here it is

2011-04-27  Hendrik Tews  <hendrik@askra.de>

    * coq/coq.el: update Hendrik's personal issue list

2011-04-26  David Aspinall  <da@inf.ed.ac.uk>

    * coq/coq-autotest.el: Fix compile

    * coq/coq-autotest.el: Fix so that make test.coq runs successfully.

    * coq/coq.el: Clean up some defcustom docstrings (remove *'s)

2011-04-15  Hendrik Tews  <hendrik@askra.de>

    * coq/coq.el: * fix coq-show-first-goal changing the current buffer

    * coq/coq-syntax.el, coq/coq.el:
    * fix overwriting setq coq-prog-name before loading Proof General
    * more complete callback listing in proof-action list doc

which only vaguely resembles the history.

Hendrik

[David Aspinall]

rcs2log makes a mess of things. I have two entries for the same date, if you find the second one, it includes the changes in coq/ as well as others including this

   * generic/proof-script.el: Fix for Trac #397.  Needs some exercise.

re: p-a-s, I use "ought" to mean that it would be desirable if it would do that. I gathered by your change that it doesn't or might not!