add test for recompilation with changes

14 files changed, 536 insertions, 5 deletions

diff --git a/ci/compile-tests/005-change-recompile/Makefile b/ci/compile-tests/005-change-recompile/Makefile
new file mode 100644
index 00000000..983227be
--- /dev/null
+++ b/ci/compile-tests/005-change-recompile/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
+
+.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/005-change-recompile/a.v.orig b/ci/compile-tests/005-change-recompile/a.v.orig
new file mode 100644
index 00000000..f3d28e82
--- /dev/null
+++ b/ci/compile-tests/005-change-recompile/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 := 35.
+
+
+(* This is line 31 *)
+Lemma x : b + c + d + e + f + g + h = sum.
+Proof using.
+  unfold b, c, d, e, f, g, h, sum in *.
+  simpl.
+  trivial.
+Qed.
+(* This is line 38 *)
diff --git a/ci/compile-tests/005-change-recompile/b.v.orig b/ci/compile-tests/005-change-recompile/b.v.orig
new file mode 100644
index 00000000..0354f635
--- /dev/null
+++ b/ci/compile-tests/005-change-recompile/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/005-change-recompile/c.v.orig b/ci/compile-tests/005-change-recompile/c.v.orig
new file mode 100644
index 00000000..0dd52b4b
--- /dev/null
+++ b/ci/compile-tests/005-change-recompile/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 e f.
+
+(* This is line 22 *)
+Definition c : nat := 3.
diff --git a/ci/compile-tests/005-change-recompile/d.v.orig b/ci/compile-tests/005-change-recompile/d.v.orig
new file mode 100644
index 00000000..8c984eb3
--- /dev/null
+++ b/ci/compile-tests/005-change-recompile/d.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 g h.
+
+(* This is line 22 *)
+Definition d : nat := 4.
diff --git a/ci/compile-tests/005-change-recompile/e.v.orig b/ci/compile-tests/005-change-recompile/e.v.orig
new file mode 100644
index 00000000..dcef3a6e
--- /dev/null
+++ b/ci/compile-tests/005-change-recompile/e.v.orig
@@ -0,0 +1,17 @@
+(* 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.
+
+Definition e : nat := 5.
diff --git a/ci/compile-tests/005-change-recompile/f.v.orig b/ci/compile-tests/005-change-recompile/f.v.orig
new file mode 100644
index 00000000..ef17405a
--- /dev/null
+++ b/ci/compile-tests/005-change-recompile/f.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 h.
+
+(* This is line 22 *)
+Definition f : nat := 6.
diff --git a/ci/compile-tests/005-change-recompile/g.v.orig b/ci/compile-tests/005-change-recompile/g.v.orig
new file mode 100644
index 00000000..fbc58fed
--- /dev/null
+++ b/ci/compile-tests/005-change-recompile/g.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 g : nat := 7.
diff --git a/ci/compile-tests/005-change-recompile/h.v.orig b/ci/compile-tests/005-change-recompile/h.v.orig
new file mode 100644
index 00000000..1a0f57f7
--- /dev/null
+++ b/ci/compile-tests/005-change-recompile/h.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 h : nat := 8.
diff --git a/ci/compile-tests/005-change-recompile/test.el b/ci/compile-tests/005-change-recompile/test.el
new file mode 100644
index 00000000..4bbc4f81
--- /dev/null
+++ b/ci/compile-tests/005-change-recompile/test.el
@@ -0,0 +1,218 @@
+;; 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 that the right files are recompiled when changes are made in
+;; the dependency hierarchy and that unaffected ancestors are not
+;; touched.
+;;
+;; The following graph shows the file dependencies in this test:
+;;
+;;           a
+;;          / \
+;;         b   c
+;;        /   / \
+;;       d   e   f
+;;      / \  |  /
+;;     |   \ | /
+;;     |    \|/
+;;     g     h
+;;
+;;
+;;
+;;
+;;
+;;
+;;
+
+;;; set configuration
+(cct-configure-proof-general)
+
+;;; Data and utility functions
+
+(defconst b-ancestors '("./b.v" "./d.v" "./g.v" "./h.v")
+  "Ancestors of b.v.")
+
+(defconst c-ancestors '("./c.v" "./e.v" "./f.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 after changes and deletion."
+  (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 "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")
+    (find-file "c.v")
+    (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)
+
+    ;; 4. change h and process again - everything except g should get compiled
+    (message (concat "\n4. change h and process again - "
+                         "everything except g should get compiled\n"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (find-file "h.v")
+    (push "h.v" other-locked-files)
+    (cct-check-locked 21 'locked)
+    (cct-replace-last-word 21 "10")
+    (cct-check-main-buffer
+     vo-times "38" '("./b.vo" "./c.vo" "./d.vo" "./e.vo" "./f.vo" "./h.vo")
+     other-locked-files)
+    
+    ;; 5. change d and f and process again -
+    ;; only b, c, d and f should get recompiled
+    (message (concat "\n5. change d and f and process again - "
+                         "only b, c, d and f should get recompiled"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (find-file "d.v")
+    (push "d.v" other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 23 "7")
+    (find-file "f.v")
+    (push "f.v" other-locked-files)
+    (cct-check-locked 23 'unlocked)
+    (cct-replace-last-word 23 "10")
+
+    (cct-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
+    (message (concat "\n6. change d and b and process again - "
+                         "only d and b should get compiled\n"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (find-file "b.v")
+    (push "b.v" other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 23 "7")
+    (set-buffer "d.v")
+    (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")
+                           other-locked-files)
+    
+    ;; 7. delete b and process again - only b should get compiled
+    (message (concat "\n7. delete b and process again - "
+                         "only b should get compiled\n"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (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)
+    
+    ;; 8. delete h and process again - everything except g should get compiled
+    (message (concat "\n8. delete h and process again - "
+                         "everything except g should get compiled\n"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (delete-file "h.vo")
+    (set-buffer "a.v")
+    (cct-process-to-line 21)
+    (cct-check-main-buffer
+     vo-times "56" '("./b.vo" "./c.vo" "./d.vo" "./e.vo" "./f.vo" "./h.vo")
+     other-locked-files)
+    
+    ;; 9. change d, delete g and process again - only b, d and g should
+    ;; get compiled
+    (message (concat "\n9. change d, delete g and process again - "
+                         "only b, d and g should get compiled\n"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (set-buffer "d.v")
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 23 "20")     ; increase by 7
+    (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")
+                           other-locked-files)
+    
+    ;; 10. delete d, change g and process again - only b, d and g should
+    ;; get compiled
+    (message (concat "\n10. delete d, change g and process again - "
+                         "only b, d and g should get compiled\n"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (delete-file "d.vo")
+    (find-file "g.v")
+    (push "g.v" other-locked-files)
+    (cct-check-locked 21 'locked)
+    (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")
+                           other-locked-files)
+  ))
diff --git a/ci/compile-tests/Makefile b/ci/compile-tests/Makefile
new file mode 100644
index 00000000..32f6561b
--- /dev/null
+++ b/ci/compile-tests/Makefile
@@ -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)
+
+
+TOPTARGETS := test clean
+
+SUBDIRS := $(wildcard [0-9][0-9][0-9]-*)
+
+$(TOPTARGETS): $(SUBDIRS)
+$(SUBDIRS):
+	$(MAKE) -C $@ $(MAKECMDGOALS)
+
+.PHONY: $(TOPTARGETS) $(SUBDIRS)
+
+.PHONY: TAGS
+TAGS:
+	etags *.el */*.el
diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el
index 42003d1c..532cd92a 100644
--- a/ci/compile-tests/cct-lib.el
+++ b/ci/compile-tests/cct-lib.el
@@ -29,6 +29,39 @@ says, programs should use this piece of code."
   (goto-char (point-min))
   (forward-line (1- line)))
 
+(defun cct-library-vo-of-v-file (v-src-file)
+  "Return .vo file name for V-SRC-FILE.
+Changes the suffix from .v to .vo.  V-SRC-FILE must have a .v suffix."
+  (concat v-src-file "o"))
+
+(defun cct-record-change-time (file)
+  "Return cons of FILE and its modification time.
+The modification time is an emacs time value, it's nil if file
+cannot be accessed."
+  (cons file (nth 5 (file-attributes file))))
+
+(defun cct-record-change-times (files)
+  "Return an assoc list of FILES with their modification times.
+The modification time is an emacs time value, it's nil if file
+cannot be accessed."
+  (mapcar 'cct-record-change-time files))
+
+(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 occoring 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."
+  (seq-reduce
+   (lambda (acc file)
+     (push (assoc file (car acc)) (cdr acc))
+     (setcar acc (assoc-delete-all file (car acc)))
+     acc)
+   files
+   (cons (copy-alist file-change-times) nil)))
+
 (defun cct-process-to-line (line)
   "Assert/retract to line LINE and wait until processing completed."
   (cct-goto-line line)
@@ -108,11 +141,49 @@ documentation of coq/coq-par-compile.el."
     (should
      (seq-set-equal-p locked-ancestors ancestors))))
 
+(defun cct-file-unchanged (file time)
+  "Check that modification time of FILE equals TIME.
+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))
+    (should
+     (and file-time (equal time file-time)))))
+
+(defun cct-unmodified-change-times (file-time-assoc)
+  "Check that files in FILE-TIME-ASSOC have not been changed.
+FILE-TIME-ASSOC must be an association list of files and emacs
+times as returned by `cct-record-change-times' or
+`cct-split-change-times'. This function checks that the
+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."
+  (mapc
+   (lambda (file-time-cons)
+     (cct-file-unchanged (car file-time-cons) (cdr file-time-cons)))
+   file-time-assoc))
+
 (defun cct-file-newer (file time)
   "Check that FILE exists and its modification time is more recent than TIME."
   (let ((file-time (nth 5 (file-attributes file))))
     (should (and file-time (time-less-p time file-time)))))
 
+(defun cct-older-change-times (file-time-assoc)
+  "Check that files exist and have been changed.
+FILE-TIME-ASSOC must be an association list of files and emacs
+times as returned by `cct-record-change-times' or
+`cct-split-change-times'. This function checks that the files in
+FILE-TIME-ASSOC do exist and that their modification time is more
+recent than in the association list, i.e., they have been updated
+or changed since recording the time in the association."
+  (mapc
+   (lambda (file-time-cons)
+     (cct-file-newer (car file-time-cons) (cdr file-time-cons)))
+   file-time-assoc))
+
 (defun cct-configure-proof-general ()
   "Configure Proof General for test execution."
   (setq delete-old-versions t
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index ed927409..3e3b7023 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -600,8 +600,8 @@ Changes the suffix from .vo to .vio.  VO-OBJ-FILE must have a .vo suffix."
   (concat (coq-library-src-of-vo-file vo-obj-file) "io"))
 
 (defun coq-library-vos-of-vo-file (vo-obj-file)
-  "Return .vok file name for VO-OBJ-FILE.
-Changes the suffix from .vo to .vok.  VO-OBJ-FILE must have a .vo suffix."
+  "Return .vos file name for VO-OBJ-FILE.
+Changes the suffix from .vo to .vos.  VO-OBJ-FILE must have a .vo suffix."
   (concat vo-obj-file "s"))
 
 
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index a914ec74..7710a029 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -25,18 +25,19 @@
 ;;
 ;; - fix -I current-dir argument for coqc invocations
 ;; - on error, try to put location info into the error message
+;; - use file-attribute-modification-time and similar functions when
+;;   dropping support for emacs 25 (emacs 26.1 released on 05/2018)
+;; - use define-error when dropping support for emacs 24 (25.1
+;;   released on 09/2016)
 ;;
 ;; Note that all argument computations inherit `coq-autodetected-version': when
 ;; changing compilers, all compilation jobs must be terminated.  This is
 ;; consistent with the fact that the _CoqProject file is not reparsed.
 ;;
 ;; tests wanted:
-;; - a require command with no dependencies or all deps ignored
 ;; - unlock checks for ancestors of failed jobs in different cases
 ;; - two require jobs, where the first finishes, while the second is
 ;;   in a state before waiting-dep
-;; - a coqdep error on a require command
-;; - some dependency cycles
 ;; - a job depending on a failed dependee, where the dependee has been finished before
 
 ;;; Code:
@@ -664,6 +665,7 @@ in a cycle."
         ;; XXX when clause does not make sense: job is a dependee or
         ;; dependency of (car p), therefore (car p) can only be in
         ;; state 'waiting-dep
+        ;; XXX only recurse for dependants not visited yet
 	(when (eq (get (car p) 'state) 'waiting-dep)
           ;; XXX should not be called on visited ancestors?
 	  (setq cycle (coq-par-find-dependency-circle-for-job (car p) path)))