improve compilation when both .vio and .vo are up-to-date

In this case Coq loads the younger file and emits a warning if
the .vio file is the younger one. With this patch, the dependency
analysis for parallel compilation continues with the older value.
The interesting case to look at is when b.v depends on a.v and
both are compiled with -quick and later a parallel vio2vo
produces a.vo and b.vo such that b.vo is older (because, eg. b.v
is shorter than a.v). Without this patch a second auto
compilation would recompile b.v, because the dependency a.vo is
younger.

3 files changed, 66 insertions, 48 deletions

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 1840f9a0..910fbd7e 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -389,9 +389,10 @@ modules are matched separately with `coq-require-id-regexp'")
 
 (defun time-less-or-equal (time-1 time-2)
   "Return `t' if time value time-1 is earlier or equal to time-2.
-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."
+A time value is a list of two, three or four integers of the
+form (high low micro pico) as returned by `file-attributes' or
+'current-time'. First element high contains the upper 16 bits and
+the second low the lower 16 bits of the time."
   (not (time-less-p time-2 time-1)))
 
 (defun coq-max-dep-mod-time (dep-mod-times)
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index d4ad2a7e..934a9932 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -873,7 +873,8 @@ therefore delete a file if it might be in the way."
 	 (vio-obj-time (nth 5 (file-attributes vio-file)))
 	 (dep-time (get job 'youngest-coqc-dependency))
 	 (src-time (nth 5 (file-attributes (get job 'src-file))))
-	 file-to-delete max-obj-time vio-is-newer result)
+	 file-to-delete max-obj-time vio-is-newer
+	 other-file other-obj-time result)
     (when coq-debug-auto-compilation
       (message
        (concat "%s: compare mod times: vo mod %s, vio mod %s, src mod %s, "
@@ -960,30 +961,46 @@ therefore delete a file if it might be in the way."
 	;; There is an up-to-date .vio or .vo file and the user does not
 	;; insist on either .vio or .vo - no need to compile.
 	;; Ensure to delete outdated .vio or .vo files.
+	;; First store the other obj file in other-file and other-obj-time.
 	(if vio-is-newer
+	    (setq other-file vo-file
+		  other-obj-time vo-obj-time)
+	  (setq other-file vio-file
+		other-obj-time vio-obj-time))
+	(if (and other-obj-time
+		 (time-less-p src-time other-obj-time)
+		 ;; dep-time is neither nil nor 'just-compiled here
+		 (time-less-p dep-time other-obj-time))
+	    ;; Both the .vio and .vo exist and are up-to-date. Coq
+	    ;; loads the younger one but we continue with the older
+	    ;; one to avoid recompilation for the case where a vio2vo
+	    ;; process took a long time for a dependency.
 	    (progn
-	      (put job 'required-obj-file vio-file)
-	      (put job 'obj-mod-time vio-obj-time)
-	      (when (and vo-obj-time
-			 (or (time-less-or-equal vo-obj-time src-time)
-			     ;; dep-time is neither nil nor 'just-compiled here
-			     (time-less-or-equal vo-obj-time dep-time)))
-		(setq file-to-delete vo-file))
+	      (put job 'required-obj-file other-file)
+	      (put job 'obj-mod-time other-obj-time)
 	      (when coq-debug-auto-compilation
-		(message "%s: vio up-to-date; delete %s"
+		(message (concat "%s: .vio and .vo up-to-date, "
+				 "continue with the older %s")
 			 (get job 'name)
-			 (if file-to-delete file-to-delete "noting"))))
-	  (put job 'required-obj-file vo-file)
-	  (put job 'obj-mod-time vo-obj-time)
-	  (when (and vio-obj-time
-		     (or (time-less-or-equal vio-obj-time src-time)
-			 ;; dep-time is neither nil nor 'just-compiled here
-			 (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"
-		     (get job 'name)
-		     (if file-to-delete file-to-delete "noting"))))))
+			 (if vio-is-newer ".vio" ".vo"))))
+	  ;; The other obj file does not exist or is outdated.
+	  ;; Delete the outdated if it exists.
+	  (when other-obj-time
+	    (setq file-to-delete other-file))
+	  (if vio-is-newer
+	      (progn
+		(put job 'required-obj-file vio-file)
+		(put job 'obj-mod-time vio-obj-time)
+		(when coq-debug-auto-compilation
+		  (message "%s: vio up-to-date; delete %s"
+			   (get job 'name)
+			   (if file-to-delete file-to-delete "noting"))))
+	    (put job 'required-obj-file vo-file)
+	    (put job 'obj-mod-time vo-obj-time)
+	    (when coq-debug-auto-compilation
+	      (message "%s: vo up-to-date 2; delete %s"
+		       (get job 'name)
+		       (if file-to-delete file-to-delete "noting")))))))
     (when file-to-delete
       (condition-case err
 	  (delete-file file-to-delete)
diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el
index 019ae62f..4d28dc79 100644
--- a/coq/coq-par-test.el
+++ b/coq/coq-par-test.el
@@ -28,13 +28,13 @@
     ;; ====================================================================
     ;; all of src dep vo vio present
     ((src dep vo vio)
-     (no-quick           nil            nil       vio)
-     (quick              nil            nil       vio)
+     (no-quick           nil            nil       vo )
+     (quick              nil            nil       vo )
      (ensure-vo          nil            vio       vo ))
 
     ((src dep vio vo)
-     (no-quick           nil            nil       vo )
-     (quick              nil            nil       vo )
+     (no-quick           nil            nil       vio)
+     (quick              nil            nil       vio)
      (ensure-vo          nil            vio       vo ))
 
     ((src vo dep vio)    
@@ -59,13 +59,13 @@
 
     ;; present files   | compilation? | delete | 'req-obj-file
     ((dep src vio vo)
-     (no-quick           nil            nil       vo )
-     (quick              nil            nil       vo )
+     (no-quick           nil            nil       vio)
+     (quick              nil            nil       vio)
      (ensure-vo          nil            vio       vo ))
 
     ((dep src vo vio)
-     (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)
@@ -219,13 +219,13 @@
     ;; present files   | compilation? | delete | 'req-obj-file
     ;; only src vo vio present
     ((src vo vio)
-     (no-quick           nil            nil      vio )
-     (quick              nil            nil      vio )
+     (no-quick           nil            nil       vo )
+     (quick              nil            nil       vo )
      (ensure-vo          nil            vio       vo ))
 
     ((src vio vo)
-     (no-quick           nil            nil      vo  )
-     (quick              nil            nil      vo  )
+     (no-quick           nil            nil       vio)
+     (quick              nil            nil       vio)
      (ensure-vo          nil            vio       vo ))
 
     ((vo src vio)
@@ -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       vo)
-     (quick              nil            nil       vo)
+     (no-quick           nil            nil       vio)
+     (quick              nil            nil       vio)
      (ensure-vo          nil            vio       vo ))
 
     (((vo vio) (src dep))
@@ -410,13 +410,13 @@
 
     ;; present files   | compilation? | delete | 'req-obj-file
     (((src dep) vo vio)
-     (no-quick           nil            nil       vio)
-     (quick              nil            nil       vio)
+     (no-quick           nil            nil       vo )
+     (quick              nil            nil       vo )
      (ensure-vo          nil            vio       vo ))
 
     (((src dep) vio vo)
-     (no-quick           nil            nil       vo )
-     (quick              nil            nil       vo )
+     (no-quick           nil            nil       vio)
+     (quick              nil            nil       vio)
      (ensure-vo          nil            vio       vo ))
 
     ((vo (src dep) vio)
@@ -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       vo)
-     (quick              nil            nil       vo)
+     (no-quick           nil            nil       vio)
+     (quick              nil            nil       vio)
      (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       vo)
-     (quick              nil            nil       vo)
+     (no-quick           nil            nil       vio)
+     (quick              nil            nil       vio)
      (ensure-vo          nil            vio       vo ))
 
     (((dep 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       vo )
-     (quick              nil            nil       vo )
+     (no-quick           nil            nil       vio)
+     (quick              nil            nil       vio)
      (ensure-vo          nil            vio       vo ))
 
     ;; 2 files with identical time stamp out of 2 files