From 6a115fa3a08e29040c29ec98f46687debe8b2b82 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Sun, 23 May 2021 23:00:05 +0200
Subject: [PATCH] CI: add tests for partially failing background compilation

---
 .../009-failure-processing/Makefile           |  44 ++++++
 .../009-failure-processing/a1.v.orig          |  28 ++++
 .../009-failure-processing/a10.v.orig         |  28 ++++
 .../009-failure-processing/a2.v.orig          |  28 ++++
 .../009-failure-processing/a3.v.orig          |  28 ++++
 .../009-failure-processing/a4.v.orig          |  28 ++++
 .../009-failure-processing/a5.v.orig          |  28 ++++
 .../009-failure-processing/a6.v.orig          |  28 ++++
 .../009-failure-processing/a7.v.orig          |  28 ++++
 .../009-failure-processing/a8.v.orig          |  28 ++++
 .../009-failure-processing/a9.v.orig          |  28 ++++
 .../009-failure-processing/b1.v.orig          |  24 +++
 .../009-failure-processing/b10.v.orig         |  24 +++
 .../009-failure-processing/b2.v.orig          |  24 +++
 .../009-failure-processing/b3.v.orig          |  24 +++
 .../009-failure-processing/b4.v.orig          |  24 +++
 .../009-failure-processing/b5.v.orig          |  24 +++
 .../009-failure-processing/b6.v.orig          |  24 +++
 .../009-failure-processing/b7.v.orig          |  24 +++
 .../009-failure-processing/b8.v.orig          |  24 +++
 .../009-failure-processing/b9.v.orig          |  24 +++
 .../009-failure-processing/c1.v.orig          |  24 +++
 .../009-failure-processing/c10.v.orig         |  24 +++
 .../009-failure-processing/c2.v.orig          |  24 +++
 .../009-failure-processing/c3.v.orig          |  24 +++
 .../009-failure-processing/c4.v.orig          |  24 +++
 .../009-failure-processing/c5.v.orig          |  24 +++
 .../009-failure-processing/c6.v.orig          |  24 +++
 .../009-failure-processing/c7.v.orig          |  24 +++
 .../009-failure-processing/c8.v.orig          |  24 +++
 .../009-failure-processing/c9.v.orig          |  24 +++
 .../009-failure-processing/d1.v.orig          |  24 +++
 .../009-failure-processing/d10.v.orig         |  24 +++
 .../009-failure-processing/d2.v.orig          |  24 +++
 .../009-failure-processing/d3.v.orig          |  24 +++
 .../009-failure-processing/d4.v.orig          |  24 +++
 .../009-failure-processing/d5.v.orig          |  24 +++
 .../009-failure-processing/d6.v.orig          |  24 +++
 .../009-failure-processing/d7.v.orig          |  24 +++
 .../009-failure-processing/d8.v.orig          |  24 +++
 .../009-failure-processing/d9.v.orig          |  24 +++
 .../009-failure-processing/e1.v.orig          |  24 +++
 .../009-failure-processing/e10.v.orig         |  25 +++
 .../009-failure-processing/e2.v.orig          |  24 +++
 .../009-failure-processing/e3.v.orig          |  24 +++
 .../009-failure-processing/e4.v.orig          |  24 +++
 .../009-failure-processing/e5.v.orig          |  25 +++
 .../009-failure-processing/e6.v.orig          |  24 +++
 .../009-failure-processing/e7.v.orig          |  24 +++
 .../009-failure-processing/e8.v.orig          |  24 +++
 .../009-failure-processing/e9.v.orig          |  24 +++
 .../009-failure-processing/f1.v.orig          |  24 +++
 .../009-failure-processing/f10.v.orig         |  24 +++
 .../009-failure-processing/f2.v.orig          |  24 +++
 .../009-failure-processing/f3.v.orig          |  24 +++
 .../009-failure-processing/f4.v.orig          |  24 +++
 .../009-failure-processing/f5.v.orig          |  24 +++
 .../009-failure-processing/f6.v.orig          |  24 +++
 .../009-failure-processing/f7.v.orig          |  24 +++
 .../009-failure-processing/f8.v.orig          |  24 +++
 .../009-failure-processing/f9.v.orig          |  24 +++
 .../009-failure-processing/g1.v.orig          |  25 +++
 .../009-failure-processing/g10.v.orig         |  28 ++++
 .../009-failure-processing/g2.v.orig          |  25 +++
 .../009-failure-processing/g3.v.orig          |  25 +++
 .../009-failure-processing/g4.v.orig          |  25 +++
 .../009-failure-processing/g5.v.orig          |  25 +++
 .../009-failure-processing/g6.v.orig          |  28 ++++
 .../009-failure-processing/g7.v.orig          |  28 ++++
 .../009-failure-processing/g8.v.orig          |  28 ++++
 .../009-failure-processing/g9.v.orig          |  28 ++++
 .../009-failure-processing/h1.v.orig          |  24 +++
 .../009-failure-processing/h10.v.orig         |  24 +++
 .../009-failure-processing/h2.v.orig          |  24 +++
 .../009-failure-processing/h3.v.orig          |  24 +++
 .../009-failure-processing/h4.v.orig          |  24 +++
 .../009-failure-processing/h5.v.orig          |  24 +++
 .../009-failure-processing/h6.v.orig          |  24 +++
 .../009-failure-processing/h7.v.orig          |  24 +++
 .../009-failure-processing/h8.v.orig          |  24 +++
 .../009-failure-processing/h9.v.orig          |  24 +++
 .../009-failure-processing/runtest.el         | 142 ++++++++++++++++++
 ci/compile-tests/README.md                    |   6 +-
 .../bin/compile-test-start-delayed            |  30 ++--
 ci/compile-tests/cct-lib.el                   |  20 +++
 coq/coq-par-compile.el                        |  31 +++-
 86 files changed, 2242 insertions(+), 18 deletions(-)
 create mode 100644 ci/compile-tests/009-failure-processing/Makefile
 create mode 100644 ci/compile-tests/009-failure-processing/a1.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/a10.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/a2.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/a3.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/a4.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/a5.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/a6.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/a7.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/a8.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/a9.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/b1.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/b10.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/b2.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/b3.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/b4.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/b5.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/b6.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/b7.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/b8.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/b9.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/c1.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/c10.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/c2.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/c3.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/c4.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/c5.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/c6.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/c7.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/c8.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/c9.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/d1.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/d10.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/d2.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/d3.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/d4.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/d5.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/d6.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/d7.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/d8.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/d9.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/e1.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/e10.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/e2.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/e3.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/e4.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/e5.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/e6.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/e7.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/e8.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/e9.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/f1.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/f10.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/f2.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/f3.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/f4.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/f5.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/f6.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/f7.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/f8.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/f9.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/g1.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/g10.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/g2.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/g3.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/g4.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/g5.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/g6.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/g7.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/g8.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/g9.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/h1.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/h10.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/h2.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/h3.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/h4.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/h5.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/h6.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/h7.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/h8.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/h9.v.orig
 create mode 100644 ci/compile-tests/009-failure-processing/runtest.el

