add tests for parallel background compilation

5 files changed, 116 insertions, 0 deletions

diff --git a/ci/compile-tests/003-require-error/Makefile b/ci/compile-tests/003-require-error/Makefile
new file mode 100644
index 00000000..4ae0a433
--- /dev/null
+++ b/ci/compile-tests/003-require-error/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/003-require-error/a.v b/ci/compile-tests/003-require-error/a.v
new file mode 100644
index 00000000..d5716ae0
--- /dev/null
+++ b/ci/compile-tests/003-require-error/a.v
@@ -0,0 +1,25 @@
+(* 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 X c.
+Require c.
+(* This is line 25 *)
diff --git a/ci/compile-tests/003-require-error/b.v b/ci/compile-tests/003-require-error/b.v
new file mode 100644
index 00000000..e3f5da5f
--- /dev/null
+++ b/ci/compile-tests/003-require-error/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.
+ *)
+
+Definition b : nat := 2.
diff --git a/ci/compile-tests/003-require-error/c.v b/ci/compile-tests/003-require-error/c.v
new file mode 100644
index 00000000..bd60ca0d
--- /dev/null
+++ b/ci/compile-tests/003-require-error/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.
+ *)
+
+Definition c : nat := 3.
diff --git a/ci/compile-tests/003-require-error/test.el b/ci/compile-tests/003-require-error/test.el
new file mode 100644
index 00000000..0a0dd3d4
--- /dev/null
+++ b/ci/compile-tests/003-require-error/test.el
@@ -0,0 +1,42 @@
+;; 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 when coqdep fails on a require
+;; command.
+;;
+;; The following graph shows the file dependencies in this test, where
+;; X does not exist:
+;;
+;;   a1    a2   a3
+;;   |    /  \ /
+;;   b   X    c
+;;
+;; and where a1, a2 and a3 are the 3 require commands in file a.v
+
+
+;;; set configuration
+(cct-configure-proof-general)
+
+;;; Define the tests
+
+(ert-deftest cct-require-error ()
+  "Test background compilation with an require that yields a coqdep error."
+  (let ((test-start-time (current-time)))
+    (find-file "a.v")
+    (cct-process-to-line 26)
+
+    (cct-check-locked 22 'locked)
+    (cct-check-locked 23 'unlocked)
+    (cct-file-newer "b.vo" test-start-time)
+    (cct-file-newer "c.vo" test-start-time)))