fix: do not resolve the same dependency multiple times

Lake/BuildBin.lean

@@ -37,12 +37,11 @@ def buildLib (pkg : Package) : IO PUnit :=
 -- # Build Package Bin
 
 def ActivePackageTarget.linkTargets
-(depTargets : List ActivePackageTarget) (self : ActivePackageTarget) : Array FileTarget :=
-  depTargets.foldl (fun ts dep => ts ++ dep.staticLibTargets) <|
-    self.oFileTargets ++ self.package.moreLibTargets
+(depTargets : Array ActivePackageTarget) (self : ActivePackageTarget) : Array FileTarget :=
+  self.oFileTargets ++ self.package.moreLibTargets ++ depTargets.concatMap (·.staticLibTargets)
 
 protected def ActivePackageTarget.binTarget
-(depTargets : List ActivePackageTarget) (self : ActivePackageTarget) : FileTarget :=
+(depTargets : Array ActivePackageTarget) (self : ActivePackageTarget) : FileTarget :=
   let linkTargets := self.linkTargets depTargets
   binTarget self.package.binFile linkTargets self.package.linkArgs "leanc"
 

Lake/BuildMonad.lean

@@ -81,8 +81,8 @@ def logError (msg : String) : BuildM PUnit := do
 def runIn (ctx : BuildContext) (self : BuildM α) : IO α :=
   self ctx
 
-def run (self : BuildM α) : IO PUnit :=
-  runIn BuildContext.io do try discard self catch e =>
+def run' (self : BuildM α) : IO α :=
+  runIn BuildContext.io do try self catch e =>
     /-
       Remark: Actual error should have already been logged earlier.
       However, if the error was thrown by something that did not know it was
@@ -93,6 +93,9 @@ def run (self : BuildM α) : IO PUnit :=
     BuildM.logError s!"build error: {toString e}"
     throw <| IO.userError "build failed"
 
+def run (self : BuildM α) : IO PUnit :=
+  discard self.run'
+
 end BuildM
 
 def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α

Lake/BuildPackage.lean