diff --git a/ci/compile-tests/009-failure-processing/Makefile b/ci/compile-tests/009-failure-processing/Makefile
new file mode 100644
index 000000000..8632198fc
--- /dev/null
+++ b/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 <hendrik@askra.de>
+# 
+# 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)
diff --git a/ci/compile-tests/009-failure-processing/a1.v.orig b/ci/compile-tests/009-failure-processing/a1.v.orig
new file mode 100644
index 000000000..44324ec06
--- /dev/null
+++ b/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 <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 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 *)
diff --git a/ci/compile-tests/009-failure-processing/a10.v.orig b/ci/compile-tests/009-failure-processing/a10.v.orig
new file mode 100644
index 000000000..24800dac3
--- /dev/null
+++ b/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 <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 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 *)
diff --git a/ci/compile-tests/009-failure-processing/a2.v.orig b/ci/compile-tests/009-failure-processing/a2.v.orig
new file mode 100644
index 000000000..99d1ed6b7
--- /dev/null
+++ b/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 <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 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 *)
diff --git a/ci/compile-tests/009-failure-processing/a3.v.orig b/ci/compile-tests/009-failure-processing/a3.v.orig
new file mode 100644
index 000000000..9e332554f
--- /dev/null
+++ b/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 <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 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 *)
diff --git a/ci/compile-tests/009-failure-processing/a4.v.orig b/ci/compile-tests/009-failure-processing/a4.v.orig
new file mode 100644
index 000000000..379134af0
--- /dev/null
+++ b/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 <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 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 *)
diff --git a/ci/compile-tests/009-failure-processing/a5.v.orig b/ci/compile-tests/009-failure-processing/a5.v.orig
new file mode 100644
index 000000000..8dedb2f87
--- /dev/null
+++ b/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 <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 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 *)
diff --git a/ci/compile-tests/009-failure-processing/a6.v.orig b/ci/compile-tests/009-failure-processing/a6.v.orig
new file mode 100644
index 000000000..444004589
--- /dev/null
+++ b/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 <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 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 *)
diff --git a/ci/compile-tests/009-failure-processing/a7.v.orig b/ci/compile-tests/009-failure-processing/a7.v.orig
new file mode 100644
index 000000000..b9db034e9
--- /dev/null
+++ b/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 <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 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 *)
diff --git a/ci/compile-tests/009-failure-processing/a8.v.orig b/ci/compile-tests/009-failure-processing/a8.v.orig
new file mode 100644
index 000000000..2aea7b0e5
--- /dev/null
+++ b/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 <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 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 *)
diff --git a/ci/compile-tests/009-failure-processing/a9.v.orig b/ci/compile-tests/009-failure-processing/a9.v.orig
new file mode 100644
index 000000000..67856647d
--- /dev/null
+++ b/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 <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 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 *)
diff --git a/ci/compile-tests/009-failure-processing/b1.v.orig b/ci/compile-tests/009-failure-processing/b1.v.orig
new file mode 100644
index 000000000..9cb45bf91
--- /dev/null
+++ b/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 <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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export f1.
diff --git a/ci/compile-tests/009-failure-processing/b10.v.orig b/ci/compile-tests/009-failure-processing/b10.v.orig
new file mode 100644
index 000000000..61f71d04f
--- /dev/null
+++ b/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 <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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 1.5
+ *)
+
+Require Export f10.
diff --git a/ci/compile-tests/009-failure-processing/b2.v.orig b/ci/compile-tests/009-failure-processing/b2.v.orig
new file mode 100644
index 000000000..79fc08bbf
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/b2.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 2
+ *)
+
+Require Export f2.
diff --git a/ci/compile-tests/009-failure-processing/b3.v.orig b/ci/compile-tests/009-failure-processing/b3.v.orig
new file mode 100644
index 000000000..12c118f01
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/b3.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 3
+ *)
+
+Require Export f3.
diff --git a/ci/compile-tests/009-failure-processing/b4.v.orig b/ci/compile-tests/009-failure-processing/b4.v.orig
new file mode 100644
index 000000000..0963e1ce3
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/b4.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export f4.
diff --git a/ci/compile-tests/009-failure-processing/b5.v.orig b/ci/compile-tests/009-failure-processing/b5.v.orig
new file mode 100644
index 000000000..54136bb28
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/b5.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 1.5
+ *)
+
+Require Export f5.
diff --git a/ci/compile-tests/009-failure-processing/b6.v.orig b/ci/compile-tests/009-failure-processing/b6.v.orig
new file mode 100644
index 000000000..2a3d88c38
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/b6.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export f6.
diff --git a/ci/compile-tests/009-failure-processing/b7.v.orig b/ci/compile-tests/009-failure-processing/b7.v.orig
new file mode 100644
index 000000000..2e756cc16
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/b7.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 1
+ *)
+
+Require Export f7.
diff --git a/ci/compile-tests/009-failure-processing/b8.v.orig b/ci/compile-tests/009-failure-processing/b8.v.orig
new file mode 100644
index 000000000..7b74bd944
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/b8.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 1.5
+ *)
+
+Require Export f8.
diff --git a/ci/compile-tests/009-failure-processing/b9.v.orig b/ci/compile-tests/009-failure-processing/b9.v.orig
new file mode 100644
index 000000000..b3fcc9a33
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/b9.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export f9.
diff --git a/ci/compile-tests/009-failure-processing/c1.v.orig b/ci/compile-tests/009-failure-processing/c1.v.orig
new file mode 100644
index 000000000..e7f5e30ce
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/c1.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay X
+ *)
+
+Require Export e1 g1.
diff --git a/ci/compile-tests/009-failure-processing/c10.v.orig b/ci/compile-tests/009-failure-processing/c10.v.orig
new file mode 100644
index 000000000..285620ba9
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/c10.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay X
+ *)
+
+Require Export e10 g10.
diff --git a/ci/compile-tests/009-failure-processing/c2.v.orig b/ci/compile-tests/009-failure-processing/c2.v.orig
new file mode 100644
index 000000000..d71147c87
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/c2.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay X
+ *)
+
+Require Export e2 g2.
diff --git a/ci/compile-tests/009-failure-processing/c3.v.orig b/ci/compile-tests/009-failure-processing/c3.v.orig
new file mode 100644
index 000000000..6b4611684
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/c3.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay X
+ *)
+
+Require Export e3 g3.
diff --git a/ci/compile-tests/009-failure-processing/c4.v.orig b/ci/compile-tests/009-failure-processing/c4.v.orig
new file mode 100644
index 000000000..9c323c3f6
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/c4.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay X
+ *)
+
+Require Export e4 g4.
diff --git a/ci/compile-tests/009-failure-processing/c5.v.orig b/ci/compile-tests/009-failure-processing/c5.v.orig
new file mode 100644
index 000000000..8b9589a75
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/c5.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay X
+ *)
+
+Require Export e5 g5.
diff --git a/ci/compile-tests/009-failure-processing/c6.v.orig b/ci/compile-tests/009-failure-processing/c6.v.orig
new file mode 100644
index 000000000..6a4322c73
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/c6.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay X
+ *)
+
+Require Export e6 g6.
diff --git a/ci/compile-tests/009-failure-processing/c7.v.orig b/ci/compile-tests/009-failure-processing/c7.v.orig
new file mode 100644
index 000000000..d67bc5044
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/c7.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay X
+ *)
+
+Require Export e7 g7.
diff --git a/ci/compile-tests/009-failure-processing/c8.v.orig b/ci/compile-tests/009-failure-processing/c8.v.orig
new file mode 100644
index 000000000..9fb660d16
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/c8.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay X
+ *)
+
+Require Export e8 g8.
diff --git a/ci/compile-tests/009-failure-processing/c9.v.orig b/ci/compile-tests/009-failure-processing/c9.v.orig
new file mode 100644
index 000000000..b6da31a7f
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/c9.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay X
+ *)
+
+Require Export e9 g9.
diff --git a/ci/compile-tests/009-failure-processing/d1.v.orig b/ci/compile-tests/009-failure-processing/d1.v.orig
new file mode 100644
index 000000000..ce3370984
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/d1.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 1.5
+ *)
+
+Require Export h1.
diff --git a/ci/compile-tests/009-failure-processing/d10.v.orig b/ci/compile-tests/009-failure-processing/d10.v.orig
new file mode 100644
index 000000000..935dab505
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/d10.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export h10.
diff --git a/ci/compile-tests/009-failure-processing/d2.v.orig b/ci/compile-tests/009-failure-processing/d2.v.orig
new file mode 100644
index 000000000..23d119f3d
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/d2.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 3
+ *)
+
+Require Export h2.
diff --git a/ci/compile-tests/009-failure-processing/d3.v.orig b/ci/compile-tests/009-failure-processing/d3.v.orig
new file mode 100644
index 000000000..decce21ff
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/d3.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 2
+ *)
+
+Require Export h3.
diff --git a/ci/compile-tests/009-failure-processing/d4.v.orig b/ci/compile-tests/009-failure-processing/d4.v.orig
new file mode 100644
index 000000000..997ee0724
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/d4.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export h4.
diff --git a/ci/compile-tests/009-failure-processing/d5.v.orig b/ci/compile-tests/009-failure-processing/d5.v.orig
new file mode 100644
index 000000000..bbdfbc661
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/d5.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export h5.
diff --git a/ci/compile-tests/009-failure-processing/d6.v.orig b/ci/compile-tests/009-failure-processing/d6.v.orig
new file mode 100644
index 000000000..44e051481
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/d6.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 1.5
+ *)
+
+Require Export h6.
diff --git a/ci/compile-tests/009-failure-processing/d7.v.orig b/ci/compile-tests/009-failure-processing/d7.v.orig
new file mode 100644
index 000000000..aafbd4800
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/d7.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 1.5
+ *)
+
+Require Export h7.
diff --git a/ci/compile-tests/009-failure-processing/d8.v.orig b/ci/compile-tests/009-failure-processing/d8.v.orig
new file mode 100644
index 000000000..3c333e978
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/d8.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 1
+ *)
+
+Require Export h8.
diff --git a/ci/compile-tests/009-failure-processing/d9.v.orig b/ci/compile-tests/009-failure-processing/d9.v.orig
new file mode 100644
index 000000000..69260cf5a
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/d9.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export h9.
diff --git a/ci/compile-tests/009-failure-processing/e1.v.orig b/ci/compile-tests/009-failure-processing/e1.v.orig
new file mode 100644
index 000000000..05a88dada
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/e1.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export b1.
diff --git a/ci/compile-tests/009-failure-processing/e10.v.orig b/ci/compile-tests/009-failure-processing/e10.v.orig
new file mode 100644
index 000000000..5d41b5490
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/e10.v.orig
@@ -0,0 +1,25 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+(* Require Export b10. *)
+Definition e : nat := 3.
diff --git a/ci/compile-tests/009-failure-processing/e2.v.orig b/ci/compile-tests/009-failure-processing/e2.v.orig
new file mode 100644
index 000000000..85d9564e3
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/e2.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export b2.
diff --git a/ci/compile-tests/009-failure-processing/e3.v.orig b/ci/compile-tests/009-failure-processing/e3.v.orig
new file mode 100644
index 000000000..5bd8653c4
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/e3.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export b3.
diff --git a/ci/compile-tests/009-failure-processing/e4.v.orig b/ci/compile-tests/009-failure-processing/e4.v.orig
new file mode 100644
index 000000000..02be93fda
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/e4.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export b4.
diff --git a/ci/compile-tests/009-failure-processing/e5.v.orig b/ci/compile-tests/009-failure-processing/e5.v.orig
new file mode 100644
index 000000000..f13dda3da
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/e5.v.orig
@@ -0,0 +1,25 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+(* Require Export b5. *)
+Definition e : nat := 3.
diff --git a/ci/compile-tests/009-failure-processing/e6.v.orig b/ci/compile-tests/009-failure-processing/e6.v.orig
new file mode 100644
index 000000000..bb1f999b8
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/e6.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export b6.
diff --git a/ci/compile-tests/009-failure-processing/e7.v.orig b/ci/compile-tests/009-failure-processing/e7.v.orig
new file mode 100644
index 000000000..d5d8608e8
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/e7.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export b7.
diff --git a/ci/compile-tests/009-failure-processing/e8.v.orig b/ci/compile-tests/009-failure-processing/e8.v.orig
new file mode 100644
index 000000000..3c9098cc1
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/e8.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export b8.
diff --git a/ci/compile-tests/009-failure-processing/e9.v.orig b/ci/compile-tests/009-failure-processing/e9.v.orig
new file mode 100644
index 000000000..3060cac17
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/e9.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Require Export b9.
diff --git a/ci/compile-tests/009-failure-processing/f1.v.orig b/ci/compile-tests/009-failure-processing/f1.v.orig
new file mode 100644
index 000000000..690b745e7
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/f1.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition f : nat := 1.
diff --git a/ci/compile-tests/009-failure-processing/f10.v.orig b/ci/compile-tests/009-failure-processing/f10.v.orig
new file mode 100644
index 000000000..690b745e7
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/f10.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition f : nat := 1.
diff --git a/ci/compile-tests/009-failure-processing/f2.v.orig b/ci/compile-tests/009-failure-processing/f2.v.orig
new file mode 100644
index 000000000..690b745e7
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/f2.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition f : nat := 1.
diff --git a/ci/compile-tests/009-failure-processing/f3.v.orig b/ci/compile-tests/009-failure-processing/f3.v.orig
new file mode 100644
index 000000000..690b745e7
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/f3.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition f : nat := 1.
diff --git a/ci/compile-tests/009-failure-processing/f4.v.orig b/ci/compile-tests/009-failure-processing/f4.v.orig
new file mode 100644
index 000000000..690b745e7
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/f4.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition f : nat := 1.
diff --git a/ci/compile-tests/009-failure-processing/f5.v.orig b/ci/compile-tests/009-failure-processing/f5.v.orig
new file mode 100644
index 000000000..690b745e7
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/f5.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition f : nat := 1.
diff --git a/ci/compile-tests/009-failure-processing/f6.v.orig b/ci/compile-tests/009-failure-processing/f6.v.orig
new file mode 100644
index 000000000..690b745e7
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/f6.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition f : nat := 1.
diff --git a/ci/compile-tests/009-failure-processing/f7.v.orig b/ci/compile-tests/009-failure-processing/f7.v.orig
new file mode 100644
index 000000000..690b745e7
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/f7.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition f : nat := 1.
diff --git a/ci/compile-tests/009-failure-processing/f8.v.orig b/ci/compile-tests/009-failure-processing/f8.v.orig
new file mode 100644
index 000000000..690b745e7
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/f8.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition f : nat := 1.
diff --git a/ci/compile-tests/009-failure-processing/f9.v.orig b/ci/compile-tests/009-failure-processing/f9.v.orig
new file mode 100644
index 000000000..690b745e7
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/f9.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition f : nat := 1.
diff --git a/ci/compile-tests/009-failure-processing/g1.v.orig b/ci/compile-tests/009-failure-processing/g1.v.orig
new file mode 100644
index 000000000..cd9aba373
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/g1.v.orig
@@ -0,0 +1,25 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 1
+ * coqc-delay X
+ *)
+
+(* coqdep error *)
+Require Export f1 h1
diff --git a/ci/compile-tests/009-failure-processing/g10.v.orig b/ci/compile-tests/009-failure-processing/g10.v.orig
new file mode 100644
index 000000000..e809ebc56
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/g10.v.orig
@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 1
+ * coqc-delay 0
+ *)
+
+
+Require Export f10 h10.
+
+(* coqc error *)
+XXX.
diff --git a/ci/compile-tests/009-failure-processing/g2.v.orig b/ci/compile-tests/009-failure-processing/g2.v.orig
new file mode 100644
index 000000000..be34de06b
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/g2.v.orig
@@ -0,0 +1,25 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 1
+ * coqc-delay X
+ *)
+
+(* coqdep error *)
+Require Export f2 h2
diff --git a/ci/compile-tests/009-failure-processing/g3.v.orig b/ci/compile-tests/009-failure-processing/g3.v.orig
new file mode 100644
index 000000000..666e4ceac
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/g3.v.orig
@@ -0,0 +1,25 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 1
+ * coqc-delay X
+ *)
+
+(* coqdep error *)
+Require Export f3 h3
diff --git a/ci/compile-tests/009-failure-processing/g4.v.orig b/ci/compile-tests/009-failure-processing/g4.v.orig
new file mode 100644
index 000000000..5b3d6c96f
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/g4.v.orig
@@ -0,0 +1,25 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 1
+ * coqc-delay X
+ *)
+
+(* coqdep error *)
+Require Export f4 h4
diff --git a/ci/compile-tests/009-failure-processing/g5.v.orig b/ci/compile-tests/009-failure-processing/g5.v.orig
new file mode 100644
index 000000000..6e901f343
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/g5.v.orig
@@ -0,0 +1,25 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 1
+ * coqc-delay X
+ *)
+
+(* coqdep error *)
+Require Export f5 h5
diff --git a/ci/compile-tests/009-failure-processing/g6.v.orig b/ci/compile-tests/009-failure-processing/g6.v.orig
new file mode 100644
index 000000000..20d037516
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/g6.v.orig
@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 1
+ *)
+
+
+Require Export f6 h6.
+
+(* coqc error *)
+XXX.
diff --git a/ci/compile-tests/009-failure-processing/g7.v.orig b/ci/compile-tests/009-failure-processing/g7.v.orig
new file mode 100644
index 000000000..bc5628002
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/g7.v.orig
@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+
+Require Export f7 h7.
+
+(* coqc error *)
+XXX.
diff --git a/ci/compile-tests/009-failure-processing/g8.v.orig b/ci/compile-tests/009-failure-processing/g8.v.orig
new file mode 100644
index 000000000..acd04dcfe
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/g8.v.orig
@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+
+Require Export f8 h8.
+
+(* coqc error *)
+XXX.
diff --git a/ci/compile-tests/009-failure-processing/g9.v.orig b/ci/compile-tests/009-failure-processing/g9.v.orig
new file mode 100644
index 000000000..f1ed88bde
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/g9.v.orig
@@ -0,0 +1,28 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 1
+ *)
+
+
+Require Export f9 h9.
+
+(* coqc error *)
+XXX.
diff --git a/ci/compile-tests/009-failure-processing/h1.v.orig b/ci/compile-tests/009-failure-processing/h1.v.orig
new file mode 100644
index 000000000..7df987076
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/h1.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition h : nat := 2.
diff --git a/ci/compile-tests/009-failure-processing/h10.v.orig b/ci/compile-tests/009-failure-processing/h10.v.orig
new file mode 100644
index 000000000..7df987076
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/h10.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition h : nat := 2.
diff --git a/ci/compile-tests/009-failure-processing/h2.v.orig b/ci/compile-tests/009-failure-processing/h2.v.orig
new file mode 100644
index 000000000..7df987076
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/h2.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition h : nat := 2.
diff --git a/ci/compile-tests/009-failure-processing/h3.v.orig b/ci/compile-tests/009-failure-processing/h3.v.orig
new file mode 100644
index 000000000..7df987076
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/h3.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition h : nat := 2.
diff --git a/ci/compile-tests/009-failure-processing/h4.v.orig b/ci/compile-tests/009-failure-processing/h4.v.orig
new file mode 100644
index 000000000..7df987076
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/h4.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition h : nat := 2.
diff --git a/ci/compile-tests/009-failure-processing/h5.v.orig b/ci/compile-tests/009-failure-processing/h5.v.orig
new file mode 100644
index 000000000..7df987076
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/h5.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition h : nat := 2.
diff --git a/ci/compile-tests/009-failure-processing/h6.v.orig b/ci/compile-tests/009-failure-processing/h6.v.orig
new file mode 100644
index 000000000..7df987076
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/h6.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition h : nat := 2.
diff --git a/ci/compile-tests/009-failure-processing/h7.v.orig b/ci/compile-tests/009-failure-processing/h7.v.orig
new file mode 100644
index 000000000..7df987076
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/h7.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition h : nat := 2.
diff --git a/ci/compile-tests/009-failure-processing/h8.v.orig b/ci/compile-tests/009-failure-processing/h8.v.orig
new file mode 100644
index 000000000..7df987076
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/h8.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition h : nat := 2.
diff --git a/ci/compile-tests/009-failure-processing/h9.v.orig b/ci/compile-tests/009-failure-processing/h9.v.orig
new file mode 100644
index 000000000..7df987076
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/h9.v.orig
@@ -0,0 +1,24 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  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.
+ *)
+
+(* Specify delays for coqdep and coqc when processing this file:
+ * coqdep-delay 0
+ * coqc-delay 0
+ *)
+
+Definition h : nat := 2.
diff --git a/ci/compile-tests/009-failure-processing/runtest.el b/ci/compile-tests/009-failure-processing/runtest.el
new file mode 100644
index 000000000..f20ae1214
--- /dev/null
+++ b/ci/compile-tests/009-failure-processing/runtest.el
@@ -0,0 +1,142 @@
+;; This file is part of Proof General.
+;;
+;; © Copyright 2021  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 a partially successful and partially failing compilation with
+;; coq-compile-keep-going. Check that the right files are compiled,
+;; locked and unlocked. Check also the case, where unlocking of failed
+;; files must be delayed, because some earlier successful require job
+;; has not yet locked its ancestors.
+;;
+;; The dependencies in this test are:
+;;
+;;    Rb    Rc  Rd
+;;    |     |   |
+;;    |     c   |
+;;    |    /|   |
+;;    |   / |   |
+;;    |  e  |   d
+;;    | ?   |   |
+;;    |?    |   |
+;;    b     g   /
+;;    |   _/|  /
+;;    | _/  | /
+;;    |/    |/
+;;    f     h
+;;
+;; Rb, Rc and Rd are three different require commands in file a. The
+;; dependency e -> b is not present in test 5 and test 10 (but in all
+;; other tests). The error always happens in file g, for test 1-5 with
+;; coqdep, for tests 6-10 with coqc. There are 10 tests, each with
+;; slighly different delays, in 10 versions of the sources, e.g.,
+;; a1-a10, b1-b10, and so on.
+;;
+;; For tests 1-5 coqdep fails on g, when this happens
+;;
+;; 1: Rb is ready and d still busy
+;; 2: f is ready and b and d are still busy and d finishes last
+;; 3: f is ready and b and d are still busy and b finishes last
+;; 4: RB is ready and Rd is queue waiting
+;; 5: without dependency e -> b: Rc, Rd are queue waiting, b finishes last
+;;
+;;
+;; For tests 6-10 coqc fails on g, when this happens
+;;
+;; 6: Rb is ready and d still busy
+;; 7: f is ready and b and d are still busy and d finishes last
+;; 8: f is ready and b and d are still busy and b finishes last
+;; 9: RB is ready and Rd is queue waiting
+;; 10: without dependency b -> e: Rc, Rd are queue waiting, b finishes last
+
+
+
+;; require cct-lib for the elisp compilation, otherwise this is present already
+(require 'cct-lib)
+
+;;; set configuration
+(cct-configure-proof-general)
+(configure-delayed-coq)    
+
+(defconst pre-b-ancestors '("b" "f")
+    "Ancestors of b without suffixes.")
+
+(defconst pre-all-compiled (append pre-b-ancestors '("e" "h" "d"))
+  "All files that get compiled.")
+
+(defun pre-not-compiled (n)
+  "List of file name stems for which coqc must not be called.
+Files for which coqc must not be called have an ``X'' in
+coqc-delay. For such files `compile-test-start-delayed' would
+create a ``.X'' file, whose absense is checked in the test."
+  (cond
+   ((< n 6) '("g" "c"))
+   (t       '("c"))))
+
+(defconst pre-all-unlocked '("c" "d" "e" "g" "h")
+  "All stems of files that should be unlocked after compilation.")
+
+(defun b-ancestors (n)
+  "Ancestors of b for part N."
+  (mapcar (lambda (f) (format "./%s%d.v" f n)) pre-b-ancestors))
+
+(defun all-compiled (n)
+  "All files that get compiled for part N."
+  (mapcar (lambda (f) (format "./%s%d.v" f n)) pre-all-compiled))
+
+(defun all-compiled-vo (n)
+  "All vo files for part N."
+  (mapcar 'cct-library-vo-of-v-file (all-compiled n)))
+
+(defun not-compiled (n)
+  "Files that should not be compiled for part N, see `pre-not-compiled'."
+  (mapcar (lambda (f) (format "./%s%d.v.X" f n)) (pre-not-compiled n)))
+
+(defun all-unlocked (n)
+  "All files that should be unlocked after compilation for part N."
+  (mapcar (lambda (f) (format "./%s%d.v" f n)) pre-all-unlocked))
+
+
+;;; Define the test
+
+(defun test-failure-processing (n)
+  "Test partially successful and partially failing compilation, part N."
+  ;; (setq cct--debug-tests t)
+  ;; (setq coq--debug-auto-compilation t)
+  (find-file (format "a%d.v" n))
+  (message "coqdep: %s\ncoqc: %s\nPATH %s\nexec-path: %s"
+           coq-dependency-analyzer
+           coq-compiler
+           (getenv "PATH")
+           exec-path)
+
+  (message "\n%d. Partially failing compilation part %d\n" n n)
+  (cct-process-to-line 28)
+  (cct-check-locked 25 'locked)
+  (cct-check-locked 26 'unlocked)
+  (cct-locked-ancestors 25 (b-ancestors n))
+  (cct-check-files-locked 24 'locked (b-ancestors n))
+  (cct-check-files-locked 1 'unlocked (all-unlocked n))
+  (cct-files-are-readable (all-compiled-vo n))
+  (cct-files-dont-exist (not-compiled n)))
+
+
+(ert-deftest cct-failure-processing-01 () (test-failure-processing 1))
+(ert-deftest cct-failure-processing-02 () (test-failure-processing 2))
+(ert-deftest cct-failure-processing-03 () (test-failure-processing 3))
+(ert-deftest cct-failure-processing-04 () (test-failure-processing 4))
+(ert-deftest cct-failure-processing-05 () (test-failure-processing 5))
+(ert-deftest cct-failure-processing-06 () (test-failure-processing 6))
+(ert-deftest cct-failure-processing-07 () (test-failure-processing 7))
+(ert-deftest cct-failure-processing-08 () (test-failure-processing 8))
+(ert-deftest cct-failure-processing-09 () (test-failure-processing 9))
+(ert-deftest cct-failure-processing-10 () (test-failure-processing 10))
diff --git a/ci/compile-tests/README.md b/ci/compile-tests/README.md
index 7c939741b..3bf3b62dd 100644
--- a/ci/compile-tests/README.md
+++ b/ci/compile-tests/README.md
@@ -32,10 +32,14 @@ All tests are for parallel background compilation.
 : test that the default/current directory is set correctly
   independent of user/emacs changing the current buffer during
   first and second stage compilation
+009-failure-processing
+: check ancestor unlocking for a failed job with
+  coq-compile-keep-going; test also the case, where the last
+  (failed) require job must be delayed, because some queue
+  dependee is still processing
 
 # Tests currently missing
 
-- unlock checks for ancestors of failed jobs in different cases
 - a job depending on a failed dependee, where the dependee has
   been finished before
 - coq-par-create-file-job detects a dependency cycle
diff --git a/ci/compile-tests/bin/compile-test-start-delayed b/ci/compile-tests/bin/compile-test-start-delayed
index 50ae7a03a..7cd40de6b 100755
--- a/ci/compile-tests/bin/compile-test-start-delayed
+++ b/ci/compile-tests/bin/compile-test-start-delayed
@@ -21,11 +21,17 @@ function usage(){
 	Start program prog with arguments args with some delay. There
 	must be at least one argument in args and the last one must be
 	a file or something that becomes a file when ".v" is appended.
-        The delay is taken from a line in that file that
+	The delay is taken from a line in that file that
 	contains the key, followed by a space and the delay in seconds
 	(maybe somewhere in the middle of the line). The file must
 	contain at most one line containing key. When there is no line
-	containing key the delay is zero.
+	containing key the delay is zero. As a special case, a delay
+	equal to X means to record the fact that prog has been called
+	on file by creating a file with suffix ".X" added to the name
+	of file. The absence of this .X file can then be used, for
+	instance, to check that prog has not been called on file. With
+	delay equal to X, the real delay is 0.
+        Fractional delays are properly handled.
 EOF
 }
 
@@ -53,22 +59,26 @@ if [ ! -f "$file" ] ; then
     fi
 fi
 
-delay=$(sed -ne "/$key/ s/.*$key \([0-9]*\).*/\1/p" $file)
+delay=$(sed -ne "/$key/ s/.*$key \([X0-9.]*\).*/\1/p" $file)
 
 if [ -z "$delay" ] ; then
     # echo compile-test-start-delayed: key $key not found in $file >&9
     delay=0
+elif [ "$delay" = "X" ] ; then
+    echo compile-test-start-delayed: delay X for $file >&9
+    delay=0
+    touch $file.X
 fi
 
-if [ $delay -ne 0 ] ; then
-    date "+compile-test-start-delayed +%Y-%m-%d %T %Z" >&9
-    echo delay $delay for $@ >&9
+# use string comparison on $delay to permit fractional values
+if [ $delay != 0 ] ; then
+    date "+compile-test-start-delayed %T delay $delay for $*" >&9
+    sleep $delay
+    date "+compile-test-start-delayed %T start now $*" >&9
+else
+    date "+compile-test-start-delayed %T start without delay $*" >&9
 fi
 
-sleep $delay
-date "+compile-test-start-delayed +%Y-%m-%d %T %Z" >&9
-echo start $@ >&9
-
 #set -x
 #echo "$@"
 set +e
diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el
index 98b71ea79..71343c88d 100644
--- a/ci/compile-tests/cct-lib.el
+++ b/ci/compile-tests/cct-lib.el
@@ -214,6 +214,20 @@ region of the buffer and signals a test failure if not."
            (funcall (if locked '< '>)
                     (point) (span-end proof-locked-span)))))))
 
+(defun cct-check-files-locked (line lock-state files)
+  "Check that all FILES at line number LINE have lock state LOCK-STATE.
+LOCK-STATE must be either 'locked or 'unlocked. FILES must be
+list of file names."
+  (when cct--debug-tests
+    (message "check files %s at line %d: %s"
+             (if (eq lock-state 'locked) "locked" "unlocked") line files))
+  (save-current-buffer
+    (mapc
+     (lambda (file)
+       (find-file file)
+       (cct-check-locked line lock-state))
+     files)))
+
 (defun cct-locked-ancestors (line ancestors)
   "Check that the vanilla span at line LINE has ANCESTORS recorded.
 The comparison treats ANCESTORS as set but the file names must
@@ -297,6 +311,12 @@ or changed since recording the time in the association."
     (message "Files should exist and be readable: %s" files))
   (mapc (lambda (fname) (should (file-readable-p fname))) files))
 
+(defun cct-files-dont-exist (files)
+  "Check that FILES don't exist."
+  (when cct--debug-tests
+    (message "Files should not exist: %s" files))
+  (mapc (lambda (fname) (should-not (file-exists-p fname))) files))
+
 (defun cct-generic-check-main-buffer
     (main-buf main-unlocked main-locked main-sum-line new-sum
               vo-times recompiled-files require-ancestors
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 19988c355..1e2d757ef 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -1026,10 +1026,12 @@ function and reported appropriately."
                 (get (process-get process 'coq-compilation-job) 'current-dir)))
 	  (when coq--debug-auto-compilation
 	    (message
-             "%s %s: process status changed to %s (default-dir %s curr buf %s)"
+             (concat "%s %s: TTT process status changed to %s  "
+                     "command: %s\n  default-dir: %s curr buf %s")
 	     (get (process-get process 'coq-compilation-job) 'name)
 	     (process-name process)
 	     event
+             (mapconcat 'identity (process-get process 'coq-process-command) " ")
              default-directory
              (buffer-name)))
 	  (cond
@@ -1558,6 +1560,9 @@ Simple wrapper around `coq-par-kickoff-queue-maybe' to set
 `default-directory' when entering background compilation
 functions from `proof-action-list'."
   (let ((default-directory (get job 'current-dir)))
+    (when coq--debug-auto-compilation
+      (message "%s: TTT retry queue kickoff after processing action list"
+               (get job 'name)))
     (coq-par-kickoff-queue-maybe job)))
 
 (defun coq-par-kickoff-queue-maybe (job)
@@ -1835,7 +1840,7 @@ was queued."
     (put job 'temp-require-file temp-file)
     (with-temp-file temp-file (insert require-command))
     (when coq--debug-auto-compilation
-      (message "%s: start coqdep for require job for file %s"
+      (message "%s: TTT start coqdep for require job for file %s"
 	       (get job 'name)
 	       (get job 'temp-require-file)))
     (coq-par-start-process
@@ -1854,6 +1859,10 @@ Lock the source file and start the coqdep background process."
 	     (eq (get job 'lock-state) 'unlocked))
     (proof-register-possibly-new-processed-file (get job 'src-file))
     (put job 'lock-state 'locked))
+  (when coq--debug-auto-compilation
+    (message "%s: TTT start coqdep for file job for file %s"
+	     (get job 'name)
+	     (get job 'src-file)))
   (coq-par-start-process
    coq-dependency-analyzer
    (coq-par-coqdep-arguments (get job 'src-file) (get job 'load-path))
@@ -1877,6 +1886,10 @@ used."
      ((eq (get job 'use-quick) 'vos) (push "-vos" arguments))
      ((eq (get job 'use-quick) 'vio) (push "-quick" arguments))
      (t t))
+    (when coq--debug-auto-compilation
+      (message "%s: TTT start coqc compile for file job for file %s"
+	       (get job 'name)
+	       (get job 'src-file)))
     (coq-par-start-process
      coq-compiler
      arguments
@@ -1891,6 +1904,10 @@ used."
              (get job 'name)
              (get job 'src-file)))
   (message "coqc -vok %s" (get job 'src-file))
+  (when coq--debug-auto-compilation
+    (message "%s: TTT start coqc -vok for file job for file %s"
+	     (get job 'name)
+	     (get job 'src-file)))
   (let ((arguments
          (coq-par-coqc-arguments (get job 'src-file) (get job 'load-path))))
     (push "-vok" arguments)
@@ -1912,6 +1929,10 @@ used."
 	       (get job 'name)
 	       (get job 'src-file)))
     (message "vio2vo %s" (get job 'src-file))
+    (when coq--debug-auto-compilation
+      (message "%s: TTT start vio2vo for file job for file %s"
+	       (get job 'name)
+	       (get job 'src-file)))
     (coq-par-start-process
      ;; in 8.9.1 and before only coqtop accepts -schedule-vio2vo
      ;; after change 103f59e only coqc accepts -schedule-vio2vo
@@ -2067,11 +2088,7 @@ Recurse for queue dependants."
     (cl-assert (not (eq (get job 'state) 'ready))
 	    nil "coq-par-mark-queue-failing impossible state")
     (when coq--debug-auto-compilation
-      (message "%s: mark as failed, %s"
-	       (get job 'name)
-	       (if (eq (get job 'state) 'waiting-queue)
-		   "and unlock ancestors"
-		 "wait")))
+      (message "%s: mark as failed" (get job 'name)))
     (when (get job 'queue-dependant)
       (coq-par-mark-queue-failing (get job 'queue-dependant)))))