From e1f5de972cbc0eb8d88675366c34ee66aca1b1b4 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Fri, 14 Jan 2011 21:59:26 +0000
Subject: - more coq test cases (some with surprising and embarrassing bugs)

---
 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 +++++
 7 files changed, 58 insertions(+)
 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

(limited to 'coq/ex/test-cases/multiple-files-single-dir')

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
-- 
cgit v1.2.3