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

fix: build o files again to enable incremental rebuilds

Browse source 
This reverts commit 182a5787aabd8924823f2232a518911c81b2b2cd.
This commit is contained in:
tydeu 2022-06-29 18:05:53 -04:00
parent 49384a69bf
commit c6f7a0d654
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
Lake/Build/Roots.lean
View file

@ -86,8 +86,7 @@ def LeanExe.recBuild (self : LeanExe) : IndexT m ActiveFileTarget := do
let (_, imports) ← self.root.imports.recBuild
let linkTargets := #[Target.active <| ← self.root.o.recBuild]
let mut linkTargets ← imports.foldlM (init := linkTargets) fun arr mod => do
-- NOTE: Building only C files cuts the build time in half
return arr.push <| Target.active <| ← mod.c.recBuild
return arr.push <| Target.active <| ← mod.o.recBuild
let deps := (← recBuild <| self.pkg.facet &`deps).push self.pkg
for dep in deps do for lib in dep.externLibs do
linkTargets := linkTargets.push <| Target.active <| ← lib.static.recBuild