diff options
| -rw-r--r-- | coq/coq-compile-common.el | 7 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 59 | ||||
| -rw-r--r-- | coq/coq-par-test.el | 48 |
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 |