diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2016-11-23 22:12:19 +0100 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2016-11-29 23:49:20 +0100 |
| commit | 6be1cced12f8e9de9724a73b8b0fb29440cad3dc (patch) | |
| tree | 07d1bf24747a1dac0786d3f63a15632501c15f9a /coq/coq-par-compile.el | |
| parent | 1466839c2182b76853380a7c91e86af30fd9778f (diff) | |
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.
Diffstat (limited to 'coq/coq-par-compile.el')
| -rw-r--r-- | coq/coq-par-compile.el | 15 |
1 files changed, 11 insertions, 4 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" |