Opened 12 years ago

Last modified 12 years ago

#443 closed defect

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

Reported by: coquser Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.2
Component: 2:pg-emacs Keywords:
Cc: jasongross9+bugzilla@…

Description (last modified by David Aspinall)

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.

Change History (5)

comment:1 Changed 12 years ago by 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.
  1. 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

comment:2 Changed 12 years ago by coquser

OK... tried it myself:

  1. it is a PG problem, *coq* contains the wrong text
  1. 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

comment:3 Changed 12 years ago by 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

comment:4 in reply to:  3 Changed 12 years ago by 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

comment:5 Changed 12 years ago by David Aspinall

Description: modified (diff)
Status: newaccepted

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.

Note: See TracTickets for help on using tickets.