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)
Change History (4)
Changed 16 years ago by
Attachment: | UndoFail.v added |
---|
comment:1 Changed 16 years ago by
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
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
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...
example of undo failure