From e1f5de972cbc0eb8d88675366c34ee66aca1b1b4 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Fri, 14 Jan 2011 21:59:26 +0000 Subject: - more coq test cases (some with surprising and embarrassing bugs) --- coq/ex/test-cases/README | 19 +++++++++++++ coq/ex/test-cases/add-load-path-unsupported/README | 12 ++++++++ coq/ex/test-cases/add-load-path-unsupported/a/a.v | 3 ++ coq/ex/test-cases/add-load-path-unsupported/b/b.v | 7 +++++ .../test-cases/multiple-files-multiple-dir/README | 23 ++++++++++++++++ .../test-cases/multiple-files-multiple-dir/a/a.v | 3 ++ .../test-cases/multiple-files-multiple-dir/b/b1.v | 9 ++++++ .../test-cases/multiple-files-multiple-dir/b/b2.v | 9 ++++++ .../test-cases/multiple-files-multiple-dir/c/c.v | 11 ++++++++ coq/ex/test-cases/multiple-files-single-dir/README | 32 ++++++++++++++++++++++ coq/ex/test-cases/multiple-files-single-dir/a.v | 3 ++ coq/ex/test-cases/multiple-files-single-dir/b.v | 3 ++ coq/ex/test-cases/multiple-files-single-dir/c.v | 3 ++ coq/ex/test-cases/multiple-files-single-dir/d.v | 5 ++++ coq/ex/test-cases/multiple-files-single-dir/e.v | 5 ++++ coq/ex/test-cases/multiple-files-single-dir/f.v | 7 +++++ coq/ex/test-cases/require-string/README | 3 ++ coq/ex/test-cases/require-string/a.v | 3 ++ coq/ex/test-cases/require-string/b.v | 8 ++++++ coq/ex/test-cases/stale-load-path/README | 18 ++++++++++++ coq/ex/test-cases/stale-load-path/a/Le.v | 3 ++ coq/ex/test-cases/stale-load-path/b/b.v | 14 ++++++++++ coq/ex/test-cases/stale-load-path/c/c.v | 9 ++++++ 23 files changed, 212 insertions(+) create mode 100644 coq/ex/test-cases/add-load-path-unsupported/README create mode 100644 coq/ex/test-cases/add-load-path-unsupported/a/a.v create mode 100644 coq/ex/test-cases/add-load-path-unsupported/b/b.v create mode 100644 coq/ex/test-cases/multiple-files-multiple-dir/README create mode 100644 coq/ex/test-cases/multiple-files-multiple-dir/a/a.v create mode 100644 coq/ex/test-cases/multiple-files-multiple-dir/b/b1.v create mode 100644 coq/ex/test-cases/multiple-files-multiple-dir/b/b2.v create mode 100644 coq/ex/test-cases/multiple-files-multiple-dir/c/c.v create mode 100644 coq/ex/test-cases/multiple-files-single-dir/README create mode 100644 coq/ex/test-cases/multiple-files-single-dir/a.v create mode 100644 coq/ex/test-cases/multiple-files-single-dir/b.v create mode 100644 coq/ex/test-cases/multiple-files-single-dir/c.v create mode 100644 coq/ex/test-cases/multiple-files-single-dir/d.v create mode 100644 coq/ex/test-cases/multiple-files-single-dir/e.v create mode 100644 coq/ex/test-cases/multiple-files-single-dir/f.v create mode 100644 coq/ex/test-cases/require-string/README create mode 100644 coq/ex/test-cases/require-string/a.v create mode 100644 coq/ex/test-cases/require-string/b.v create mode 100644 coq/ex/test-cases/stale-load-path/README create mode 100644 coq/ex/test-cases/stale-load-path/a/Le.v create mode 100644 coq/ex/test-cases/stale-load-path/b/b.v create mode 100644 coq/ex/test-cases/stale-load-path/c/c.v (limited to 'coq/ex') diff --git a/coq/ex/test-cases/README b/coq/ex/test-cases/README index 62081521..3943793a 100644 --- a/coq/ex/test-cases/README +++ b/coq/ex/test-cases/README @@ -7,6 +7,25 @@ a README file, describing the test case. Overview of the test cases: +add-load-path-unsupported + Add LoadPath is not supported + +multiple-files-multiple-dir + working with multiple files in a multiple directories + (triggers known bugs) + +multiple-files-single-dir + working with multiple files in a single directory + (triggers known bugs) + +require-string + test Require "x.vo" + (triggers known bugs) + retract-completely-asserted test how proof-no-fully-processed-buffer retracts fully asserted buffers + +stale-load-path + test switching between files with different load path. + (triggers known bugs) diff --git a/coq/ex/test-cases/add-load-path-unsupported/README b/coq/ex/test-cases/add-load-path-unsupported/README new file mode 100644 index 00000000..d6e56c25 --- /dev/null +++ b/coq/ex/test-cases/add-load-path-unsupported/README @@ -0,0 +1,12 @@ +b/b.v depends on a/a.v and the code is correct because of Add +LoadPath in b. + +Scripting b/b.v works if coq-recompile-before-require is set to +nil and if a/a.v is compiled manually. + +This problem is not considered a bug, but a feature that does not +make much sense to implement, because apparently nobody is using +Add LoadPath. + +Note that not even coqdep is able to handle b/b.v correctly! + diff --git a/coq/ex/test-cases/add-load-path-unsupported/a/a.v b/coq/ex/test-cases/add-load-path-unsupported/a/a.v new file mode 100644 index 00000000..984ad082 --- /dev/null +++ b/coq/ex/test-cases/add-load-path-unsupported/a/a.v @@ -0,0 +1,3 @@ +(* This file depends on nothing. *) + +Definition a := 0. diff --git a/coq/ex/test-cases/add-load-path-unsupported/b/b.v b/coq/ex/test-cases/add-load-path-unsupported/b/b.v new file mode 100644 index 00000000..226b71ee --- /dev/null +++ b/coq/ex/test-cases/add-load-path-unsupported/b/b.v @@ -0,0 +1,7 @@ +(* This file depends on ../a/a.v *) + +Add LoadPath "../a". + +Require a. + +Print a.a. \ No newline at end of file diff --git a/coq/ex/test-cases/multiple-files-multiple-dir/README b/coq/ex/test-cases/multiple-files-multiple-dir/README new file mode 100644 index 00000000..82c7fc2a --- /dev/null +++ b/coq/ex/test-cases/multiple-files-multiple-dir/README @@ -0,0 +1,23 @@ +Test multiple file support when files are distributed over +different directories. + +Dependency graph + + a/a.v + \ + \ + b/b1.v --- b/b2.v + \ + \ + c/c.v + +That is, c depends on b2, which depends on b1, which depends on +a. + +Script c.v and watch the compilation messages in *Messages*. +Touch any file and retract and assert the Require in c. + +The bugs described in ../multiple-files-single-dir/README can +also be reproduced here. + + diff --git a/coq/ex/test-cases/multiple-files-multiple-dir/a/a.v b/coq/ex/test-cases/multiple-files-multiple-dir/a/a.v new file mode 100644 index 00000000..e4dadf39 --- /dev/null +++ b/coq/ex/test-cases/multiple-files-multiple-dir/a/a.v @@ -0,0 +1,3 @@ +(* this file depends on nothing *) + +Definition a := 0. \ No newline at end of file diff --git a/coq/ex/test-cases/multiple-files-multiple-dir/b/b1.v b/coq/ex/test-cases/multiple-files-multiple-dir/b/b1.v new file mode 100644 index 00000000..afcd3941 --- /dev/null +++ b/coq/ex/test-cases/multiple-files-multiple-dir/b/b1.v @@ -0,0 +1,9 @@ +(* this file depends on ../a/a.v *) + +Definition a := 1. + +Require a. + +(*** Local Variables: ***) +(*** coq-load-path: ("../a") ***) +(*** End: ***) diff --git a/coq/ex/test-cases/multiple-files-multiple-dir/b/b2.v b/coq/ex/test-cases/multiple-files-multiple-dir/b/b2.v new file mode 100644 index 00000000..6d79572a --- /dev/null +++ b/coq/ex/test-cases/multiple-files-multiple-dir/b/b2.v @@ -0,0 +1,9 @@ +(* this file depends on b1 and therefore indirectly on ../a/a.v *) + +Definition a := 2. + +Require b1. + +(*** Local Variables: ***) +(*** coq-load-path: ("../a") ***) +(*** End: ***) diff --git a/coq/ex/test-cases/multiple-files-multiple-dir/c/c.v b/coq/ex/test-cases/multiple-files-multiple-dir/c/c.v new file mode 100644 index 00000000..5171340c --- /dev/null +++ b/coq/ex/test-cases/multiple-files-multiple-dir/c/c.v @@ -0,0 +1,11 @@ +(* this file depends on ../b/b2 and therefore indirectly + * on ../b/b1 and ../a/a.v + *) + +Definition a := 2. + +Require b2. + +(*** Local Variables: ***) +(*** coq-load-path: ("../a" "../b") ***) +(*** End: ***) diff --git a/coq/ex/test-cases/multiple-files-single-dir/README b/coq/ex/test-cases/multiple-files-single-dir/README new file mode 100644 index 00000000..db1a6a9b --- /dev/null +++ b/coq/ex/test-cases/multiple-files-single-dir/README @@ -0,0 +1,32 @@ +Test multiple file support for the simple case in which all files +are in one directory. + +Dependency graph: + + a.v b.v c.v + \ / \ / + \ / \ / + d.v e.v + \ / + \ / + f.v + +That is, d.v depends on a.v and b.v, and so on. + +Some tests: + +- first visit f.v and display the *Message* buffer in some other + frame +- script f.v and watch the recompilation messages in the + *Message* buffer +- Change now an arbitrary file (either from within emacs or + simply do touch), retract the Require in f.v, and watch the + compilation messages when you assert it again. + +The implementation in Proof General cvs at 2011-01-14 20:03:51 UTC +has an embarrassing bug: Touching b.v causes recompilation of b.v +and d.v but not of e.v! + +Another problem is the following: After a consistent compilation, +change b.v and recompile it outside of Proof General. Then script +f.v -- Proof General will not recompile d and e! diff --git a/coq/ex/test-cases/multiple-files-single-dir/a.v b/coq/ex/test-cases/multiple-files-single-dir/a.v new file mode 100644 index 00000000..e4dadf39 --- /dev/null +++ b/coq/ex/test-cases/multiple-files-single-dir/a.v @@ -0,0 +1,3 @@ +(* this file depends on nothing *) + +Definition a := 0. \ No newline at end of file diff --git a/coq/ex/test-cases/multiple-files-single-dir/b.v b/coq/ex/test-cases/multiple-files-single-dir/b.v new file mode 100644 index 00000000..a2f896a9 --- /dev/null +++ b/coq/ex/test-cases/multiple-files-single-dir/b.v @@ -0,0 +1,3 @@ +(* this file depends on nothing *) + +Definition a := 1. \ No newline at end of file diff --git a/coq/ex/test-cases/multiple-files-single-dir/c.v b/coq/ex/test-cases/multiple-files-single-dir/c.v new file mode 100644 index 00000000..b90ef9a0 --- /dev/null +++ b/coq/ex/test-cases/multiple-files-single-dir/c.v @@ -0,0 +1,3 @@ +(* this file depends on nothing *) + +Definition a := 2. \ No newline at end of file diff --git a/coq/ex/test-cases/multiple-files-single-dir/d.v b/coq/ex/test-cases/multiple-files-single-dir/d.v new file mode 100644 index 00000000..b0c47e8b --- /dev/null +++ b/coq/ex/test-cases/multiple-files-single-dir/d.v @@ -0,0 +1,5 @@ +(* this file depends on a.v and b.v *) + +Require Import a b. + +Definition a := 3. \ No newline at end of file diff --git a/coq/ex/test-cases/multiple-files-single-dir/e.v b/coq/ex/test-cases/multiple-files-single-dir/e.v new file mode 100644 index 00000000..9dc2be32 --- /dev/null +++ b/coq/ex/test-cases/multiple-files-single-dir/e.v @@ -0,0 +1,5 @@ +(* this file depends on b.v and c.v *) + +Require Import b c. + +Definition a := 4. \ No newline at end of file diff --git a/coq/ex/test-cases/multiple-files-single-dir/f.v b/coq/ex/test-cases/multiple-files-single-dir/f.v new file mode 100644 index 00000000..d36ccef6 --- /dev/null +++ b/coq/ex/test-cases/multiple-files-single-dir/f.v @@ -0,0 +1,7 @@ +(* this file depends on d.v and e.v and therefore + * indirectly also on a.v, b.v and c.v + *) + +Require Import d e. + +Definition a := 5. \ No newline at end of file diff --git a/coq/ex/test-cases/require-string/README b/coq/ex/test-cases/require-string/README new file mode 100644 index 00000000..7b3c5cbe --- /dev/null +++ b/coq/ex/test-cases/require-string/README @@ -0,0 +1,3 @@ +The "Require string" variant is currently not supported. + +Here b.v contains Require "a.vo". diff --git a/coq/ex/test-cases/require-string/a.v b/coq/ex/test-cases/require-string/a.v new file mode 100644 index 00000000..fc20deef --- /dev/null +++ b/coq/ex/test-cases/require-string/a.v @@ -0,0 +1,3 @@ +(* This file has no dependencies. *) + +Definition a := 0. \ No newline at end of file diff --git a/coq/ex/test-cases/require-string/b.v b/coq/ex/test-cases/require-string/b.v new file mode 100644 index 00000000..219c29e2 --- /dev/null +++ b/coq/ex/test-cases/require-string/b.v @@ -0,0 +1,8 @@ +(* This file depends on a.v. *) + +(* The following works in Proof General 4.0, if a.v has been compiled and + * if the path is the correct absolute path. + *) +Require "/home/tews/src/pg/coq/ex/test-cases/require-string/a". + +Print a.a. \ No newline at end of file diff --git a/coq/ex/test-cases/stale-load-path/README b/coq/ex/test-cases/stale-load-path/README new file mode 100644 index 00000000..343fe85a --- /dev/null +++ b/coq/ex/test-cases/stale-load-path/README @@ -0,0 +1,18 @@ +Here we have three projects a, b and c. The projects b and c are +totally independent from each other. + +Strangely, project a contains a module Le, which clashes with +Coq.Arith.Le from the standard library. + +Project b depends on a, more precisely, b/b.v requires a/Le.v. + +File c/c.v require Le, but this refers to Coq.Arith.Le!! + +Currently coqtop is not able to reset the LoadPath, therefore, +when first scripting b/b.v and then switching to c/c.v, coq +wrongly loads a/Le.vo! Vice versa, when first scripting c/c.v and +then switching to b/b.v, coq loads Coq.Arith.Le instead of +a/Le.vo! + +Because coq-load-path is file-local, the dependency analysis +works correctly. diff --git a/coq/ex/test-cases/stale-load-path/a/Le.v b/coq/ex/test-cases/stale-load-path/a/Le.v new file mode 100644 index 00000000..d739fbc5 --- /dev/null +++ b/coq/ex/test-cases/stale-load-path/a/Le.v @@ -0,0 +1,3 @@ +(* This file intentionally hides Coq.Arith.Le *) + +Definition a := 0. diff --git a/coq/ex/test-cases/stale-load-path/b/b.v b/coq/ex/test-cases/stale-load-path/b/b.v new file mode 100644 index 00000000..e021cf7a --- /dev/null +++ b/coq/ex/test-cases/stale-load-path/b/b.v @@ -0,0 +1,14 @@ +(* This file depends on ../a/Le.v *) + +Require Le. + +(* The next print should work. *) +Print Le.a. + +(* The next print should not work. *) +Print Le.le_refl. + + +(*** Local Variables: ***) +(*** coq-load-path: ("../a") ***) +(*** End: ***) diff --git a/coq/ex/test-cases/stale-load-path/c/c.v b/coq/ex/test-cases/stale-load-path/c/c.v new file mode 100644 index 00000000..f05f65a1 --- /dev/null +++ b/coq/ex/test-cases/stale-load-path/c/c.v @@ -0,0 +1,9 @@ +(* This file depends on Coq.Arith.Le from the standard library. *) + +Require Le. + +(* The next print should work. *) +Print Le.le_refl. + +(* The next print should not work. *) +Print Le.a. -- cgit v1.2.3