max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: once again use to lean target mtime in fetch

Browse source
This commit is contained in:
tydeu 2021-07-13 13:40:05 -04:00
parent 511f34fd53
commit 4844f8c459
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
Lake/Build.lean
View file

@ -174,16 +174,17 @@ def fetchAfterDirectLocalImports
fun mod fetch => do
let leanFile := pkg.modToSource mod
let imports ← parseDirectLocalImports pkg.module leanFile
-- we fetch the import targets even if a rebuild is not required
-- because other build processes (ex. `.o`) rely on the map being complete
let importTargets ← imports.mapM fetch
-- calculate max dependency `MTime`
let leanMTime ← getMTime leanFile
let importMTimes ← imports.mapM fun i => getMTime <| pkg.modToSource i
let importMTimes ← importTargets.map (·.mtime)
let depMTime := MTime.listMax <| leanMTime :: depsTarget.mtime :: importMTimes
-- construct target
let cFile := pkg.modToC mod
let oleanFile := pkg.modToOlean mod
-- we fetch the import targets even if a rebuild is not required
-- because other build processes (ex. `.o`) rely on the map being complete
let importTasks ← imports.mapM fun i => fetch i >>= (·.buildTask)
let importTasks := importTargets.map (·.buildTask)
skipIfNewer ⟨oleanFile, cFile⟩ depMTime <|
BuildTask.afterTasks (depsTarget.buildTask :: importTasks) <| catchErrors <|
compileOleanAndC leanFile oleanFile cFile leanPath pkg.dir pkg.leanArgs