diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2016-11-22 23:06:30 +0100 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2016-11-22 23:07:29 +0100 |
| commit | d33897df4d6a2af94d0d315707111528a3c4a403 (patch) | |
| tree | 3e8837c6142f27f9ca86c414ba1b971492fa9273 /coq/coq-par-test.el | |
| parent | c4caac41845362173499397e589e9619f5e18d77 (diff) | |
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.
Diffstat (limited to 'coq/coq-par-test.el')
| -rw-r--r-- | coq/coq-par-test.el | 48 |
1 files changed, 24 insertions, 24 deletions
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 |