diff options
| -rw-r--r-- | coq/coq-compile-common.el | 3 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 16 | ||||
| -rw-r--r-- | coq/coq-par-test.el | 907 |
3 files changed, 652 insertions, 274 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index a6b5abb3..1840f9a0 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -392,8 +392,7 @@ modules are matched separately with `coq-require-id-regexp'") A time value is a list of two integers as returned by `file-attributes'. The first integer contains the upper 16 bits and the second the lower 16 bits of the time." - (or (time-less-p time-1 time-2) - (equal time-1 time-2))) + (not (time-less-p time-2 time-1))) (defun coq-max-dep-mod-time (dep-mod-times) "Return the maximum in DEP-MOD-TIMES. diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 167c0869..d4ad2a7e 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -888,7 +888,7 @@ therefore delete a file if it might be in the way." (if vo-obj-time (time-less-p vo-obj-time src-time) "-") (if vio-obj-time (time-less-p vio-obj-time src-time) "-") (if vo-obj-time (coq-par-time-less vo-obj-time dep-time) "-") - (if vio-obj-time (coq-par-time-less-p vio-obj-time dep-time) "-"))) + (if vio-obj-time (coq-par-time-less vio-obj-time dep-time) "-"))) ;; Compute first the max of vo-obj-time and vio-obj-time and remember ;; which of both is newer. This is only meaningful if at least one of ;; the .vo or .vio file exists. @@ -906,8 +906,10 @@ therefore delete a file if it might be in the way." ;; Decide if and what to compile. (if (or (eq dep-time 'just-compiled) ; a dep has been just compiled (and (not vo-obj-time) (not vio-obj-time)) ; no obj exists - (time-less-p max-obj-time src-time) ; src is younger than any obj - (time-less-p max-obj-time dep-time)) ; dep is younger than any obj + ;; src younger than any obj? + (time-less-or-equal max-obj-time src-time) + ;; dep younger than any obj? + (time-less-or-equal max-obj-time dep-time)) ;; compilation is definitely needed (progn (setq result t) @@ -963,9 +965,9 @@ therefore delete a file if it might be in the way." (put job 'required-obj-file vio-file) (put job 'obj-mod-time vio-obj-time) (when (and vo-obj-time - (or (time-less-p vo-obj-time src-time) + (or (time-less-or-equal vo-obj-time src-time) ;; dep-time is neither nil nor 'just-compiled here - (time-less-p vo-obj-time dep-time))) + (time-less-or-equal vo-obj-time dep-time))) (setq file-to-delete vo-file)) (when coq-debug-auto-compilation (message "%s: vio up-to-date; delete %s" @@ -974,9 +976,9 @@ therefore delete a file if it might be in the way." (put job 'required-obj-file vo-file) (put job 'obj-mod-time vo-obj-time) (when (and vio-obj-time - (or (time-less-p vio-obj-time src-time) + (or (time-less-or-equal vio-obj-time src-time) ;; dep-time is neither nil nor 'just-compiled here - (time-less-p vio-obj-time dep-time))) + (time-less-or-equal vio-obj-time dep-time))) (setq file-to-delete vio-file)) (when coq-debug-auto-compilation (message "%s: vo up-to-date 2; delete %s" diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el index 9ebd775c..019ae62f 100644 --- a/coq/coq-par-test.el +++ b/coq/coq-par-test.el @@ -17,7 +17,6 @@ ;;; TODO: ;; ;; - integrate into PG build and test(?) system -;; - add tests for files with identical time stamps (require 'coq-par-compile) @@ -25,273 +24,673 @@ (defconst coq-par-job-needs-compilation-tests ;; for documentation see the doc string following the init value '( - ;; present files | compilation? | delete | 'req-obj-file | 'obj-mod-t + ;; present files | compilation? | delete | 'req-obj-file ;; ==================================================================== ;; all of src dep vo vio present ((src dep vo vio) - (no-quick nil nil vio vio) - (quick nil nil vio vio) - (ensure-vo nil vio vo vo)) + (no-quick nil nil vio) + (quick nil nil vio) + (ensure-vo nil vio vo )) ((src dep vio vo) - (no-quick nil nil vo vo ) - (quick nil nil vo vo ) - (ensure-vo nil vio vo vo )) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) ((src vo dep vio) - (no-quick nil vo vio vio ) - (quick nil vo vio vio ) - (ensure-vo t vio vo nil )) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t vio vo )) ((src vo vio dep) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) ((src vio dep vo) - (no-quick nil vio vo vo ) - (quick nil vio vo vo ) - (ensure-vo nil vio vo vo )) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) ((src vio vo dep) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) - ;; present files | compilation? | delete | 'req-obj-file | 'obj-mod-t + ;; present files | compilation? | delete | 'req-obj-file ((dep src vio vo) - (no-quick nil nil vo vo ) - (quick nil nil vo vo ) - (ensure-vo nil vio vo vo )) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) ((dep src vo vio) - (no-quick nil nil vio vio ) - (quick nil nil vio vio ) - (ensure-vo nil vio vo vo )) + (no-quick nil nil vio) + (quick nil nil vio) + (ensure-vo nil vio vo )) ((dep vo vio src) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) ((dep vo src vio) - (no-quick nil vo vio vio ) - (quick nil vo vio vio ) - (ensure-vo t vio vo nil )) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t vio vo )) ((dep vio vo src) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) ((dep vio src vo) - (no-quick nil vio vo vo ) - (quick nil vio vo vo ) - (ensure-vo nil vio vo vo )) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) ((vo src dep vio) - (no-quick nil vo vio vio ) - (quick nil vo vio vio ) - (ensure-vo t vio vo nil )) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t vio vo )) - ;; present files | compilation? | delete | 'req-obj-file | 'obj-mod-t + ;; present files | compilation? | delete | 'req-obj-file ((vo src vio dep) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) ((vo dep src vio) - (no-quick nil vo vio vio ) - (quick nil vo vio vio ) - (ensure-vo t vio vo nil )) + (no-quick nil vo vio ) + (quick nil vo vio ) + (ensure-vo t vio vo )) ((vo dep vio src) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) ((vo vio src dep) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) ((vo vio dep src) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) ((vio src vo dep) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) ((vio src dep vo) - (no-quick nil vio vo vo ) - (quick nil vio vo vo ) - (ensure-vo nil vio vo vo )) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) ((vio dep vo src) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) - ;; present files | compilation? | delete | 'req-obj-file | 'obj-mod-t + ;; present files | compilation? | delete | 'req-obj-file ((vio dep src vo) - (no-quick nil vio vo vo ) - (quick nil vio vo vo ) - (ensure-vo nil vio vo vo )) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) ((vio vo dep src) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) ((vio vo src dep) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) ;; only src dep vo present ((src dep vo) - (no-quick nil nil vo vo ) - (quick nil nil vo vo ) - (ensure-vo nil nil vo vo )) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil nil vo )) ((src vo dep) - (no-quick t nil vo nil ) - (quick t vo vio nil ) - (ensure-vo t nil vo nil )) + (no-quick t nil vo ) + (quick t vo vio ) + (ensure-vo t nil vo )) ((dep src vo) - (no-quick nil nil vo vo ) - (quick nil nil vo vo ) - (ensure-vo nil nil vo vo )) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil nil vo )) ((dep vo src) - (no-quick t nil vo nil ) - (quick t vo vio nil ) - (ensure-vo t nil vo nil )) + (no-quick t nil vo ) + (quick t vo vio ) + (ensure-vo t nil vo )) ((vo src dep) - (no-quick t nil vo nil ) - (quick t vo vio nil ) - (ensure-vo t nil vo nil )) + (no-quick t nil vo ) + (quick t vo vio ) + (ensure-vo t nil vo )) ((vo dep src) - (no-quick t nil vo nil ) - (quick t vo vio nil ) - (ensure-vo t nil vo nil )) + (no-quick t nil vo ) + (quick t vo vio ) + (ensure-vo t nil vo )) - ;; present files | compilation? | delete | 'req-obj-file | 'obj-mod-t + ;; present files | compilation? | delete | 'req-obj-file ;; only src dep vio present ((src dep vio) - (no-quick nil nil vio vio ) - (quick nil nil vio vio ) - (ensure-vo t vio vo nil )) + (no-quick nil nil vio ) + (quick nil nil vio ) + (ensure-vo t vio vo )) ((src vio dep) - (no-quick t vio vo nil ) - (quick t nil vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t nil vio ) + (ensure-vo t vio vo )) ((dep src vio) - (no-quick nil nil vio vio ) - (quick nil nil vio vio ) - (ensure-vo t vio vo nil )) + (no-quick nil nil vio ) + (quick nil nil vio ) + (ensure-vo t vio vo )) ((dep vio src) - (no-quick t vio vo nil ) - (quick t nil vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t nil vio ) + (ensure-vo t vio vo )) ((vio src dep) - (no-quick t vio vo nil ) - (quick t nil vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t nil vio ) + (ensure-vo t vio vo )) ((vio dep src) - (no-quick t vio vo nil ) - (quick t nil vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t nil vio ) + (ensure-vo t vio vo )) - ;; present files | compilation? | delete | 'req-obj-file | 'obj-mod-t + ;; present files | compilation? | delete | 'req-obj-file ;; only src vo vio present ((src vo vio) - (no-quick nil nil vio vio ) - (quick nil nil vio vio ) - (ensure-vo nil vio vo vo )) + (no-quick nil nil vio ) + (quick nil nil vio ) + (ensure-vo nil vio vo )) ((src vio vo) - (no-quick nil nil vo vo ) - (quick nil nil vo vo ) - (ensure-vo nil vio vo vo )) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) ((vo src vio) - (no-quick nil vo vio vio ) - (quick nil vo vio vio ) - (ensure-vo t vio vo nil )) + (no-quick nil vo vio ) + (quick nil vo vio ) + (ensure-vo t vio vo )) ((vo vio src) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) ((vio src vo) - (no-quick nil vio vo vo ) - (quick nil vio vo vo ) - (ensure-vo nil vio vo vo )) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) ((vio vo src) - (no-quick t vio vo nil ) - (quick t vo vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) - ;; present files | compilation? | delete | 'req-obj-file | 'obj-mod-t + ;; present files | compilation? | delete | 'req-obj-file ;; only src dep present ((src dep) - (no-quick t nil vo nil ) - (quick t nil vio nil ) - (ensure-vo t nil vo nil )) + (no-quick t nil vo ) + (quick t nil vio ) + (ensure-vo t nil vo )) ((dep src) - (no-quick t nil vo nil ) - (quick t nil vio nil ) - (ensure-vo t nil vo nil )) + (no-quick t nil vo ) + (quick t nil vio ) + (ensure-vo t nil vo )) ;; only src vo present ((src vo) - (no-quick nil nil vo vo ) - (quick nil nil vo vo ) - (ensure-vo nil nil vo vo )) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil nil vo )) ((vo src) - (no-quick t nil vo nil ) - (quick t vo vio nil ) - (ensure-vo t nil vo nil )) + (no-quick t nil vo ) + (quick t vo vio ) + (ensure-vo t nil vo )) ;; only src vio present ((src vio) - (no-quick nil nil vio vio ) - (quick nil nil vio vio ) - (ensure-vo t vio vo nil )) + (no-quick nil nil vio ) + (quick nil nil vio ) + (ensure-vo t vio vo )) ((vio src) - (no-quick t vio vo nil ) - (quick t nil vio nil ) - (ensure-vo t vio vo nil )) + (no-quick t vio vo ) + (quick t nil vio ) + (ensure-vo t vio vo )) ;; only src present ((src) - (no-quick t nil vo nil ) - (quick t nil vio nil ) - (ensure-vo t nil vo nil )) + (no-quick t nil vo ) + (quick t nil vio ) + (ensure-vo t nil vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ;; + ;; test cases for some objects with identical time stamp + ;; + ;; 4 files with same time stamp + (((src vo dep vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; 3 files with same time stamp + (((src vo dep) vio) + (no-quick nil vo vio ) + (quick nil vo vio ) + (ensure-vo t vio vo )) + + ((vio (src vo dep)) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + (((src vo vio) dep) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + ((dep (src vo vio)) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + (((src dep vio) vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((vo (src dep vio)) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + (((vo dep vio) src) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + ((src (vo dep vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; 2 times 2 files with same time stamp + (((src vo) (dep vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((dep vio) (src vo)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((src dep) (vo vio)) + ;; could also use the vio as 'req-obj-file in the first 2 cases here + (no-quick nil nil vo) + (quick nil nil vo) + (ensure-vo nil vio vo )) + + (((vo vio) (src dep)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((src vio) (vo dep)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + (((vo dep) (src vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; 2 files with same time stamp + (((src vo) dep vio) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t vio vo )) + + (((src vo) vio dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((dep (src vo) vio) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t vio vo )) + + ((dep vio (src vo)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vio (src vo) dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vio dep (src vo)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + (((src dep) vo vio) + (no-quick nil nil vio) + (quick nil nil vio) + (ensure-vo nil vio vo )) + + (((src dep) vio vo) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) + + ((vo (src dep) vio) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t vio vo )) + + ((vo vio (src dep)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vio (src dep) vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((vio vo (src dep)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((src vio) vo dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((src vio) dep vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((vo (src vio) dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((vo dep (src vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((dep (src vio) vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((dep vo (src vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((vo dep) src vio) + (no-quick nil vo vio ) + (quick nil vo vio ) + (ensure-vo t vio vo )) + + (((vo dep) vio src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((src (vo dep) vio) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t vio vo )) + + ((src vio (vo dep)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vio (vo dep) src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vio src (vo dep)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + (((vo vio) src dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((vo vio) dep src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((src (vo vio) dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((src dep (vo vio)) + ;; could also use the vio as 'req-obj-file in the first 2 cases here + (no-quick nil nil vo) + (quick nil nil vo) + (ensure-vo nil vio vo )) + + ((dep (vo vio) src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((dep src (vo vio)) + ;; could also use the vio as 'req-obj-file in the first 2 cases here + (no-quick nil nil vo) + (quick nil nil vo) + (ensure-vo nil vio vo )) + + (((dep vio) src vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + (((dep vio) vo src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((src (dep vio) vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((src vo (dep vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vo (dep vio) src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vo src (dep vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; 2 files with the same time stamp out of 3 files + ;; without vio + (((src dep vo)) + (no-quick t nil vo ) + (quick t vo vio) + (ensure-vo t nil vo )) + + (((src dep) vo) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil nil vo )) + + ((vo (src dep)) + (no-quick t nil vo ) + (quick t vo vio) + (ensure-vo t nil vo )) + + (((src vo) dep) + (no-quick t nil vo ) + (quick t vo vio) + (ensure-vo t nil vo )) + + ((dep (src vo)) + (no-quick t nil vo ) + (quick t vo vio) + (ensure-vo t nil vo )) + + (((dep vo) src) + (no-quick t nil vo ) + (quick t vo vio) + (ensure-vo t nil vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((src (dep vo)) + (no-quick t nil vo ) + (quick t vo vio) + (ensure-vo t nil vo )) + + ;; without vo + (((src dep vio)) + (no-quick t vio vo ) + (quick t nil vio) + (ensure-vo t vio vo )) + + (((src dep) vio) + (no-quick nil nil vio ) + (quick nil nil vio ) + (ensure-vo t vio vo )) + + ((vio (src dep)) + (no-quick t vio vo ) + (quick t nil vio) + (ensure-vo t vio vo )) + + (((src vio) dep) + (no-quick t vio vo ) + (quick t nil vio) + (ensure-vo t vio vo )) + + ((dep (src vio)) + (no-quick t vio vo ) + (quick t nil vio) + (ensure-vo t vio vo )) + + (((dep vio) src) + (no-quick t vio vo ) + (quick t nil vio) + (ensure-vo t vio vo )) + + ((src (dep vio)) + (no-quick t vio vo ) + (quick t nil vio) + (ensure-vo t vio vo )) + + ;; without dep + (((src vio vo)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((src vio) vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((vo (src vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((src vo) vio) + (no-quick nil vo vio ) + (quick nil vo vio ) + (ensure-vo t vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((vio (src vo)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((vio vo) src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((src (vio vo)) + ;; could also use the vio as 'req-obj-file in the first 2 cases here + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) + + ;; 2 files with identical time stamp out of 2 files + (((src dep)) + (no-quick t nil vo ) + (quick t nil vio ) + (ensure-vo t nil vo )) + + (((src vo)) + (no-quick t nil vo ) + (quick t vo vio ) + (ensure-vo t nil vo )) + + (((src vio)) + (no-quick t vio vo ) + (quick t nil vio ) + (ensure-vo t vio vo )) ) "Test and result specification for `coq-par-job-needs-compilation'. @@ -302,7 +701,11 @@ a (already compiled) dependency (dep.vo or dep.vio), `vo' for the .vo file (x.vo) and `vio' for the .vio file (x.vio). A label in the list denotes an existing file, a missing label a missing file. The first element is the oldest file, the last element the -newest file. +newest file. A sublist specifies a set of files with identical +time stamps. For example, ``(src (vo vio) dep)'' specifies source +is older than .vo and .vio, .vo and .vio have identical last +modification time stamps and .vo and .vio are older than the +dependency. Elements 2-4 of a test specify the results and side effects of `coq-par-job-needs-compilation' for all setting of @@ -310,7 +713,7 @@ Elements 2-4 of a test specify the results and side effects of element 1. The options `quick-no-vio2vo' and `quick-and-vio2vo' are specified together with label `quick'. Each result and side effect specification (also called a variant in the source code -below) is itself a list of 5 elements. Element 1 is the value for +below) is itself a list of 4 elements. Element 1 is the value for `coq-compile-quick', where `quick' denotes both `quick-no-vio2vo' and `quick-and-vio2vo'. Element 2 specifies the result of `coq-par-job-needs-compilation', nil for don't compile, t for do @@ -320,77 +723,18 @@ must be deleted, where nil means no file must be deleted. Element `required-obj-file' property of the job. This file will be used as the compiled module library. In case compilation is needed (element 2 equals t), this is the target of the -compilation. Element 5 specifies the file whose time stamp must -be stored in the `obj-mod-time' property of the job. A value of -nil there specifies that the `obj-mod-time' property should -contain nil. Element 5 is a bit superfluous, because it must be -set precisely when no compilation is needed (element 2 equals -nil) and then it must equal element 4. +compilation. This list contains 1 test for all possible file configuration and relative ages.") -;; missing test cases for some objects with identical time stamp -;; -;; src-vo-dep-vio -;; -;; src-vo-dep vio -;; vio src-vo-dep -;; src-vo-vio dep -;; dep src-vo-vio -;; src-dep-vio vo -;; vo src-dep-vio -;; vo-dep-vio src -;; src vo-dep-vio -;; -;; src-vo dep-vio -;; dep-vio src-vo -;; src-dep vo-vio -;; vo-vio src-dep -;; src-vio vo-dep -;; vo-dep src-vio -;; -;; src-vo dep vio -;; src-vo vio dep -;; dep src-vo vio -;; dep vio src-vo -;; vio src-vo dep -;; vio dep src-vo -;; -;; src-dep vo vio -;; src-dep vio vo -;; vo src-dep vio -;; vo vio src-dep -;; vio src-dep vo -;; vio vo src-dep -;; -;; src-vio vo dep -;; src-vio dep vo -;; vo src-vio dep -;; vo dep src-vio -;; dep src-vio vo -;; dep vo src-vio -;; -;; vo-dep src vio -;; vo-dep vio src -;; src vo-dep vio -;; src vio vo-dep -;; vio vo-dep src -;; vio src vo-dep -;; -;; vo-vio src dep -;; vo-vio dep src -;; src vo-vio dep -;; src dep vo-vio -;; dep vo-vio src -;; dep src vo-vio -;; -;; dep-vio src vo -;; dep-vio vo src -;; src dep-vio vo -;; src vo dep-vio -;; vo dep-vio src -;; vo src dep-vio +(defun coq-par-test-flatten-files (file-descr) + "Flatten a file description test case list into a list of files." + (let (result) + (dolist (f file-descr result) + (if (listp f) + (setq result (append f result)) + (push f result))))) (defun test-coq-par-test-data-invarint () "Wellformedness check for the test specifications." @@ -405,26 +749,16 @@ relative ages.") nil (concat test-id " 1")) (mapc (lambda (variant) - ;; a variant is a list of 5 elements - (assert (eq (length variant) 5) nil (concat test-id " 2")) - (let ((compilation-result (nth 1 variant)) + ;; a variant is a list of 4 elements + (assert (eq (length variant) 4) nil (concat test-id " 2")) + (let ((files (coq-par-test-flatten-files (car test))) + (compilation-result (nth 1 variant)) (delete-result (nth 2 variant)) - (req-obj-result (nth 3 variant)) - (obj-mod-result (nth 4 variant))) - ;; when the obj-mod-time field is set, it must be equal to - ;; the required-obj-file field - (assert (or (not obj-mod-result) - (eq req-obj-result obj-mod-result)) - nil (concat test-id " 3")) - (if compilation-result - ;; when compilation is t, obj-mod-time must be set - (assert (not obj-mod-result) nil (concat test-id " 4")) - ;; when compilation? is nil, obj-mod-result must be nil - (assert obj-mod-result nil (concat test-id " 5"))) + (req-obj-result (nth 3 variant))) ;; the delete field, when set, must be a member of the files list (assert (or (not delete-result) - (member delete-result (car test))) - nil (concat test-id " 6")))) + (member delete-result files)) + nil (concat test-id " 3")))) (cdr test)))) coq-par-job-needs-compilation-tests)) @@ -438,13 +772,13 @@ relative ages.") (t (assert nil))))) (concat dir "/" file))) -(defun test-coq-par-one-test (counter dir files variant dep-just-compiled) +(defun test-coq-par-one-test (counter dir file-descr variant dep-just-compiled) "Do one test for one specific `coq-compile-quick' value. This function creates the files in DIR, sets up a job with the necessary fields, calls `coq-par-job-needs-compilation-tests' and test the result and side effects wth `assert'." - (let ((id (format "%s: %s %s%s" counter (car variant) files + (let ((id (format "%s: %s %s%s" counter (car variant) file-descr (if dep-just-compiled " just" ""))) (job (make-symbol "coq-compile-job-symbol")) (module-vo-file (concat dir "/a.vo")) @@ -452,9 +786,17 @@ test the result and side effects wth `assert'." (compilation-result (nth 1 variant)) (delete-result (nth 2 variant)) (req-obj-result (nth 3 variant)) - (obj-mod-result (nth 4 variant)) - result non-deleted-files) - (message "test case %s" id) + (different-counter 5) + (same-counter 5) + (different-not-ok t) + (same-not-ok t) + (last-different-time-stamp '(0 0)) + same-time-stamp file-list + obj-mod-result result) + (message "test case %s/576: %s %s%s" counter (car variant) file-descr + (if dep-just-compiled " just" "")) + (when (not compilation-result) + (setq obj-mod-result req-obj-result)) (ignore-errors (delete-directory dir t)) (make-directory dir) @@ -464,18 +806,50 @@ test the result and side effects wth `assert'." (put job 'youngest-coqc-dependency '(0 0)) (put job 'name id) ;; create files in order - (mapc - (lambda (sym) - (let ((file (test-coq-par-sym-to-file dir sym))) - ;;(message "file create for %s: %s" sym file) - (with-temp-file file t) - (when (eq sym 'dep) - (put job 'youngest-coqc-dependency (nth 5 (file-attributes file)))) - (unless (eq sym delete-result) - (push file non-deleted-files)) - (sleep-for 0 10) - )) - files) + (while different-not-ok + ;; (message "enter different loop %s at %s" + ;; different-counter (current-time)) + (setq different-not-ok nil) + (setq different-counter (1- different-counter)) + (assert (> different-counter 0) + nil "create files with different time stamps failed") + (dolist (same-descr file-descr) + (when (symbolp same-descr) + (setq same-descr (list same-descr))) + (setq file-list + (mapcar (lambda (sym) (test-coq-par-sym-to-file dir sym)) + same-descr)) + ;; (message "try %s files %s" same-descr file-list) + (setq same-counter 5) + (setq same-not-ok t) + (while same-not-ok + (setq same-counter (1- same-counter)) + (assert (> same-counter 0) + nil "create files with same time stamp filed") + (dolist (file file-list) + (with-temp-file file t)) + ;; check now that all the files in file-list have the same time stamp + (setq same-not-ok nil) + (setq same-time-stamp (nth 5 (file-attributes (car file-list)))) + ;; (message "got first time stamp %s" same-time-stamp) + (dolist (file (cdr file-list)) + (let ((ots (nth 5 (file-attributes file)))) + ;; (message "got other time stamp %s" ots) + (unless (equal same-time-stamp ots) + (setq same-not-ok t))))) + ;; (message "successful finished %s" same-descr) + (when (member 'dep same-descr) + (put job 'youngest-coqc-dependency + (nth 5 (file-attributes (test-coq-par-sym-to-file dir 'dep))))) + ;; (message "XX %s < %s = %s" + ;; last-different-time-stamp same-time-stamp + ;; (time-less-p last-different-time-stamp same-time-stamp)) + (unless (time-less-p last-different-time-stamp same-time-stamp) + ;; error - got the same time stamp + ;; (message "unsuccsessful - need different retry") + (setq different-not-ok t)) + (setq last-different-time-stamp same-time-stamp) + (sleep-for 0 15))) (when dep-just-compiled (put job 'youngest-coqc-dependency 'just-compiled)) (setq result (coq-par-job-needs-compilation job)) @@ -488,11 +862,12 @@ test the result and side effects wth `assert'." (test-coq-par-sym-to-file dir delete-result)))) nil (concat id " delete file")) ;; check no other file is deleted - (mapc - (lambda (f) - (assert (file-attributes f) - nil (concat id " non del file " f))) - non-deleted-files) + (dolist (f (coq-par-test-flatten-files file-descr)) + (unless (eq f delete-result) + (assert (file-attributes (test-coq-par-sym-to-file dir f)) + nil (format "%s non del file %s: %s" + id f + (test-coq-par-sym-to-file dir f))))) ;; check value of 'required-obj-file property (assert (equal (get job 'required-obj-file) (test-coq-par-sym-to-file dir req-obj-result)) @@ -510,7 +885,9 @@ test the result and side effects wth `assert'." ;; check 'use-quick property (assert (eq (not (not (and compilation-result (eq req-obj-result 'vio)))) (get job 'use-quick)) - nil (concat id " use-quick")))) + nil (concat id " use-quick")) + (ignore-errors + (delete-directory dir t)))) (defvar test-coq-par-counter 0 "Stupid counter.") @@ -531,7 +908,7 @@ test the result and side effects wth `assert'." (setq test-coq-par-counter (1+ test-coq-par-counter))) (defun test-coq-par-job-needs-compilation (dir) - "Check test date wellformedness and run all the tests." + "Check test data wellformedness and run all the tests." (test-coq-par-test-data-invarint) (setq test-coq-par-counter 1) (mapc |