Opened 16 years ago

Closed 16 years ago

#204 closed defect (fixed)

undo stops undoing in large proofs

Reported by: mccreight Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-3.7.1
Component: 2:pg-emacs Keywords: coq undo
Cc:

Description

In large Coq proofs (with more than 100 lines), undo stops working.

For instance:

Lemma Foo : True.

idtac.

[repeat "idtac." around another 112 times]

assert (NI : ~False).

intros IX; auto.

(* Process the script until here, then undo back 3 or 4 lines.

Notice that NI doesn't disappear. *)

Attachments (1)

UndoFail.v​ (1.0 KB) - added by mccreight 16 years ago.
example of undo failure

Download all attachments as: .zip

Change History (4)

Changed 16 years ago by mccreight

Attachment: UndoFail.v​ added

example of undo failure

comment:1 Changed 16 years ago by mccreight

Maybe this is actually just a result of the value of Coq Default Undo Limit being 100 by default? I guess I can just change that.

comment:2 Changed 16 years ago by mccreight

Okay, it looks like things do work when the limit is increased. Maybe this could be added to the FAQ? Or maybe I just missed wherever it is discussed.

comment:3 Changed 16 years ago by David Aspinall

Resolution: → fixed
Status: new → closed

Thanks for raising this.

I've added an item to the FAQ, and also added a setting for Undo Depth to the Coq settings menu, and made this default to 200, which should make it a bit harder to reach with real proofs...

Note: See TracTickets for help on using tickets.