From 74f3e963ffcc1178e052e24b56a80938314815cb Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 30 Jun 2022 01:30:14 -0400 Subject: [PATCH] feat: use `nativeFacets` in exe's `recBuild` --- Lake/Build/Roots.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Lake/Build/Roots.lean b/Lake/Build/Roots.lean index 86ffb5e2c7..8755a9331a 100644 --- a/Lake/Build/Roots.lean +++ b/Lake/Build/Roots.lean @@ -86,7 +86,10 @@ 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 - return arr.push <| Target.active <| ← mod.o.recBuild + let mut arr := arr + for facet in mod.nativeFacets do + arr := arr.push <| Target.active <| ← recBuild <| mod.facet facet.name + return arr 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