From 3d76e48181beaf7360a5cd8ff7982865d6d5b298 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sat, 2 Oct 2021 16:11:53 -0400
Subject: [PATCH] fix: do not build deep deps multiple times

---
 Lake/BuildPackage.lean   | 34 ++++++++++++++++++++--------------
 Lake/BuildTop.lean       | 36 +++++++++++++++++++++++++++---------
 examples/deps/package.sh | 11 +++++------
 3 files changed, 52 insertions(+), 29 deletions(-)

diff --git a/Lake/BuildPackage.lean b/Lake/BuildPackage.lean
index f01e88c600..b351adbc67 100644
--- a/Lake/BuildPackage.lean
+++ b/Lake/BuildPackage.lean
@@ -39,7 +39,7 @@ def Package.buildModuleOleanAndCTargetDAG
 (self : Package) : BuildM (Array ActiveOleanAndCTarget × OleanAndCTargetMap) := do
   let buildMod : OleanAndCTargetBuild :=
     self.recBuildModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget
-  let (resE, map) ← mods.mapM (buildRBTop buildMod id) |>.run {}
+  let (resE, map) ← mods.mapM (buildRBTop buildMod id) |>.run
   (← failOnBuildCycle resE, map)
 
 def Package.buildModuleOleanTargetDAG
@@ -47,7 +47,7 @@ def Package.buildModuleOleanTargetDAG
 (self : Package) : BuildM (Array ActiveFileTarget × OleanTargetMap) := do
   let buildMod : OleanTargetBuild :=
     self.recBuildModuleOleanTargetWithLocalImports moreOleanDirs depTarget
-  let (resE, map) ← mods.mapM (buildRBTop buildMod id) |>.run {}
+  let (resE, map) ← RBTopT.run <| mods.mapM (buildRBTop buildMod id)
   (← failOnBuildCycle resE, map)
 
 def Package.buildOleanAndCTargetDAG
@@ -65,14 +65,14 @@ def Package.buildModuleOleanAndCTargets
 (self : Package) : BuildM (Array ActiveOleanAndCTarget) := do
   let buildMod : OleanAndCTargetBuild :=
     self.recBuildModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget
