add tests for parallel background compilation

8 files changed, 176 insertions, 0 deletions

diff --git a/ci/compile-tests/004-dependency-cycle/Makefile b/ci/compile-tests/004-dependency-cycle/Makefile
new file mode 100644
index 00000000..4ae0a433
--- /dev/null
+++ b/ci/compile-tests/004-dependency-cycle/Makefile
@@ -0,0 +1,19 @@
+# This file is part of Proof General.
+# 
+# © Copyright 2020  Hendrik Tews
+# 
+# Authors: Hendrik Tews
+# Maintainer: Hendrik Tews <hendrik@askra.de>
+# 
+# License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+
+.PHONY: test
+test:
+	$(MAKE) clean
+	emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \
+		-l test.el -f ert-run-tests-batch-and-exit
+
+.PHONY: clean
+clean:
+	rm -f *.vo *.glob *.vio *.vos *.vok .*.aux
diff --git a/ci/compile-tests/004-dependency-cycle/a.v b/ci/compile-tests/004-dependency-cycle/a.v
new file mode 100644
index 00000000..d84f5d10
--- /dev/null
+++ b/ci/compile-tests/004-dependency-cycle/a.v
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+
+
+(* This is line 21 *)
+Require b.
+Require f.
+(* This is line 24 *)
diff --git a/ci/compile-tests/004-dependency-cycle/b.v b/ci/compile-tests/004-dependency-cycle/b.v
new file mode 100644
index 00000000..c703c3ae
--- /dev/null
+++ b/ci/compile-tests/004-dependency-cycle/b.v
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Require c.
diff --git a/ci/compile-tests/004-dependency-cycle/c.v b/ci/compile-tests/004-dependency-cycle/c.v
new file mode 100644
index 00000000..53bc67d5
--- /dev/null
+++ b/ci/compile-tests/004-dependency-cycle/c.v
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Require d.
diff --git a/ci/compile-tests/004-dependency-cycle/d.v b/ci/compile-tests/004-dependency-cycle/d.v
new file mode 100644
index 00000000..d06e5fec
--- /dev/null
+++ b/ci/compile-tests/004-dependency-cycle/d.v
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Require e.
diff --git a/ci/compile-tests/004-dependency-cycle/e.v b/ci/compile-tests/004-dependency-cycle/e.v
new file mode 100644
index 00000000..604b44e0
--- /dev/null
+++ b/ci/compile-tests/004-dependency-cycle/e.v
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Require b.
diff --git a/ci/compile-tests/004-dependency-cycle/f.v b/ci/compile-tests/004-dependency-cycle/f.v
new file mode 100644
index 00000000..e3f5da5f
--- /dev/null
+++ b/ci/compile-tests/004-dependency-cycle/f.v
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Definition b : nat := 2.
diff --git a/ci/compile-tests/004-dependency-cycle/test.el b/ci/compile-tests/004-dependency-cycle/test.el
new file mode 100644
index 00000000..5f9f63f3
--- /dev/null
+++ b/ci/compile-tests/004-dependency-cycle/test.el
@@ -0,0 +1,58 @@
+;; This file is part of Proof General.
+;;
+;; © Copyright 2020  Hendrik Tews
+;;
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hendrik@askra.de>
+;;
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
+;; Coq Compile Tests (cct) --
+;; ert tests for parallel background compilation for Coq
+;;
+;; Test parallel background compilation for a dependency cycle.
+;;
+;; The following graph shows the file dependencies in this test:
+;;
+;;              a1   a2
+;;             /     |
+;;            b<-e   f
+;;            |  |
+;;            c->d
+;;
+;; where a1 and a2 are the 2 require commands in file a.v.
+
+
+;;; set configuration
+(cct-configure-proof-general)
+
+;;; Define the tests
+
+(ert-deftest cct-require-error ()
+  "Test background compilation on cyclic dependencies."
+  (find-file "a.v")
+  (cct-process-to-line 25)
+  (let ((last-message (cct-last-message-line))
+        message-cycle)
+    (should (equal "Coq compilation error: Circular dependency"
+                   (substring last-message 0 42)))
+
+    (should
+     (string-match
+      (concat
+       "\\./\\([b-e]\\).v -> \\./\\([b-e]\\).v -> "
+       "\\./\\([b-e]\\).v -> \\./\\([b-e]\\).v")
+      last-message))
+    (setq message-cycle
+          (list (match-string 1 last-message) (match-string 2 last-message)
+                (match-string 3 last-message) (match-string 4 last-message)))
+    (should
+     (or (equal message-cycle '("b" "c" "d" "e"))
+         (equal message-cycle '("c" "d" "e" "b"))
+         (equal message-cycle '("d" "e" "b" "c"))
+         (equal message-cycle '("e" "b" "c" "d"))))
+
+    (cct-check-locked 21 'locked)
+    (cct-check-locked 22 'unlocked)))