@@ -32,6 +32,10 @@ def moduleTargets (self : ActivePackageTarget) : Array (Name × ActiveOleanAndCT
 
 end ActivePackageTarget
 
+/-- Returns the `oleanDir`s of the given package targets in reverse order. -/
+def packageTargetsToOleanDirs (targets : Array ActivePackageTarget) : List FilePath :=
+  targets.map (·.package.oleanDir) |>.foldl (flip List.cons) []
+
 -- # Build Modules
 
 def Package.buildModuleOleanAndCTargetDAG
@@ -87,22 +91,22 @@ def Package.buildOleanTargets
 -- # Configure/Build Packages
 
 def Package.buildDepTargetWith
-(depTargets : List ActivePackageTarget) (self : Package) : BuildM ActiveOpaqueTarget := do
+(depTargets : Array ActivePackageTarget) (self : Package) : BuildM ActiveOpaqueTarget := do
   let extraDepTarget ← self.extraDepTarget.run
-  let depTarget ← ActiveTarget.collectOpaqueList depTargets
+  let depTarget ← ActiveTarget.collectOpaqueArray depTargets
   extraDepTarget.mixOpaqueAsync depTarget
 
 def Package.buildModuleOleanAndCTargetsWithDepTargets
-(mods : Array Name) (depTargets : List ActivePackageTarget) (self : Package)
+(mods : Array Name) (depTargets : Array ActivePackageTarget) (self : Package)
 : BuildM ActivePackageTarget := do
   let depTarget ← self.buildDepTargetWith depTargets
-  let moreOleanDirs := depTargets.map (·.package.oleanDir)
+  let moreOleanDirs := packageTargetsToOleanDirs depTargets
   let (targets, targetMap) ← self.buildModuleOleanAndCTargetDAG mods moreOleanDirs depTarget
   let target ← ActiveTarget.collectOpaqueArray targets
   return target.withInfo ⟨self, targetMap⟩
 
 def Package.buildOleanAndCTargetsWithDepTargets
-(depTargets : List ActivePackageTarget) (self : Package) : BuildM ActivePackageTarget := do
+(depTargets : Array ActivePackageTarget) (self : Package) : BuildM ActivePackageTarget := do
   self.buildModuleOleanAndCTargetsWithDepTargets (← self.getModuleArray) depTargets
 
 /--
@@ -111,28 +115,35 @@ def Package.buildOleanAndCTargetsWithDepTargets
   It resolves the package's dependencies and recursively builds them.
   For each package, it compiles its modules into `.olean` and `.c` files.
 -/
-def recBuildPkgWithDeps [Monad m] [MonadLiftT BuildM m]
-: RecBuild Package ActivePackageTarget m := fun pkg buildPkg => do
-  -- TODO: merge dependency resolution into build
-  let deps ← liftM (m := BuildM) <| solveDeps pkg
-  pkg.buildOleanAndCTargetsWithDepTargets (← deps.mapM buildPkg)
+def recBuildPackageWithDeps
+[Monad m] [MonadLiftT BuildM m] [MonadStore Name (Array ActivePackageTarget) m]
+: RecBuild Package (Array ActivePackageTarget) m := fun pkg buildPkg => do
+  let mut depTargets := #[]
+  for dep in pkg.dependencies do
+    let targets? ← fetch? dep.name.toName
+    let targets ← do
+      if let some targets := targets? then
+        pure targets
+      else
+        let depPkg ← liftM (m := BuildM) <| resolveDep pkg dep
+        buildPkg depPkg
+    depTargets := depTargets ++ targets
+  let pkgTarget ← pkg.buildOleanAndCTargetsWithDepTargets depTargets
+  depTargets.push pkgTarget
 
-def buildPackageTargetList (pkgs : List Package) : BuildM (List ActivePackageTarget) := do
-  failOnBuildCycle <| ← RBTopT.run' <| pkgs.mapM fun pkg =>
-    buildRBTop (cmp := Name.quickCmp) recBuildPkgWithDeps (·.name.toName) pkg
+def buildPackageTargetsWithDeps (pkgs : Array Package) : BuildM (Array ActivePackageTarget) := do
+  failOnBuildCycle <| ← RBTopT.run' <| pkgs.concatMapM fun pkg =>
+    buildRBTop (cmp := Name.quickCmp) recBuildPackageWithDeps (·.name.toName) pkg
 
 def Package.buildTarget (self : Package) : BuildM ActivePackageTarget := do
-  failOnBuildCycle <| ← RBTopT.run' <|
-    buildRBTop (cmp := Name.quickCmp) recBuildPkgWithDeps (·.name.toName) self
+  (← buildPackageTargetsWithDeps #[self]).back
 
-def Package.buildDepTargets (self : Package) : BuildM (List ActivePackageTarget) := do
-  buildPackageTargetList (← solveDeps self)
+def Package.buildDepTargets (self : Package) : BuildM (Array ActivePackageTarget) := do
+  buildPackageTargetsWithDeps (← self.resolveDirectDeps).toArray
 
-def Package.buildDeps (self : Package) : BuildM (List Package) := do
-  let deps ← solveDeps self
-  let targets ← buildPackageTargetList deps
-  targets.forM (discard ·.materialize)
-  return deps
+def Package.buildDeps (self : Package) : BuildM (Array Package) := do
+  let targets ← self.buildDepTargets
+  targets.mapM fun target => Functor.mapConst target.info.1 target.materialize
 
 def configure (pkg : Package) : IO Unit :=
   pkg.buildDeps.run
@@ -140,7 +151,7 @@ def configure (pkg : Package) : IO Unit :=
 def Package.build (self : Package) : BuildM PUnit := do
   let depTargets ← self.buildDepTargets
   let depTarget ← self.buildDepTargetWith depTargets
-  let moreOleanDirs := depTargets.map (·.package.oleanDir)
+  let moreOleanDirs := packageTargetsToOleanDirs depTargets
   let targets ← self.buildOleanTargets moreOleanDirs depTarget
   discard <| ActiveTarget.materializeArray targets
 
@@ -149,22 +160,27 @@ def build (pkg : Package) : IO PUnit :=
 
 -- # Print Paths
 
-def Package.buildModuleOleanTargetsWithDeps
-(deps : List Package) (mods : Array Name) (self : Package)
-: BuildM (Array ActiveFileTarget) := do
-  let moreOleanDirs := deps.map (·.oleanDir)
-  let depTarget ← self.buildDepTargetWith <| ← buildPackageTargetList deps
-  self.buildModuleOleanTargets mods moreOleanDirs depTarget
-
-def Package.buildModuleOleansWithDeps
-(deps : List Package) (mods : Array Name) (self : Package) :=
-  self.buildModuleOleanTargetsWithDeps deps mods >>= (·.forM (discard ·.materialize))
+/-- Pick the local imports of the package from a list of import strings. -/
+def Package.filterLocalImports (imports : List String) (self : Package) : Array Name := do
+  let mut localImports := #[]
+  for imp in imports do
+    let impName := imp.toName
+    if self.isLocalModule impName then
+      localImports := localImports.push impName
+  return localImports
 
 def printPaths (pkg : Package) (imports : List String := []) : IO Unit := do
-  let deps ← solveDeps pkg
-  unless imports.isEmpty do
-    let imports := imports.map (·.toName)
-    let localImports := imports.filter pkg.isLocalModule |>.toArray
-    pkg.buildModuleOleansWithDeps deps localImports |>.run
+  let deps ← BuildM.run' do
+    -- resolve and build deps
+    let depTargets ← pkg.buildDepTargets
+    let depPkgs := depTargets.map (·.package) |>.foldl (flip List.cons) []
+    -- build any additional imports
+    unless imports.isEmpty do
+      let moreOleanDirs := depPkgs.map (·.oleanDir)
+      let depTarget ← pkg.buildDepTargetWith depTargets
+      let localImports := pkg.filterLocalImports imports
+      let oleanTargets ← pkg.buildModuleOleanTargets localImports moreOleanDirs depTarget
+      oleanTargets.forM (discard ·.materialize)
+    pure depPkgs
   IO.println <| SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
   IO.println <| SearchPath.toString <| pkg.srcDir :: deps.map (·.srcDir)

Lake/BuildTop.lean

@@ -19,7 +19,7 @@ def RecBuild.{u,v,w} (i : Type u) (o : Type v) (m : Type v → Type w) :=
   i → (i → m o) → m o
 
 /-- A monad equipped with a key-object store. -/
-class MonadStore (k : Type u) (o : Type v) (m : Type v → Type w) where
+class MonadStore (k : Type u) (o : outParam $ Type v) (m : Type v → Type w) where
   fetch? : k → m (Option o)
   store : k → o → m PUnit
 

Lake/Resolve.lean

@@ -11,8 +11,12 @@ open System
 namespace Lake
 
 open Git in
-def materializeGit
-  (name : String) (dir : FilePath) (url rev : String) (branch : Option String)
+/--
+  Materializes a Git dependency in the given `dir`,
+  cloning and/or updating it as necessary.
+-/
+def materializeGitDep
+(name : String) (dir : FilePath) (url rev : String) (branch : Option String)
 : IO Unit := do
   if ← dir.isDir then
     IO.eprint s!"{name}: trying to update {dir} to revision {rev}"
@@ -26,63 +30,36 @@ def materializeGit
     let hash ← parseOriginRevision rev dir
     checkoutDetach hash dir
 
-def materialize (pkg : Package) (dep : Dependency) : IO FilePath :=
+/--
+  Materializes a dependency relative to the given package,
+  downloading and/or updating it as necessary.
+-/
+def materializeDep (pkg : Package) (dep : Dependency) : IO FilePath :=
   match dep.src with
   | Source.path dir => do
     let depDir := pkg.dir / dir
     depDir
   | Source.git url rev branch => do
     let depDir := pkg.depsDir / dep.name
-    materializeGit dep.name depDir url rev branch
+    materializeGitDep dep.name depDir url rev branch
     depDir
 
-def Assignment := List (String × Package)
-
-namespace Assignment
-
-def empty : Assignment := []
-
-def contains (a : Assignment) (s : String) : Bool :=
-  (a.lookup s).isSome
-
-def insert (a : Assignment) (k : String) (v : Package) : Assignment :=
-  if a.contains k then a else (k, v) :: a
-
-def fold {α} (i : α) (f : α → String → Package → α) : Assignment → α :=
-  List.foldl (fun a ⟨k, v⟩ => f a k v) i
-
-end Assignment
-
-abbrev Solver := StateT Assignment IO
-
-def notYetAssigned (d : String) : Solver Bool := do
-  ¬ (← get).contains d
-
-def resolvedPackage (d : String) : Solver Package := do
-  let some pkg ← pure ((← get).lookup d) | unreachable!
-  pkg
-
-def solveDepsCore (pkg : Package) : (maxDepth : Nat) → Solver Unit
-  | 0 => throw <| IO.userError "maximum dependency resolution depth reached"
-  | maxDepth + 1 => do
-    let newDeps ← pkg.dependencies.filterM (notYetAssigned ·.name)
-    for dep in newDeps do
-      let dir ← materialize pkg dep
-      let pkg ← Package.fromDir (dir / dep.dir) dep.args
-      modify (·.insert dep.name pkg)
-    for dep in newDeps do
-      let depPkg ← resolvedPackage dep.name
-      unless depPkg.name = dep.name do
-        throw <| IO.userError <|
-          s!"{pkg.name} (in {pkg.dir}) depends on {dep.name}, " ++
-          s!"but resolved dependency has name {depPkg.name} (in {depPkg.dir})"
-      solveDepsCore depPkg maxDepth
+/--
+  Resolves a dependency relative to the given package,
+  downloading and/or updating it as necessary.
+-/
+def resolveDep (pkg : Package) (dep : Dependency) : IO Package := do
+  let dir ← materializeDep pkg dep
+  let depPkg ← Package.fromDir (dir / dep.dir) dep.args
+  unless depPkg.name = dep.name do
+    throw <| IO.userError <|
+      s!"{pkg.name} (in {pkg.dir}) depends on {dep.name}, " ++
+      s!"but resolved dependency has name {depPkg.name} (in {depPkg.dir})"
+  return depPkg
 
 /--
-  Resolves the dependency tree for the given package,
-  downloading and/or updating missing dependencies as necessary.
+  Resolves the package's direct dependencies,
+  downloading and/or updating them as necessary.
 -/
-def solveDeps (pkg : Package) : IO (List Package) := do
-  let solver := solveDepsCore pkg 1024
-  let (_, assg) ← solver.run <| Assignment.empty.insert pkg.name pkg
-  assg.reverse.tail!.mapM (·.2)
+def Package.resolveDirectDeps (self : Package) : IO (List Package) :=
+  self.dependencies.mapM (resolveDep self ·)