CI: add tests for partially failing background compilation

ci/compile-tests/009-failure-processing/Makefile

@@ -0,0 +1,44 @@
+# This file is part of Proof General.
+# 
+# © Copyright 2021  Hendrik Tews
+# 
+# Authors: Hendrik Tews
+# Maintainer: Hendrik Tews <[email protected]>
+# 
+# License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+
+# This test modifies some .v files during the test. The original
+# versions are in .v.orig files. They are moved to the corresponding
+# .v files before the test starts.
+TEST_SOURCES:=\
+	a1.v b1.v c1.v d1.v e1.v f1.v g1.v h1.v \
+	a2.v b2.v c2.v d2.v e2.v f2.v g2.v h2.v \
+	a3.v b3.v c3.v d3.v e3.v f3.v g3.v h3.v \
+	a4.v b4.v c4.v d4.v e4.v f4.v g4.v h4.v \
+	a5.v b5.v c5.v d5.v e5.v f5.v g5.v h5.v \
+	a6.v b6.v c6.v d6.v e6.v f6.v g6.v h6.v \
+	a7.v b7.v c7.v d7.v e7.v f7.v g7.v h7.v \
+	a8.v b8.v c8.v d8.v e8.v f8.v g8.v h8.v \
+	a9.v b9.v c9.v d9.v e9.v f9.v g9.v h9.v \
+	a10.v b10.v c10.v d10.v e10.v f10.v g10.v h10.v
+
+# This test uses ../bin/compile-test-start-delayed to start certain
+# commands with specified delays to check carfully constructed
+# internal states. compile-test-start-delayed outputs diagnostics on
+# file descriptor 9, which bypasses emacs and is joined with stderr of
+# the current make. Open file descriptor 9 here.
+.PHONY: test
+test:
+	$(MAKE) clean
+	$(MAKE) $(TEST_SOURCES)
+	emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \
+		-l runtest.el -f ert-run-tests-batch-and-exit \
+		9>&1
+
+%.v: %.v.orig
+	cp $< $@
+
+.PHONY: clean
+clean:
+	rm -f *.vo *.glob *.vio *.vos *.vok .*.aux *.X $(TEST_SOURCES)

ci/compile-tests/009-failure-processing/a1.v.orig

@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * 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 runtest.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT/DELETE ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export b1.
+Require Export c1.
+Require Export d1.
+(* This is line 28 *)

ci/compile-tests/009-failure-processing/a10.v.orig

@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * 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 runtest.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT/DELETE ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export b10.
+Require Export c10.
+Require Export d10.
+(* This is line 28 *)

ci/compile-tests/009-failure-processing/a2.v.orig

@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * 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 runtest.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT/DELETE ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export b2.
+Require Export c2.
+Require Export d2.
+(* This is line 28 *)

ci/compile-tests/009-failure-processing/a3.v.orig

@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * 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 runtest.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT/DELETE ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export b3.
+Require Export c3.
+Require Export d3.
+(* This is line 28 *)

ci/compile-tests/009-failure-processing/a4.v.orig

@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * 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 runtest.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT/DELETE ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export b4.
+Require Export c4.
+Require Export d4.
+(* This is line 28 *)

ci/compile-tests/009-failure-processing/a5.v.orig

@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * 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 runtest.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT/DELETE ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export b5.
+Require Export c5.
+Require Export d5.
+(* This is line 28 *)

ci/compile-tests/009-failure-processing/a6.v.orig

@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * 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 runtest.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT/DELETE ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export b6.
+Require Export c6.
+Require Export d6.
+(* This is line 28 *)

ci/compile-tests/009-failure-processing/a7.v.orig

@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * 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 runtest.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT/DELETE ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export b7.
+Require Export c7.
+Require Export d7.
+(* This is line 28 *)

ci/compile-tests/009-failure-processing/a8.v.orig

@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * 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 runtest.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT/DELETE ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export b8.
+Require Export c8.
+Require Export d8.
+(* This is line 28 *)

ci/compile-tests/009-failure-processing/a9.v.orig

@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * 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 runtest.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT/DELETE ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export b9.
+Require Export c9.
+Require Export d9.
+(* This is line 28 *)

ci/compile-tests/009-failure-processing/b1.v.orig

@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * 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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export f1.

ci/compile-tests/009-failure-processing/b10.v.orig

@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * 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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 1.5
+ *)
+
+Require Export f10.