From 16e784a63f2a38ce3f03e36b6fa9a7db2da211b9 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sat, 5 Dec 2020 22:27:47 +0100 Subject: add test for recompilation with changes --- ci/compile-tests/005-change-recompile/Makefile | 28 ++++ ci/compile-tests/005-change-recompile/a.v.orig | 38 +++++ ci/compile-tests/005-change-recompile/b.v.orig | 23 +++ ci/compile-tests/005-change-recompile/c.v.orig | 23 +++ ci/compile-tests/005-change-recompile/d.v.orig | 23 +++ ci/compile-tests/005-change-recompile/e.v.orig | 17 ++ ci/compile-tests/005-change-recompile/f.v.orig | 23 +++ ci/compile-tests/005-change-recompile/g.v.orig | 21 +++ ci/compile-tests/005-change-recompile/h.v.orig | 21 +++ ci/compile-tests/005-change-recompile/test.el | 218 +++++++++++++++++++++++++ ci/compile-tests/Makefile | 23 +++ ci/compile-tests/cct-lib.el | 71 ++++++++ coq/coq-compile-common.el | 4 +- coq/coq-par-compile.el | 8 +- 14 files changed, 536 insertions(+), 5 deletions(-) create mode 100644 ci/compile-tests/005-change-recompile/Makefile create mode 100644 ci/compile-tests/005-change-recompile/a.v.orig create mode 100644 ci/compile-tests/005-change-recompile/b.v.orig create mode 100644 ci/compile-tests/005-change-recompile/c.v.orig create mode 100644 ci/compile-tests/005-change-recompile/d.v.orig create mode 100644 ci/compile-tests/005-change-recompile/e.v.orig create mode 100644 ci/compile-tests/005-change-recompile/f.v.orig create mode 100644 ci/compile-tests/005-change-recompile/g.v.orig create mode 100644 ci/compile-tests/005-change-recompile/h.v.orig create mode 100644 ci/compile-tests/005-change-recompile/test.el create mode 100644 ci/compile-tests/Makefile 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 +# +# 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 + * + * 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 + * + * 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 + * + * 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 + * + * 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 + * + * 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 + * + * 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 + * + * 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 + * + * 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 +;; +;; 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 +# +# 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))) -- cgit v1.2.3