diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2016-11-17 13:06:37 +0100 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2016-11-17 13:06:37 +0100 |
| commit | 42312958454c0fcc700586781084510f7da0dbcd (patch) | |
| tree | db98c263a285200bcfcdeee7ed00545eceedb9c6 /coq/coq-par-compile.el | |
| parent | 94e8ce4389c1d9926a629d30075dae64bee84779 (diff) | |
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.
Diffstat (limited to 'coq/coq-par-compile.el')
| -rw-r--r-- | coq/coq-par-compile.el | 16 |
1 files changed, 9 insertions, 7 deletions
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" |