- more coq test cases (some with surprising and embarrassing bugs)

23 files changed, 212 insertions, 0 deletions

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.