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.

1 files changed, 38 insertions, 21 deletions

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)