diff options
| -rw-r--r-- | ci/compile-tests/006-ready-dependee/test.el | 2 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 33 |
2 files changed, 23 insertions, 12 deletions
diff --git a/ci/compile-tests/006-ready-dependee/test.el b/ci/compile-tests/006-ready-dependee/test.el index 280c008a..7105c6e7 100644 --- a/ci/compile-tests/006-ready-dependee/test.el +++ b/ci/compile-tests/006-ready-dependee/test.el @@ -125,6 +125,6 @@ Combine all the following tests in this order: (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") + "./h.vo" "./i.vo" "./j.vo" "./k.vo") other-locked-files) )) diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 7710a029..c4e45af8 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -39,6 +39,9 @@ ;; - two require jobs, where the first finishes, while the second is ;; in a state before waiting-dep ;; - 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 every possible state +;; - coq-par-create-file-job finds a failed job ;;; Code: @@ -1577,18 +1580,24 @@ before." ;; ;; If this job has just been compiled then it is clearly ;; 'just-compiled. Otherwise it must be 'obj-mod-time, because - ;; if some ancestore were newer, this just would have been + ;; if some ancestor were newer, this just would have been ;; compiled. For failed jobs obj-mod-time might be nil, but ;; this does not matter. (dep-time (if just-compiled 'just-compiled (get job 'obj-mod-time)))) (put job 'youngest-coqc-dependency dep-time) (when coq--debug-auto-compilation - (message "%s: kickoff %d coqc dependencies with time %s" - (get job 'name) (length (get job 'coqc-dependants)) - (if (eq dep-time 'just-compiled) - 'just-compiled - (current-time-string dep-time)))) + (let (ancs) + ;; don't use map-apply here, this changes the timing too much + (maphash + (lambda (anc-job not-used) (push (get anc-job 'src-file) ancs)) + ancestor-hash) + (message "%s: kickoff %d coqc dependencies with time %s\n\tancestors %s" + (get job 'name) (length (get job 'coqc-dependants)) + (if (eq dep-time 'just-compiled) + 'just-compiled + (current-time-string dep-time)) + ancs))) ;; In the recursion coq-par-kickoff-coqc-dependants -> ;; coq-par-decrease-coqc-dependency -> coq-par-compile-job-maybe ;; -> coq-par-kickoff-coqc-dependants jobs on the path upwards @@ -1605,8 +1614,7 @@ before." (if dependant-alive "some" "no"))) (when (and (not dependant-alive) (not (get job 'failed))) - ;; job has not failed (see first assert), but all dependants - ;; have 'failed set + ;; job has not failed, but all dependants have 'failed set (coq-par-unlock-job-ancestors-on-error job)))) (defun coq-par-start-coqdep-on-require (job) @@ -1998,13 +2006,16 @@ is directly passed to `coq-par-analyse-coq-dep-exit'." (dep-time (get dep-job 'youngest-coqc-dependency))) (when (get dep-job 'failed) (setq dependee-failed t)) - ;; XXX what happens when dep-job failed? - (unless (eq (get dep-job 'state) 'ready) + (when (eq (get dep-job 'state) 'ready) + (merge-hash-content (get job 'ancestors) (get dep-job 'ancestors)) ;; the following clause is not needed for require jobs, ;; but it doesn't harm either, so keep the code a little ;; bit more simple (when (coq-par-time-less job-max-time dep-time) - (setq job-max-time dep-time)) + (setq job-max-time dep-time))) + ;; not adding the dependency link is fine now + ;; with a feature for background vo compilation, this link is needed + (unless (eq (get dep-job 'state) 'ready) (coq-par-add-coqc-dependency dep-job job))))) (put job 'youngest-coqc-dependency job-max-time) (when dependee-failed |