-  failOnBuildCycle <| ← mods.mapM (buildRBTop buildMod id) |>.run' {}
+  failOnBuildCycle <| ← RBTopT.run' <| mods.mapM <| buildRBTop buildMod id
 
 def Package.buildModuleOleanTargets
 (mods : Array Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
 (self : Package) : BuildM (Array ActiveFileTarget) := do
   let buildMod : OleanTargetBuild :=
     self.recBuildModuleOleanTargetWithLocalImports moreOleanDirs depTarget
-  failOnBuildCycle <| ← mods.mapM (buildRBTop buildMod id) |>.run' {}
+  failOnBuildCycle <| ← RBTopT.run' <| mods.mapM <| buildRBTop buildMod id
 
 def Package.buildOleanAndCTargets
 (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
@@ -111,20 +111,26 @@ 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.
 -/
-partial def Package.buildTarget (self : Package) : BuildM ActivePackageTarget := do
-  let deps ← solveDeps self
-  -- build dependencies recursively
-  -- TODO: share build of common dependencies
-  let depTargets ← deps.mapM (·.buildTarget)
-  self.buildOleanAndCTargetsWithDepTargets depTargets
+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 buildPackageTargetList (pkgs : List Package) : BuildM (List ActivePackageTarget) := do
+  failOnBuildCycle <| ← RBTopT.run' <| pkgs.mapM fun pkg =>
+    buildRBTop (cmp := Name.quickCmp) recBuildPkgWithDeps (·.name.toName) pkg
+
+def Package.buildTarget (self : Package) : BuildM ActivePackageTarget := do
+  failOnBuildCycle <| ← RBTopT.run' <|
+    buildRBTop (cmp := Name.quickCmp) recBuildPkgWithDeps (·.name.toName) self
 
 def Package.buildDepTargets (self : Package) : BuildM (List ActivePackageTarget) := do
-  let deps ← solveDeps self
-  deps.mapM (·.buildTarget)
+  buildPackageTargetList (← solveDeps self)
 
 def Package.buildDeps (self : Package) : BuildM (List Package) := do
   let deps ← solveDeps self
-  let targets ← deps.mapM (·.buildTarget)
+  let targets ← buildPackageTargetList deps
   targets.forM (discard ·.materialize)
   return deps
 
@@ -147,7 +153,7 @@ def Package.buildModuleOleanTargetsWithDeps
 (deps : List Package) (mods : Array Name) (self : Package)
 : BuildM (Array ActiveFileTarget) := do
   let moreOleanDirs := deps.map (·.oleanDir)
-  let depTarget ← self.buildDepTargetWith <| ← deps.mapM (·.buildTarget)
+  let depTarget ← self.buildDepTargetWith <| ← buildPackageTargetList deps
   self.buildModuleOleanTargets mods moreOleanDirs depTarget
 
 def Package.buildModuleOleansWithDeps
diff --git a/Lake/BuildTop.lean b/Lake/BuildTop.lean
index d0b4e025dd..0520e0c25e 100644
--- a/Lake/BuildTop.lean
+++ b/Lake/BuildTop.lean
@@ -50,6 +50,8 @@ partial def buildTopCore [BEq k] [Inhabited o] [Monad m] [MonadStore k o m]
 /--
   Recursively fills a `MonadStore` of key-object pairs by
   building objects topologically (i.e., via a depth-first search with memoization).
+  If a cycle is detected, the list of keys traversed is thrown.
+
   Called a suspending scheduler in "Build systems à la carte".
 -/
 def buildTop [BEq k] [Inhabited o] [Monad m] [MonadStore k o m]
@@ -61,30 +63,46 @@ def buildTop [BEq k] [Inhabited o] [Monad m] [MonadStore k o m]
 --------------------------------------------------------------------------------
 
 /-- A exception plus state monad transformer (i.e., `ExceptT` + `StateT`). -/
-abbrev EStateT (ε σ m) :=
+abbrev EStateT.{u,v} (ε : Type u) (σ : Type u) (m : Type u → Type v) :=
   ExceptT ε <| StateT σ m
 
-def EStateT.run (state : σ) (self : EStateT ε σ m α) : m (Except ε α × σ) :=
+namespace EStateT
+variable {ε : Type u} {σ : Type u} {m : Type u → Type v}
+
+def run (state : σ) (self : EStateT ε σ m α) : m (Except ε α × σ) :=
   ExceptT.run self |>.run state
 
-def EStateT.run' [Monad m] (state : σ) (self : EStateT ε σ m α) : m (Except ε α) :=
+def run' [Monad m] (state : σ) (self : EStateT ε σ m α) : m (Except ε α) :=
   ExceptT.run self |>.run' state
 
+end EStateT
+
 /-- A transformer that adds an `RBMap` store to a monad. -/
-abbrev RBMapT.{u,v} (k : Type u) (o : Type u) (cmp) (m : Type u → Type v) :=
+abbrev RBMapT.{u,v} (k : Type u) (o : Type u) (cmp : k → k → Ordering) (m : Type u → Type v) :=
   StateT (RBMap k o cmp) m
 
 instance (cmp) [Monad m] : MonadStore k o (RBMapT k o cmp m) where
   fetch? key := do (← get).find? key
   store key obj := modify (·.insert key obj)
 
-/--
-  Monad transformer for an RBMap-based topological walk.
-  If a cycle is detected, the list of keys traversed is thrown.
--/
-abbrev RBTopT.{u,v} (k : Type u) (o : Type u) (cmp) (m : Type u → Type v) :=
+/-- Monad transformer for an `RBMap`-based topological walk. -/
+abbrev RBTopT.{u,v} (k : Type u) (o : Type u) (cmp : k → k → Ordering) (m : Type u → Type v) :=
   EStateT (List k) (RBMap k o cmp) m
 
+namespace RBTopT
+variable {k : Type u} {o : Type u} {cmp : k → k → Ordering} {m : Type u → Type v}
+
+def runWith [Monad m] (map : RBMap.{u,u} k o cmp) (self : RBTopT k o cmp m α) :=
+  EStateT.run map self
+
+def run [Monad m] (self : RBTopT k o cmp m α) :=
+  self.runWith {}
+
+def run' [Monad m] (self : RBTopT k o cmp m α) :=
+  Functor.map (·.1) self.run
+
+end RBTopT
+
 /-- The `RBMap` version of `buildTop`. -/
 def buildRBTop {k o} {cmp} {m} [BEq k] [Inhabited o] [Monad m]
 (build : RecBuild i o (RBTopT k o cmp m)) (keyOf : i → k) (info : i) : RBTopT k o cmp m o :=
diff --git a/examples/deps/package.sh b/examples/deps/package.sh
index c0edb02a31..888f097638 100755
--- a/examples/deps/package.sh
+++ b/examples/deps/package.sh
@@ -1,11 +1,10 @@
 set -ex
 
-# TODO: flip and fix example (deep deps are currently broken)
-
-cd foo
-${LAKE:-../../../build/bin/lake} build-bin
-cd ..
-
 cd bar
 ${LAKE:-../../../build/bin/lake} build-bin
 cd ..
+
+
+cd foo
+${LAKE:-../../../build/bin/lake} build-bin
+cd ..