fix parallel compilation for the unlikely case of identical time stamps

Since version 24.3 Emacs supports pico second precision in time
stamps and Emacs on ext4 seems to have a time precision of 5
milliseconds for file time stamps. It is therefor quite unlikely
that a source and an object file have the same time stamp. This
patch fixes parallel compilation for these corner cases and adds
a few hundred test cases to test all combinations where some
files have identical time stamps. On Emacs older than 24.3 or on
file systems with a low precision (eg. ext3) this patch can cause
additional compilations.

1 files changed, 642 insertions, 265 deletions

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