don't unnecessarily delete .vio files for ensure-vo

If both .vio and .vo exists, coq loads the newer one. Therefore,
for ensure-vo, don't delete up-to-date .vio files when the .vo is
newer.

2 files changed, 39 insertions, 32 deletions

diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index e88c72c5..dab1cf42 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -966,7 +966,8 @@ therefore delete a file if it might be in the way. Sets the
     ;; which of both is newer. This is only meaningful if at least one of
     ;; the .vo or .vio file exists.
     (cond
-     ((and vio-obj-time vo-obj-time (time-less-p vo-obj-time vio-obj-time))
+     ((and vio-obj-time vo-obj-time
+	   (time-less-or-equal vo-obj-time vio-obj-time))
       (setq max-obj-time vio-obj-time)
       (setq vio-is-newer t))
      ((and vio-obj-time vo-obj-time)
@@ -1015,10 +1016,13 @@ therefore delete a file if it might be in the way. Sets the
 			 (time-less-p src-time vo-obj-time)
 			 (time-less-p dep-time vo-obj-time)))
 		;; .vo is newer than src and youngest dep - don't compile
-		;; need to ensure no .vio is laying around
 		(progn
 		  (put job 'obj-mod-time vo-obj-time)
-		  (when vio-obj-time
+		  ;; delete vio if it is outdated or newer than vo
+		  (when (and vio-obj-time
+			     (or vio-is-newer
+				 (time-less-or-equal vio-obj-time src-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 1; delete %s"
@@ -1026,7 +1030,10 @@ therefore delete a file if it might be in the way. Sets the
 			     (if file-to-delete file-to-delete "noting"))))
 	      ;; .vo outdated - need to compile
 	      (setq result t)
-	      (when vio-obj-time
+	      ;; delete vio if it is outdated
+	      (when (and vio-obj-time
+			 (or (time-less-or-equal vio-obj-time src-time)
+			     (time-less-or-equal vio-obj-time dep-time)))
 		(setq file-to-delete vio-file))
 	      (when coq-debug-auto-compilation
 		(message "%s: need to compile to vo; delete %s"
diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el
index d22102c8..1ce85d0d 100644
--- a/coq/coq-par-test.el
+++ b/coq/coq-par-test.el
@@ -35,12 +35,12 @@
     ((src dep vio vo)
      (no-quick           nil            nil       vio)
      (quick              nil            nil       vio)
-     (ensure-vo          nil            vio       vo ))
+     (ensure-vo          nil            nil       vo ))
 
     ((src vo dep vio)    
      (no-quick           nil            vo        vio)
      (quick              nil            vo        vio)
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ((src vo vio dep)
      (no-quick           t              vio       vo )
@@ -61,7 +61,7 @@
     ((dep src vio vo)
      (no-quick           nil            nil       vio)
      (quick              nil            nil       vio)
-     (ensure-vo          nil            vio       vo ))
+     (ensure-vo          nil            nil       vo ))
 
     ((dep src vo vio)
      (no-quick           nil            nil       vo )
@@ -76,7 +76,7 @@
     ((dep vo src vio)
      (no-quick           nil            vo        vio)
      (quick              nil            vo        vio)
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ((dep vio vo src)
      (no-quick           t              vio       vo )
@@ -91,7 +91,7 @@
     ((vo src dep vio)
      (no-quick           nil            vo        vio)
      (quick              nil            vo        vio)
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ;; present files   | compilation? | delete | 'req-obj-file
     ((vo src vio dep)
@@ -102,7 +102,7 @@
     ((vo dep src vio)
      (no-quick           nil            vo       vio )
      (quick              nil            vo       vio )
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ((vo dep vio src)
      (no-quick           t              vio       vo )
@@ -188,7 +188,7 @@
     ((src dep vio)
      (no-quick           nil            nil      vio )
      (quick              nil            nil      vio )
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ((src vio dep)
      (no-quick           t             vio       vo  )
@@ -198,7 +198,7 @@
     ((dep src vio)
      (no-quick           nil           nil       vio )
      (quick              nil           nil       vio )
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ((dep vio src)
      (no-quick           t             vio       vo  )
@@ -226,12 +226,12 @@
     ((src vio vo)
      (no-quick           nil            nil       vio)
      (quick              nil            nil       vio)
-     (ensure-vo          nil            vio       vo ))
+     (ensure-vo          nil            nil       vo ))
 
     ((vo src vio)
      (no-quick           nil            vo       vio )
      (quick              nil            vo       vio )
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ((vo vio src)
      (no-quick           t              vio      vo  )
@@ -278,7 +278,7 @@
     ((src vio)
      (no-quick           nil            nil      vio )
      (quick              nil            nil      vio )
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ((vio src)
      (no-quick           t              vio      vo  )
@@ -306,7 +306,7 @@
     (((src vo dep) vio)
      (no-quick           nil            vo       vio )
      (quick              nil            vo       vio )
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ((vio (src vo dep))
      (no-quick           t              vio      vo  )
@@ -357,8 +357,8 @@
 
     (((src dep) (vo vio))
      ;; could also use the vio as 'req-obj-file in the first 2 cases here
-     (no-quick           nil            nil       vio)
-     (quick              nil            nil       vio)
+     (no-quick           nil            nil       vo )
+     (quick              nil            nil       vo )
      (ensure-vo          nil            vio       vo ))
 
     (((vo vio) (src dep))
@@ -381,7 +381,7 @@
     (((src vo) dep vio)
      (no-quick           nil            vo        vio)
      (quick              nil            vo        vio)
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     (((src vo) vio dep)
      (no-quick           t              vio       vo )
@@ -391,7 +391,7 @@
     ((dep (src vo) vio)
      (no-quick           nil            vo        vio)
      (quick              nil            vo        vio)
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ((dep vio (src vo))
      (no-quick           t              vio       vo )
@@ -417,12 +417,12 @@
     (((src dep) vio vo)
      (no-quick           nil            nil       vio)
      (quick              nil            nil       vio)
-     (ensure-vo          nil            vio       vo ))
+     (ensure-vo          nil            nil       vo ))
 
     ((vo (src dep) vio)
      (no-quick           nil            vo        vio)
      (quick              nil            vo        vio)
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ((vo vio (src dep))
      (no-quick           t              vio       vo )
@@ -473,7 +473,7 @@
     (((vo dep) src vio)
      (no-quick           nil            vo       vio )
      (quick              nil            vo       vio )
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     (((vo dep) vio src)
      (no-quick           t              vio       vo )
@@ -483,7 +483,7 @@
     ((src (vo dep) vio)
      (no-quick           nil            vo        vio)
      (quick              nil            vo        vio)
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ((src vio (vo dep))
      (no-quick           t              vio       vo )
@@ -518,8 +518,8 @@
 
     ((src dep (vo vio))
      ;; could also use the vio as 'req-obj-file in the first 2 cases here
-     (no-quick           nil            nil       vio)
-     (quick              nil            nil       vio)
+     (no-quick           nil            nil       vo )
+     (quick              nil            nil       vo )
      (ensure-vo          nil            vio       vo ))
 
     ((dep (vo vio) src)
@@ -529,8 +529,8 @@
 
     ((dep src (vo vio))
      ;; could also use the vio as 'req-obj-file in the first 2 cases here
-     (no-quick           nil            nil       vio)
-     (quick              nil            nil       vio)
+     (no-quick           nil            nil       vo )
+     (quick              nil            nil       vo )
      (ensure-vo          nil            vio       vo ))
 
     (((dep vio) src vo)
@@ -611,7 +611,7 @@
     (((src dep) vio)
      (no-quick           nil           nil       vio )
      (quick              nil           nil       vio )
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ((vio (src dep))
      (no-quick           t              vio       vo )
@@ -657,7 +657,7 @@
     (((src vo) vio)
      (no-quick           nil            vo       vio )
      (quick              nil            vo       vio )
-     (ensure-vo          t              vio       vo ))
+     (ensure-vo          t              nil       vo ))
 
     ;; present files   | compilation? | delete | 'req-obj-file
     ((vio (src vo))
@@ -672,8 +672,8 @@
 
     ((src (vio vo))
      ;; could also use the vio as 'req-obj-file in the first 2 cases here
-     (no-quick           nil            nil       vio)
-     (quick              nil            nil       vio)
+     (no-quick           nil            nil       vo )
+     (quick              nil            nil       vo )
      (ensure-vo          nil            vio       vo ))
 
     ;; 2 files with identical time stamp out of 2 files