diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2011-05-12 11:59:15 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2011-05-12 11:59:15 +0000 |
| commit | df9f007644f89c6acd7104ea641876a868e10e89 (patch) | |
| tree | f0aba499bc141ef873d05908453b6b14a8b260dc /coq/ex/test-cases | |
| parent | 3b1a0c3079bf120cda4afbf2d191b98018555659 (diff) | |
- add test coq/ex/test-cases/change-ancestor for the
change-ancestor bug
Diffstat (limited to 'coq/ex/test-cases')
| -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 |
4 files changed, 35 insertions, 0 deletions
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. + |