add Coq compile test for a delayed require

32 files changed, 1197 insertions, 63 deletions

diff --git a/ci/compile-tests/005-change-recompile/runtest.el b/ci/compile-tests/005-change-recompile/runtest.el
index c5d7f9b3..825ad834 100644
--- a/ci/compile-tests/005-change-recompile/runtest.el
+++ b/ci/compile-tests/005-change-recompile/runtest.el
@@ -57,44 +57,22 @@
   "All vo ancestors files.")
   
 
-(defun cct-replace-last-word (line word)
-  "Replace last word in line LINE with WORD.
-In current buffer, go to the end of line LINE and one word
-backward. Replace the word there with WORD."
-  (cct-goto-line line)
-  (end-of-line)
-  (backward-word)
-  (kill-word 1)
-  (insert word))
-
-(defun cct-check-main-buffer (vo-times new-sum recompiled-files
+(defun check-main-buffer (vo-times new-sum recompiled-files
                                        other-locked-files)
-  "Perform various checks for recompilation in buffer a.v.
-Combine all the following tests in this order:
-- line 21 in a.v is unlocked
-- after replacing the sum on line 28 with NEW-SUM, a.v can be
-  processed until line 38
-- files in VO-TIMES not listed in RECOMPILED-FILES have the same
-  last change time as in VO-TIMES
-- files in RECOMPILED-FILES have a newer change time
-- the spans in line 22 and 23 hold the ancestors of b and c, respectively.
-- all the buffers in OTHER-LOCKED-FILES are locked until line 18."
-  (let (splitted)
-    (set-buffer "a.v")
-    (cct-check-locked 21 'unlocked)
-    (cct-replace-last-word 28 new-sum)
-    (cct-process-to-line 38)
-    (cct-check-locked 37 'locked)
-    (setq splitted (cct-split-change-times vo-times recompiled-files))
-    (cct-unmodified-change-times (car splitted))
-    (cct-older-change-times (cdr splitted))
-    (cct-locked-ancestors 22 b-ancestors)
-    (cct-locked-ancestors 23 c-ancestors)
-    (mapc
-     (lambda (b)
-       (set-buffer b)
-       (cct-check-locked 18 'locked))
-     other-locked-files)))
+  "Perform various checks in buffer a.v.
+See `cct-generic-check-main-buffer'."
+  (cct-generic-check-main-buffer
+   "a.v"                                ; main-buf
+   21                                   ; main-unlocked
+   37                                   ; main-locked
+   28                                   ; main-sum-line
+   new-sum
+   vo-times
+   recompiled-files
+   `((22 . ,b-ancestors) (23 . ,c-ancestors)) ; require-ancestors
+   other-locked-files
+   18                                   ; other-locked-line
+   ))
 
 
 ;;; The test itself
@@ -116,7 +94,7 @@ Combine all the following tests in this order:
     ;; 2. retract and process again - nothing should be compiled
     (message "\n2. retract and process again - nothing should be compiled\n")
     (cct-process-to-line 21)
-    (cct-check-main-buffer vo-times "35" nil nil)
+    (check-main-buffer vo-times "35" nil nil)
 
     ;; 3. change c and process again - only c should be compiled
     (message "\n3. change c and process again - only c should be compiled\n")
@@ -124,7 +102,7 @@ Combine all the following tests in this order:
     (push "c.v" other-locked-files)
     (cct-check-locked 23 'locked)
     (cct-replace-last-word 23 "4")
-    (cct-check-main-buffer vo-times "36" '("./c.vo") other-locked-files)
+    (check-main-buffer vo-times "36" '("./c.vo") other-locked-files)
 
     ;; 4. change h and process again - everything except g should get compiled
     (message (concat "\n4. change h and process again - "
@@ -134,7 +112,7 @@ Combine all the following tests in this order:
     (push "h.v" other-locked-files)
     (cct-check-locked 21 'locked)
     (cct-replace-last-word 21 "10")
-    (cct-check-main-buffer
+    (check-main-buffer
      vo-times "38" '("./b.vo" "./c.vo" "./d.vo" "./e.vo" "./f.vo" "./h.vo")
      other-locked-files)
     
@@ -152,7 +130,7 @@ Combine all the following tests in this order:
     (cct-check-locked 23 'unlocked)
     (cct-replace-last-word 23 "10")
 
-    (cct-check-main-buffer
+    (check-main-buffer
      vo-times "45" '("./b.vo" "./c.vo" "./d.vo" "./f.vo") other-locked-files)
 
     ;; 6. change d and b and process again - only d and b should get compiled
@@ -167,7 +145,7 @@ Combine all the following tests in this order:
     (cct-check-locked 23 'unlocked)
     (cct-replace-last-word 23 "13")    ; increase by 6
 
-    (cct-check-main-buffer vo-times "56" '("./b.vo" "./d.vo")
+    (check-main-buffer vo-times "56" '("./b.vo" "./d.vo")
                            other-locked-files)
     
     ;; 7. delete b and process again - only b should get compiled
@@ -177,7 +155,7 @@ Combine all the following tests in this order:
     (delete-file "b.vo")
     (set-buffer "a.v")
     (cct-process-to-line 21)
-    (cct-check-main-buffer vo-times "56" '("./b.vo") other-locked-files)
+    (check-main-buffer vo-times "56" '("./b.vo") other-locked-files)
     
     ;; 8. delete h and process again - everything except g should get compiled
     (message (concat "\n8. delete h and process again - "
@@ -186,7 +164,7 @@ Combine all the following tests in this order:
     (delete-file "h.vo")
     (set-buffer "a.v")
     (cct-process-to-line 21)
-    (cct-check-main-buffer
+    (check-main-buffer
      vo-times "56" '("./b.vo" "./c.vo" "./d.vo" "./e.vo" "./f.vo" "./h.vo")
      other-locked-files)
     
@@ -201,7 +179,7 @@ Combine all the following tests in this order:
     (delete-file "g.vo")
     (set-buffer "a.v")
     (cct-process-to-line 21)
-    (cct-check-main-buffer vo-times "63" '("./b.vo" "./d.vo" "./g.vo")
+    (check-main-buffer vo-times "63" '("./b.vo" "./d.vo" "./g.vo")
                            other-locked-files)
     
     ;; 10. delete d, change g and process again - only b, d and g should
@@ -216,6 +194,6 @@ Combine all the following tests in this order:
     (cct-replace-last-word 21 "15")     ; increase by 8
     (set-buffer "a.v")
     (cct-process-to-line 21)
-    (cct-check-main-buffer vo-times "71" '("./b.vo" "./d.vo" "./g.vo")
+    (check-main-buffer vo-times "71" '("./b.vo" "./d.vo" "./g.vo")
                            other-locked-files)
   ))
diff --git a/ci/compile-tests/007-slow-require/Makefile b/ci/compile-tests/007-slow-require/Makefile
new file mode 100644
index 00000000..b99eebc1
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/Makefile
@@ -0,0 +1,35 @@
+# 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 \
+	a2.v b2.v c2.v d2.v \
+	a3.v b3.v c3.v d3.v \
+	a4.v b4.v c4.v d4.v \
+	a5.v b5.v c5.v d5.v \
+	a6.v b6.v c6.v d6.v
+
+.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 $(TEST_SOURCES)
diff --git a/ci/compile-tests/007-slow-require/a1.v.orig b/ci/compile-tests/007-slow-require/a1.v.orig
new file mode 100644
index 00000000..6b3e3349
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/a1.v.orig
@@ -0,0 +1,41 @@
+(* 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.
+ *)
+
+(* 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 (* coqdep-delay 2 *) c1.
+(* This is line 27 *)
+
+
+(* This is line 30 *)
+Definition sum : nat := 9.
+
+
+(* This is line 34 *)
+Lemma x : b + c + d = sum.
+Proof using.
+  unfold b, c, d, sum in *.
+  simpl.
+  trivial.
+Qed.
+(* This is line 41 *)
diff --git a/ci/compile-tests/007-slow-require/a2.v.orig b/ci/compile-tests/007-slow-require/a2.v.orig
new file mode 100644
index 00000000..60ac1279
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/a2.v.orig
@@ -0,0 +1,41 @@
+(* 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.
+ *)
+
+(* 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.
+(* This is line 27 *)
+
+
+(* This is line 30 *)
+Definition sum : nat := 9.
+
+
+(* This is line 34 *)
+Lemma x : b + c + d = sum.
+Proof using.
+  unfold b, c, d, sum in *.
+  simpl.
+  trivial.
+Qed.
+(* This is line 41 *)
diff --git a/ci/compile-tests/007-slow-require/a3.v.orig b/ci/compile-tests/007-slow-require/a3.v.orig
new file mode 100644
index 00000000..8337b2ad
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/a3.v.orig
@@ -0,0 +1,41 @@
+(* 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.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export (* coqdep-delay 2 *) b3.
+Require Export c3.
+(* This is line 27 *)
+
+
+(* This is line 30 *)
+Definition sum : nat := 9.
+
+
+(* This is line 34 *)
+Lemma x : b + c + d = sum.
+Proof using.
+  unfold b, c, d, sum in *.
+  simpl.
+  trivial.
+Qed.
+(* This is line 41 *)
diff --git a/ci/compile-tests/007-slow-require/a4.v.orig b/ci/compile-tests/007-slow-require/a4.v.orig
new file mode 100644
index 00000000..fd5d4b60
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/a4.v.orig
@@ -0,0 +1,41 @@
+(* 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.
+ *)
+
+(* 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.
+(* This is line 27 *)
+
+
+(* This is line 30 *)
+Definition sum : nat := 9.
+
+
+(* This is line 34 *)
+Lemma x : b + c + d = sum.
+Proof using.
+  unfold b, c, d, sum in *.
+  simpl.
+  trivial.
+Qed.
+(* This is line 41 *)
diff --git a/ci/compile-tests/007-slow-require/a5.v.orig b/ci/compile-tests/007-slow-require/a5.v.orig
new file mode 100644
index 00000000..b6d7edbb
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/a5.v.orig
@@ -0,0 +1,41 @@
+(* 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.
+ *)
+
+(* 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.
+(* This is line 27 *)
+
+
+(* This is line 30 *)
+Definition sum : nat := 9.
+
+
+(* This is line 34 *)
+Lemma x : b + c + d = sum.
+Proof using.
+  unfold b, c, d, sum in *.
+  simpl.
+  trivial.
+Qed.
+(* This is line 41 *)
diff --git a/ci/compile-tests/007-slow-require/a6.v.orig b/ci/compile-tests/007-slow-require/a6.v.orig
new file mode 100644
index 00000000..a9bb279f
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/a6.v.orig
@@ -0,0 +1,41 @@
+(* 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.
+ *)
+
+(* 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.
+(* This is line 27 *)
+
+
+(* This is line 30 *)
+Definition sum : nat := 9.
+
+
+(* This is line 34 *)
+Lemma x : b + c + d = sum.
+Proof using.
+  unfold b, c, d, sum in *.
+  simpl.
+  trivial.
+Qed.
+(* This is line 41 *)
diff --git a/ci/compile-tests/007-slow-require/b1.v.orig b/ci/compile-tests/007-slow-require/b1.v.orig
new file mode 100644
index 00000000..926bed1d
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/b1.v.orig
@@ -0,0 +1,27 @@
+(* 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 d1.
+
+(* This is line 27 *)
+Definition b : nat := 2.
diff --git a/ci/compile-tests/007-slow-require/b2.v.orig b/ci/compile-tests/007-slow-require/b2.v.orig
new file mode 100644
index 00000000..b9cff7ea
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/b2.v.orig
@@ -0,0 +1,27 @@
+(* 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 d2.
+
+(* This is line 26 *)
+Definition b : nat := 2.
diff --git a/ci/compile-tests/007-slow-require/b3.v.orig b/ci/compile-tests/007-slow-require/b3.v.orig
new file mode 100644
index 00000000..51ab7a2f
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/b3.v.orig
@@ -0,0 +1,27 @@
+(* 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 d3.
+
+(* This is line 27 *)
+Definition b : nat := 2.
diff --git a/ci/compile-tests/007-slow-require/b4.v.orig b/ci/compile-tests/007-slow-require/b4.v.orig
new file mode 100644
index 00000000..fd8d331e
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/b4.v.orig
@@ -0,0 +1,27 @@
+(* 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 2
+ * coqc-delay 0
+ *)
+
+Require Export d4.
+
+(* This is line 27 *)
+Definition b : nat := 2.
diff --git a/ci/compile-tests/007-slow-require/b5.v.orig b/ci/compile-tests/007-slow-require/b5.v.orig
new file mode 100644
index 00000000..3fec38a3
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/b5.v.orig
@@ -0,0 +1,27 @@
+(* 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 d5.
+
+(* This is line 27 *)
+Definition b : nat := 2.
diff --git a/ci/compile-tests/007-slow-require/b6.v.orig b/ci/compile-tests/007-slow-require/b6.v.orig
new file mode 100644
index 00000000..2b957e6e
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/b6.v.orig
@@ -0,0 +1,27 @@
+(* 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 d6.
+
+(* This is line 27 *)
+Definition b : nat := 2.
diff --git a/ci/compile-tests/007-slow-require/c1.v.orig b/ci/compile-tests/007-slow-require/c1.v.orig
new file mode 100644
index 00000000..9df47c9b
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/c1.v.orig
@@ -0,0 +1,27 @@
+(* 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 d1.
+
+(* This is line 26 *)
+Definition c : nat := 3.
diff --git a/ci/compile-tests/007-slow-require/c2.v.orig b/ci/compile-tests/007-slow-require/c2.v.orig
new file mode 100644
index 00000000..b8db7474
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/c2.v.orig
@@ -0,0 +1,27 @@
+(* 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 2
+ * coqc-delay 0
+ *)
+
+Require Export d2.
+
+(* This is line 26 *)
+Definition c : nat := 3.
diff --git a/ci/compile-tests/007-slow-require/c3.v.orig b/ci/compile-tests/007-slow-require/c3.v.orig
new file mode 100644
index 00000000..04b225ab
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/c3.v.orig
@@ -0,0 +1,27 @@
+(* 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 d3.
+
+(* This is line 26 *)
+Definition c : nat := 3.
diff --git a/ci/compile-tests/007-slow-require/c4.v.orig b/ci/compile-tests/007-slow-require/c4.v.orig
new file mode 100644
index 00000000..400a8a6c
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/c4.v.orig
@@ -0,0 +1,27 @@
+(* 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 d4.
+
+(* This is line 26 *)
+Definition c : nat := 3.
diff --git a/ci/compile-tests/007-slow-require/c5.v.orig b/ci/compile-tests/007-slow-require/c5.v.orig
new file mode 100644
index 00000000..2fa5a612
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/c5.v.orig
@@ -0,0 +1,27 @@
+(* 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 d5.
+
+(* This is line 26 *)
+Definition c : nat := 3.
diff --git a/ci/compile-tests/007-slow-require/c6.v.orig b/ci/compile-tests/007-slow-require/c6.v.orig
new file mode 100644
index 00000000..fd0289bf
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/c6.v.orig
@@ -0,0 +1,27 @@
+(* 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 2
+ * coqc-delay 0
+ *)
+
+Require Export d6.
+
+(* This is line 26 *)
+Definition c : nat := 3.
diff --git a/ci/compile-tests/007-slow-require/d1.v.orig b/ci/compile-tests/007-slow-require/d1.v.orig
new file mode 100644
index 00000000..fec95787
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/d1.v.orig
@@ -0,0 +1,27 @@
+(* 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
+ *)
+
+
+
+(* This is line 26 *)
+Definition d : nat := 4.
diff --git a/ci/compile-tests/007-slow-require/d2.v.orig b/ci/compile-tests/007-slow-require/d2.v.orig
new file mode 100644
index 00000000..fec95787
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/d2.v.orig
@@ -0,0 +1,27 @@
+(* 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
+ *)
+
+
+
+(* This is line 26 *)
+Definition d : nat := 4.
diff --git a/ci/compile-tests/007-slow-require/d3.v.orig b/ci/compile-tests/007-slow-require/d3.v.orig
new file mode 100644
index 00000000..fec95787
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/d3.v.orig
@@ -0,0 +1,27 @@
+(* 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
+ *)
+
+
+
+(* This is line 26 *)
+Definition d : nat := 4.
diff --git a/ci/compile-tests/007-slow-require/d4.v.orig b/ci/compile-tests/007-slow-require/d4.v.orig
new file mode 100644
index 00000000..fec95787
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/d4.v.orig
@@ -0,0 +1,27 @@
+(* 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
+ *)
+
+
+
+(* This is line 26 *)
+Definition d : nat := 4.
diff --git a/ci/compile-tests/007-slow-require/d5.v.orig b/ci/compile-tests/007-slow-require/d5.v.orig
new file mode 100644
index 00000000..d2fae3f6
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/d5.v.orig
@@ -0,0 +1,27 @@
+(* 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 2
+ * coqc-delay 0
+ *)
+
+
+
+(* This is line 26 *)
+Definition d : nat := 4.
diff --git a/ci/compile-tests/007-slow-require/d6.v.orig b/ci/compile-tests/007-slow-require/d6.v.orig
new file mode 100644
index 00000000..b60d54a6
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/d6.v.orig
@@ -0,0 +1,27 @@
+(* 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 
+ * coqc-delay 4
+ *)
+
+
+
+(* This is line 26 *)
+Definition d : nat := 4.
diff --git a/ci/compile-tests/007-slow-require/runtest.el b/ci/compile-tests/007-slow-require/runtest.el
new file mode 100644
index 00000000..52c2f392
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/runtest.el
@@ -0,0 +1,211 @@
+;; 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 two require jobs with different delays such that
+;; coq-par-retire-top-level-job happens when the other require job is
+;; in each possible state. For specifying the different delays there
+;; are 6 mini projects, one for each test in this file. Each project
+;; consists of four files, a1.v, b1.v, c1.v and d1.v for the first one
+;; and a6.v, b6.v, c6.v and d6.v for the sixth one.
+;;
+;; The dependencies are the same in all projects:
+;; 
+;;           a
+;;          / \
+;;         b   c
+;;          \ /
+;;           d
+;;
+;; Test 1 delays coqdep on require c, such that queue kickoff happens
+;; in state 'enqueued-coqdep, the dependency link d->c is created when
+;; d is ready and kickoff-queue-maybe on require c happens when
+;; require b is in state 'ready.
+;;
+;; Test 2 delays coqdep on c, such that queue kickoff happens in state
+;; 'waiting-dep.
+;;
+;; Test 3 delays coqdep on require b, such that kickoff-queue-maybe on
+;; require c happens when require b is in state 'enqueued-coqdep and
+;; queue kickoff happens in state 'waiting-queue.
+;;
+;; Test 4 delays coqdep on b, such that kickoff-queue-maybe on require
+;; c happens when require b is in state 'waiting-dep.
+;;
+;; Test 5 delays coqdep on d, such that the second dependency on d is
+;; created when d is in state enqueued-coqdep.
+;;
+;; Test 6 delays coqdep on c for 2 seconds and coqc on d for 4
+;; seconds, such that the dependency link d->c is created when d is in
+;; state enqueued-coqc.
+
+;; 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" "./d")
+    "Ancestors of b without suffixes.")
+
+(defconst pre-c-ancestors '("./c")
+  "Ancestors of c without suffixes.")
+
+(defconst pre-all-ancestors (append pre-b-ancestors pre-c-ancestors)
+  "All ancestors without suffixes.")
+
+(defun b-ancestors (n)
+  "Ancestors of b for part N."
+  (mapcar (lambda (a) (concat a (format "%d.v" n))) pre-b-ancestors))
+
+(defun c-ancestors (n)
+  "Ancestors of c for part N."
+  (mapcar (lambda (a) (concat a (format "%d.v" n))) pre-c-ancestors))
+
+(defun all-ancestors (n)
+  "All ancestors for part N."
+  (mapcar (lambda (a) (concat a (format "%d.v" n))) pre-all-ancestors))
+
+(defun all-compiled-ancestors (n)
+  "All vo ancestor files for part N."
+  (mapcar 'cct-library-vo-of-v-file (all-ancestors n)))
+
+(defun check-main-buffer (n vo-times new-sum recompiled-files
+                                       other-locked-files)
+  "Perform various checks in buffer aN.v.
+See `cct-generic-check-main-buffer'."
+  (cct-generic-check-main-buffer
+   (format "a%d.v" n)                   ; main-buf
+   25                                   ; main-unlocked
+   41                                   ; main-locked
+   31                                   ; main-sum-line
+   new-sum
+   vo-times
+   recompiled-files
+   `((25 . ,(b-ancestors n)) (26 . ,(c-ancestors n))) ; require-ancestors
+   other-locked-files
+   27                                   ; other-locked-line
+   ))
+
+
+;;; Define the test
+
+(defun test-slow-require (n)
+  "Test part N of slow require job tests.
+XXX Test a setting where the second require job is still in state
+'enqueued-coqdep when the first one finishes."
+  (let*
+      ;; .v file names are used as file and as buffer names
+      ((av (format "a%d.v" n))
+       (bv (format "b%d.v" n))
+       (cv (format "c%d.v" n))
+       (dv (format "d%d.v" n))
+       ;; .vo names compared with ancestors, they need a "./" prefix
+       (bvo (concat "./" (cct-library-vo-of-v-file bv)))
+       (cvo (concat "./" (cct-library-vo-of-v-file cv)))
+       (dvo (concat "./" (cct-library-vo-of-v-file dv)))
+       vo-times other-locked-files)
+
+    ;; (setq cct--debug-tests t)
+    ;; (setq coq--debug-auto-compilation t)
+    (find-file av)
+    (message "coqdep: %s\ncoqc: %s\nPATH %s\nexec-path: %s"
+             coq-dependency-analyzer
+             coq-compiler
+             (getenv "PATH")
+             exec-path)
+
+    ;; 1. process original content - compile everything
+    (message "\n%d.1. process original content - compile everything\n" n)
+    ;;(setq coq--debug-auto-compilation t)
+    (cct-process-to-line 42)
+    (cct-check-locked 41 'locked)
+    (cct-locked-ancestors 25 (b-ancestors n))
+    (cct-locked-ancestors 26 (c-ancestors n))
+
+    ;; (cl-assert nil nil "exit")
+
+    (setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
+    ;; 2. retract and process again - nothing should be compiled
+    (message "\n%d.2. retract and process again - nothing should be compiled\n"
+             n)
+    (cct-process-to-line 24)
+    (check-main-buffer n vo-times "9" nil nil)
+
+    ;; 3. change d and process again - b and c should be compiled
+    (message "\n%d.3. change d and process again - b and c should be compiled\n"
+             n)
+    (find-file dv)
+    (push dv other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 27 "5")
+    (check-main-buffer n vo-times "10" (list bvo cvo dvo)
+                       other-locked-files)
+
+    ;; 4. change b and process again - only b should be compiled
+    (message "\n%d.4. change b and process again - only b should be compiled\n"
+             n)
+    (setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
+    (find-file bv)
+    (push bv other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 27 "4")
+    (check-main-buffer n vo-times "12" (list bvo) other-locked-files)
+
+    ;; 5. change c and process again - only c should be compiled
+    (message "\n%d.5. change c and process again - only c should be compiled\n"
+             n)
+    (setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
+    (find-file cv)
+    (push cv other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 27 "8")
+    (check-main-buffer n vo-times "17" (list cvo) other-locked-files)
+
+    ;; 6. delete d and process again - b and c should be compiled
+    (message "\n%d.6. delete d and process again - b and c should be compiled\n"
+             n)
+    (setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
+    (delete-file dvo)
+    (set-buffer av)
+    (cct-process-to-line 24)
+    (check-main-buffer n vo-times "17" (list bvo cvo dvo)
+                       other-locked-files)
+
+    ;; 7. delete b and process again - only b should be compiled
+    (message "\n%d.7. delete b and process again - only b should be compiled\n"
+             n)
+    (setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
+    (delete-file bvo)
+    (set-buffer av)
+    (cct-process-to-line 24)
+    (check-main-buffer n vo-times "17" (list bvo) other-locked-files)
+
+    ;; 8. delete c and process again - only c should be compiled
+    (message "\n%d.8. delete c and process again - only c should be compiled\n"
+             n)
+    (setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
+    (delete-file cvo)
+    (set-buffer av)
+    (cct-process-to-line 24)
+    (check-main-buffer n vo-times "17" (list cvo) other-locked-files)
+  ))
+
+
+(ert-deftest cct-slow-require-1 () (test-slow-require 1))
+(ert-deftest cct-slow-require-2 () (test-slow-require 2))
+(ert-deftest cct-slow-require-3 () (test-slow-require 3))
+(ert-deftest cct-slow-require-4 () (test-slow-require 4))
+(ert-deftest cct-slow-require-5 () (test-slow-require 5))
+(ert-deftest cct-slow-require-6 () (test-slow-require 6))
diff --git a/ci/compile-tests/README.md b/ci/compile-tests/README.md
new file mode 100644
index 00000000..3b0364e2
--- /dev/null
+++ b/ci/compile-tests/README.md
@@ -0,0 +1,18 @@
+This directory contains tests for the parallel background
+compilation feature for Coq. The test check that
+- files get compiled in the right order, 
+- after changes, precisely those files that need recompilation
+  are compiled
+- files are locked and registered in the right require commands.
+
+
+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
+- coq-par-create-file-job finds a job in state waiting-dep
+- coq-par-kickoff-queue-maybe is done when the queue dependee is
+  in state waiting-queue
+- coq-par-create-file-job finds a failed job
+- all tests in all quick and all vos variants
diff --git a/ci/compile-tests/bin/compile-test-start-delayed b/ci/compile-tests/bin/compile-test-start-delayed
new file mode 100755
index 00000000..f528f4d1
--- /dev/null
+++ b/ci/compile-tests/bin/compile-test-start-delayed
@@ -0,0 +1,61 @@
+#!/bin/bash
+#
+# 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)
+#
+# See function usage for documentation.
+
+set -e
+#set -x
+
+function usage(){
+    cat <<-EOF
+	usage: compile-test-start-delayed key prog args...
+
+	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. 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.
+EOF
+}
+
+if [ $# -lt 3 ] ; then
+    usage
+    exit 1
+fi
+
+# echo compile-test-start-delayed "$@"
+
+key="$1"
+file="${@: -1}"
+shift
+
+delay=$(sed -ne "/$key/ s/.*$key \([0-9]*\).*/\1/p" $file)
+
+if [ -z "$delay" ] ; then
+    # echo compile-test-start-delayed: key $key not found in $file >&9
+    delay=0
+fi
+
+if [ $delay -ne 0 ] ; then
+    date "+compile-test-start-delayed +%Y-%m-%d %T %Z" >&9
+    echo delay $delay for $@ >&9
+fi
+
+sleep $delay
+date "+compile-test-start-delayed +%Y-%m-%d %T %Z" >&9
+echo start $@ >&9
+
+#set -x
+#echo "$@"
+set +e
+exec "$@"
diff --git a/ci/compile-tests/bin/coqc-delayed b/ci/compile-tests/bin/coqc-delayed
new file mode 100755
index 00000000..26c92805
--- /dev/null
+++ b/ci/compile-tests/bin/coqc-delayed
@@ -0,0 +1,3 @@
+#!/bin/bash
+
+exec compile-test-start-delayed coqc-delay coqc "$*"
diff --git a/ci/compile-tests/bin/coqdep-delayed b/ci/compile-tests/bin/coqdep-delayed
new file mode 100755
index 00000000..f123770a
--- /dev/null
+++ b/ci/compile-tests/bin/coqdep-delayed
@@ -0,0 +1,3 @@
+#!/bin/bash
+
+exec compile-test-start-delayed coqdep-delay coqdep "$*"
diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el
index 2685d9ae..740b04c1 100644
--- a/ci/compile-tests/cct-lib.el
+++ b/ci/compile-tests/cct-lib.el
@@ -35,6 +35,9 @@
 (require 'ert)
 
 
+(defvar cct--debug-tests nil
+  "Set to t to get more output during test runs.")
+
 (defmacro cct-implies (p q)
   "Short-circuit logical implication.
 Evaluate Q only if P is non-nil."
@@ -61,7 +64,9 @@ Evaluate Q only if P is non-nil."
 Very similar to `goto-line', but the documentation of `goto-line'
 says, programs should use this piece of code."
   (goto-char (point-min))
-  (forward-line (1- line)))
+  (forward-line (1- line))
+  (cl-assert (eq (line-number-at-pos) line) nil
+             "point not at required line in cct-goto-line"))
 
 (defun cct-library-vo-of-v-file (v-src-file)
   "Return .vo file name for V-SRC-FILE.
@@ -82,20 +87,31 @@ cannot be accessed."
 
 (defun cct-split-change-times (file-change-times files)
   "Split assoc list FILE-CHANGE-TIMES.
-FILE-CHANGE-TIMES must be an assoc list and FILES must be a
-subset (i.e., each key occurring at most once) of the keys of
-FILE-CHANGE-TIMES as list. This function returns two associations
-lists (as cons cell). The car contains those associations in
-FILE-CHANGE-TIMES with keys not in FILES, the cdr contains those
-with keys in FILES."
+FILE-CHANGE-TIMES must be an assoc list and FILES must be a list
+of some of the keys of FILE-CHANGE-TIMES. This function returns
+two associations lists (as cons cell). The car contains those
+associations in FILE-CHANGE-TIMES with keys not in FILES, the cdr
+contains those with keys in FILES."
   (let (out in)
     (dolist (file-time file-change-times (cons out in))
       (if (member (car file-time) files)
           (push file-time in)
         (push file-time out)))))
 
+(defun cct-replace-last-word (line word)
+  "Replace last word in line LINE with WORD.
+In current buffer, go to the end of line LINE and one word
+backward. Replace the word there with WORD."
+  (cct-goto-line line)
+  (end-of-line)
+  (backward-word)
+  (kill-word 1)
+  (insert word))
+
 (defun cct-process-to-line (line)
   "Assert/retract to line LINE and wait until processing completed."
+  (when cct--debug-tests
+    (message "assert/retrect to line %d in buffer %s" line (buffer-name)))
   (cct-goto-line line)
   (proof-goto-point)
 
@@ -140,12 +156,18 @@ LOCKED-STATE must be 'locked or 'unlocked. This function checks
 whether line LINE is inside or outside the asserted (locked)
 region of the buffer and signals a test failure if not."
   (let ((locked (eq locked-state 'locked)))
-    ;; (message "tcl line %d check %s: %s %s\n"
-    ;;          line (if locked "locked" "unlocked")
-    ;;          proof-locked-span
-    ;;          (if (overlayp proof-locked-span)
-    ;;              (span-end proof-locked-span)
-    ;;            "no-span"))
+    (when cct--debug-tests
+      (message (concat "check lock state in buffer %s: line %d should be %s;\n"
+                       "\tlocked-span: %s ends at char %s in line %d")
+               (buffer-name)
+               line (if locked "locked" "unlocked")
+               proof-locked-span
+               (if (overlayp proof-locked-span)
+                   (span-end proof-locked-span)
+                 "<no-span>")
+               (if (overlayp proof-locked-span)
+                   (line-number-at-pos (span-end proof-locked-span))
+                 "<no-span>")))
     (cl-assert (or locked (eq locked-state 'unlocked))
                nil "test-check-locked 2nd argument wrong")
     (cct-goto-line line)
@@ -177,10 +199,11 @@ documentation of coq/coq-par-compile.el."
 Used to check that FILE has not been changed since TIME was
 recorded before."
   (let ((file-time (nth 5 (file-attributes file))))
-    ;; (message "TFU on %s: rec: %s now: %s\n"
-    ;;          file
-    ;;          (format-time-string "%H:%M:%S.%3N" time)
-    ;;          (format-time-string "%H:%M:%S.%3N" file-time))
+    (when cct--debug-tests
+      (message "file %s should be unchanged, recorded time: %s now: %s\n"
+               file
+               (format-time-string "%H:%M:%S.%3N" time)
+               (format-time-string "%H:%M:%S.%3N" file-time)))
     (should
      (and file-time (equal time file-time)))))
 
@@ -192,6 +215,12 @@ times as returned by `cct-record-change-times' or
 modification time of files in FILE-TIME-ASSOC equals the time
 recorded in FILE-TIME-ASSOC, i.e., that the file has not been
 changed since FILE-TIME-ASSOC has been recorded."
+  (when cct--debug-tests
+    (message "Files should be unchanged: %s"
+             (mapconcat
+              (lambda (file-time) (car file-time))
+              file-time-assoc
+              ", ")))
   (mapc
    (lambda (file-time-cons)
      (cct-file-unchanged (car file-time-cons) (cdr file-time-cons)))
@@ -215,6 +244,54 @@ or changed since recording the time in the association."
      (cct-file-newer (car file-time-cons) (cdr file-time-cons)))
    file-time-assoc))
 
+(defun cct-generic-check-main-buffer
+    (main-buf main-unlocked main-locked main-sum-line new-sum
+              vo-times recompiled-files require-ancestors
+              other-locked-files other-locked-line)
+  "Perform various checks for recompilation in MAIN-BUF.
+MAIN-BUF is a buffer, MAIN-LOCKED and MAIN-SUM-line are line
+numbers in that buffer. NEW-SUM is a number as string. VO-TIMES
+is an association list of files and emacs times as returned by
+`cct-record-change-times' or `cct-split-change-times'.
+RECOMPILED-FILES is a list of some of the files in VO-TIMES.
+REQUIRE-ANCESTORS is a list of cons cells, each cons containing a
+line number in MAIN-BUF (which should contain a require) and a
+list of ancestor files that should get registered in the span of
+that require. OTHER-LOCKED-FILES is a list of buffers and
+OTHER-LOCKED-LINE is a common line number in those files.
+
+This function combines all the following tests in this order:
+- line MAIN-UNLOCKED in MAIN-BUF is unlocked
+- after replacing the sum on line MAIN-SUM-LINE with NEW-SUM,
+  MAIN-BUF can be processed until line MAIN-LOCKED
+- files in VO-TIMES not listed in RECOMPILED-FILES have the same
+  last change time as in VO-TIMES
+- files in RECOMPILED-FILES have a newer change time
+- the spans in lines in REQUIRE-ANCESTORS have precisely the
+  ancestors registered as specified in REQUIRE-ANCESTORS.
+- all the buffers in OTHER-LOCKED-FILES are locked until line
+  OTHER-LOCKED-LINE."
+  (let (splitted)
+    (set-buffer main-buf)
+    (cct-check-locked main-unlocked 'unlocked)
+    (cct-replace-last-word main-sum-line new-sum)
+    (cct-process-to-line (1+ main-locked))
+    (cct-check-locked main-locked 'locked)
+    (setq splitted (cct-split-change-times vo-times recompiled-files))
+    ;; (message "check file dates, unmodified %s, modified %s"
+    ;;          (car splitted) (cdr splitted))
+    (cct-unmodified-change-times (car splitted))
+    (cct-older-change-times (cdr splitted))
+    (mapc
+     (lambda (line-ancestors)
+       (cct-locked-ancestors (car line-ancestors) (cdr line-ancestors)))
+     require-ancestors)
+    (mapc
+     (lambda (b)
+       (set-buffer b)
+       (cct-check-locked other-locked-line 'locked))
+     other-locked-files)))
+
 (defun cct-configure-proof-general ()
   "Configure Proof General for test execution."
   (setq delete-old-versions t
@@ -232,4 +309,20 @@ or changed since recording the time in the association."
            coq-max-background-compilation-jobs
            coq--internal-max-jobs))
 
+(defun configure-delayed-coq ()
+  "Configure PG to honor artificial delays in background compilation.
+Configure Proof General to use coqdep-delayed and coqc-delayed
+from directory ../bin. These scripts delay the start of the real
+coqdep and coqc as specified in the Coq soure file, see
+../bin/compile-test-start-delayed.
+
+This function uses relative file names and must be called in a
+test subdirectory parallel to the bin directory."
+  (let ((bin-dir (file-truename "../bin")))
+    (add-to-list 'exec-path bin-dir)
+    (setenv "PATH" (concat bin-dir ":" (getenv "PATH")))
+    (custom-set-variables
+     '(coq-dependency-analyzer "coqdep-delayed")
+     '(coq-compiler "coqc-delayed"))))
+
 (provide 'cct-lib)