Changes between Initial Version and Version 5 of Ticket #443


Ignore:
Timestamp:
Aug 9, 2012, 1:21:25 PM (12 years ago)
Author:
David Aspinall
Comment:

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.

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #443

    • Property Status changed from new to accepted
  • Ticket #443 – Description

    initial v5  
    22
    33Given the following file*:
    4 
     4{{{
    55Require Import Program Omega Bool.
    66
     
    2222Print foo.
    2323Print foo.
    24 
     24}}}
    2525Tell 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]).
    2626