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

fix: don't duplicate dep link targets in diamonds

Browse source 
closes  leanprover/lake#43
This commit is contained in:
tydeu 2022-01-31 00:49:42 -05:00
parent 30e3f10c6c
commit 985bdcb4d0
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
Lake/Build/Binary.lean
View file

@ -50,12 +50,14 @@ def Package.linkTargetsOf
(targetMap : NameMap ActiveOleanAndCTarget) (self : Package) : LakeM (Array FileTarget) := do
let collect dep recurse := do
let pkg := (← getPackageByName? dep.name).get!
let depTargets ← pkg.dependencies.concatMapM recurse
return pkg.oFileTargetsOf targetMap ++ pkg.moreLibTargets ++ depTargets
let x ← RBTopT.run' <| self.dependencies.concatMapM fun dep =>
buildRBTop (cmp := Name.quickCmp) collect Dependency.name dep
pkg.dependencies.forM fun dep => discard <| recurse dep
return pkg.oFileTargetsOf targetMap ++ pkg.moreLibTargets
let ⟨x, map⟩ ← RBTopT.run <| self.dependencies.forM fun dep =>
discard <| buildRBTop (cmp := Name.quickCmp) collect Dependency.name dep
match x with
| Except.ok ts => return self.oFileTargetsOf targetMap ++ self.moreLibTargets ++ ts
| Except.ok _ =>
let ts := map.fold (fun acc _ vs => acc ++ vs) #[]
return self.oFileTargetsOf targetMap ++ self.moreLibTargets ++ ts
| Except.error _ => panic! "dependency cycle emerged after resolution"
protected def Package.sharedLibTarget (self : Package) : FileTarget :=