13 files changed, 368 insertions, 0 deletions
diff --git a/ci/compile-tests/006-ready-dependee/Makefile b/ci/compile-tests/006-ready-dependee/Makefile
new file mode 100644
index 00000000..fe014bfc
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/Makefile
@@ -0,0 +1,28 @@
+# This file is part of Proof General.
+# 
+# © Copyright 2020  Hendrik Tews
+# 
+# Authors: Hendrik Tews
+# Maintainer: Hendrik Tews <hendrik@askra.de>
+# 
+# License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+
+# This 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:=a.v b.v c.v d.v e.v f.v g.v h.v i.v j.v k.v
+
+.PHONY: test
+test:
+	$(MAKE) clean
+	$(MAKE) $(TEST_SOURCES)
+	emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \
+		-l test.el -f ert-run-tests-batch-and-exit
+
+%.v: %.v.orig
+	cp $< $@
+
+.PHONY: clean
+clean:
+	rm -f *.vo *.glob *.vio *.vos *.vok .*.aux $(TEST_SOURCES)
diff --git a/ci/compile-tests/006-ready-dependee/a.v.orig b/ci/compile-tests/006-ready-dependee/a.v.orig
new file mode 100644
index 00000000..8e4300e8
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/a.v.orig
@@ -0,0 +1,38 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+
+
+(* This is line 21 *)
+Require Export b.
+Require Export c.
+(* This is line 24 *)
+
+
+(* This is line 27 *)
+Definition sum : nat := 9.
+
+
+(* This is line 31 *)
+Lemma x : b + c + k = sum.
+Proof using.
+  unfold b, c, k, sum in *.
+  simpl.
+  trivial.
+Qed.
+(* This is line 38 *)
diff --git a/ci/compile-tests/006-ready-dependee/b.v.orig b/ci/compile-tests/006-ready-dependee/b.v.orig
new file mode 100644
index 00000000..0354f635
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/b.v.orig
@@ -0,0 +1,23 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+
+Require Export d.
+
+(* This is line 22 *)
+Definition b : nat := 2.
diff --git a/ci/compile-tests/006-ready-dependee/c.v.orig b/ci/compile-tests/006-ready-dependee/c.v.orig
new file mode 100644
index 00000000..3d2e542c
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/c.v.orig
@@ -0,0 +1,23 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+
+Require Export k.
+
+(* This is line 22 *)
+Definition c : nat := 3.
diff --git a/ci/compile-tests/006-ready-dependee/d.v.orig b/ci/compile-tests/006-ready-dependee/d.v.orig
new file mode 100644
index 00000000..2f9825cb
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/d.v.orig
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Require Export e.
diff --git a/ci/compile-tests/006-ready-dependee/e.v.orig b/ci/compile-tests/006-ready-dependee/e.v.orig
new file mode 100644
index 00000000..0589d31b
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/e.v.orig
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Require Export f.
diff --git a/ci/compile-tests/006-ready-dependee/f.v.orig b/ci/compile-tests/006-ready-dependee/f.v.orig
new file mode 100644
index 00000000..32c9287b
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/f.v.orig
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Require Export g.
diff --git a/ci/compile-tests/006-ready-dependee/g.v.orig b/ci/compile-tests/006-ready-dependee/g.v.orig
new file mode 100644
index 00000000..73b210c1
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/g.v.orig
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Require Export h.
diff --git a/ci/compile-tests/006-ready-dependee/h.v.orig b/ci/compile-tests/006-ready-dependee/h.v.orig
new file mode 100644
index 00000000..5db2c3ca
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/h.v.orig
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Require Export i.
diff --git a/ci/compile-tests/006-ready-dependee/i.v.orig b/ci/compile-tests/006-ready-dependee/i.v.orig
new file mode 100644
index 00000000..09135c38
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/i.v.orig
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Require Export j.
diff --git a/ci/compile-tests/006-ready-dependee/j.v.orig b/ci/compile-tests/006-ready-dependee/j.v.orig
new file mode 100644
index 00000000..62702b4f
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/j.v.orig
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Require Export k.
diff --git a/ci/compile-tests/006-ready-dependee/k.v.orig b/ci/compile-tests/006-ready-dependee/k.v.orig
new file mode 100644
index 00000000..7405e2c9
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/k.v.orig
@@ -0,0 +1,21 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2020  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+
+(* This is line 20 *)
+Definition k : nat := 4.
diff --git a/ci/compile-tests/006-ready-dependee/test.el b/ci/compile-tests/006-ready-dependee/test.el
new file mode 100644
index 00000000..280c008a
--- /dev/null
+++ b/ci/compile-tests/006-ready-dependee/test.el
@@ -0,0 +1,130 @@
+;; This file is part of Proof General.
+;;
+;; © Copyright 2020  Hendrik Tews
+;;
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hendrik@askra.de>
+;;
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
+;; Coq Compile Tests (cct) --
+;; ert tests for parallel background compilation for Coq
+;;
+;; Test recompilation and ancestor registration for the case a
+;; dependency is in state ready already.
+;;
+;; The following graph shows the file dependencies in this test:
+;;
+;;           a
+;;          / \
+;;         b   c
+;;         |   |____________
+;;         d                \
+;;         |                 |
+;;         e--f--g--h--i--j--k
+;;
+;; The idea is that the coqdep chain from b to j takes so long, that k
+;; has been compiled and is in state ready before the coqdep results
+;; from j are processed. This works - unless the disk cache is cold.
+;; If it works the test triggers two bugs. First, k is locked with the
+;; require command of c. Second, the modification time of k is not
+;; propagated to j, such that the whole chain from j to b is not
+;; recompiled after k has changed.
+
+
+;;; set configuration
+(cct-configure-proof-general)
+
+;;; Data and utility functions
+
+(defconst b-ancestors '("./b.v" "./d.v" "./e.v" "./f.v" "./g.v"
+                        "./h.v" "./i.v" "./j.v" "./k.v")
+  "Ancestors of b.v.")
+
+(defconst c-ancestors '("./c.v")
+  "Ancestors of c.v.")
+
+(defconst all-ancestors (append b-ancestors c-ancestors)
+  "All ancestors.")
+
+(defconst all-compiled-ancestors
+  (mapcar 'cct-library-vo-of-v-file all-ancestors)
+  "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
+                                       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)))
+
+
+;;; The test itself
+
+(ert-deftest cct-change-recompile ()
+  "Test successful recompilation for a dependency in state ready."
+  ;; :expected-result :failed
+  ;;(setq coq--debug-auto-compilation t)
+  (find-file "a.v")
+
+  ;; 1. process original content - compile everything
+  (message "\n1. process original content - compile everything\n")
+  (cct-process-to-line 38)
+  (cct-check-locked 37 'locked)
+  (cct-locked-ancestors 22 b-ancestors)
+  (cct-locked-ancestors 23 c-ancestors)
+
+  (let ((vo-times (cct-record-change-times all-compiled-ancestors))
+        other-locked-files)
+
+    ;; 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 "9" nil nil)
+
+    ;; 3. change k and process again - everything should be compiled
+    (message "\n3. change k and process again - everything should be compiled\n")
+    (find-file "k.v")
+    (push "k.v" other-locked-files)
+    (cct-check-locked 21 'locked)
+    (cct-replace-last-word 21 "5")
+    (cct-check-main-buffer
+     vo-times "10"
+     '("./b.vo" "./c.vo" "./d.vo" "./e.vo" "./f.vo" "./g.vo"
+       "./h.vo" "./i.vo" "./j.v" "./k.v")
+     other-locked-files)
+  ))