diff options
| -rw-r--r-- | coq/coq.el | 5 | ||||
| -rw-r--r-- | coq/ex/test-cases/README | 4 | ||||
| -rw-r--r-- | coq/ex/test-cases/change-ancestor/README | 23 | ||||
| -rw-r--r-- | coq/ex/test-cases/change-ancestor/a.v | 3 | ||||
| -rw-r--r-- | coq/ex/test-cases/change-ancestor/b.v | 5 |
5 files changed, 40 insertions, 0 deletions
@@ -955,6 +955,9 @@ This is specific to `coq-mode'." ;; ;; TODO list: +;; - Bug: assert newly appended text in locked ancestor apparently +;; sends text before killing coqtop +;; (unreported) ;; - Bug: undo in locked ancestor ;; - Bug: never stopping busy cursor ;; - modify behavior of locked ancestors, see proof-span-read-only @@ -971,6 +974,8 @@ This is specific to `coq-mode'." ;; (http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000138.html) ;; - don't move point in invisible scripting buffer ;; (http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000139.html) + + ;; user options and variables (defgroup coq-auto-compile () diff --git a/coq/ex/test-cases/README b/coq/ex/test-cases/README index 2163c915..d719e333 100644 --- a/coq/ex/test-cases/README +++ b/coq/ex/test-cases/README @@ -10,6 +10,10 @@ Overview of the test cases: add-load-path-unsupported Add LoadPath is not supported +change-ancestor + assert something just added to an completely locked ancestor + (triggers known bugs) + multiple-files-multiple-dir working with multiple files in multiple directories diff --git a/coq/ex/test-cases/change-ancestor/README b/coq/ex/test-cases/change-ancestor/README new file mode 100644 index 00000000..056bd892 --- /dev/null +++ b/coq/ex/test-cases/change-ancestor/README @@ -0,0 +1,23 @@ +One can add text at the end of an completely locked ancestor. +When this text is asserted the following should happen +- retract the current scripting buffer, thereby unlocking all ancestors +- restart Coq +- start asserting at the beginning of the ancestor + +To reproduce the test do the following: +- visit b.v and assert at least the initial Require command in it + (this will lock the ancestor a.v) +- visit the ancestor a.v and add the following text at the end + + Definition b := a. + +- assert that with proof-assert-next-command-interactive or + proof-goto-point + + +This test case triggers a bug in the cvs version from +2011-05-12 12:10:00 UTC. The bug is that after unlocking the +ancestor a.v only the newly added text is sent to Coq. Therefore +Coq responds with an error (reference a was not found in the +current environment). When one asserts a.v from the beginning, +the definition of b is of course accepted. diff --git a/coq/ex/test-cases/change-ancestor/a.v b/coq/ex/test-cases/change-ancestor/a.v new file mode 100644 index 00000000..8981074c --- /dev/null +++ b/coq/ex/test-cases/change-ancestor/a.v @@ -0,0 +1,3 @@ + +Definition a := 0. + diff --git a/coq/ex/test-cases/change-ancestor/b.v b/coq/ex/test-cases/change-ancestor/b.v new file mode 100644 index 00000000..ddc15cb7 --- /dev/null +++ b/coq/ex/test-cases/change-ancestor/b.v @@ -0,0 +1,5 @@ + +Require Import a. + +Definition b := a. + |