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

5 files changed, 55 insertions, 0 deletions

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: ***)