From 42312958454c0fcc700586781084510f7da0dbcd Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Thu, 17 Nov 2016 13:06:37 +0100 Subject: 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. --- coq/coq-par-compile.el | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'coq/coq-par-compile.el') 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" -- cgit v1.2.3