From bd45c0cd047acb8133aee01e40af5fd75d17c9ff Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Tue, 18 Jun 2024 22:49:59 -0400
Subject: [PATCH] fix: lake: visit direct deps before adding manifest entries
 (#4485)

Fixes a bug in #4371 where the version of a package used by a dependency
would take precedence over that of a the same package as a direct
dependency if that package had a a manifest. This was because the direct
dependency's manifest entries were added before all the direct
dependencies were visited.
---
 src/lake/Lake/Load/Resolve.lean | 48 ++++++++++++++++++---------------
 src/lake/tests/order/test.sh    |  6 +++++
 2 files changed, 32 insertions(+), 22 deletions(-)

diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean
index 921549875a..5bcd3eb610 100644
--- a/src/lake/Lake/Load/Resolve.lean
+++ b/src/lake/Lake/Load/Resolve.lean
@@ -57,9 +57,9 @@ instance [Monad m] [MonadError m] : MonadCycleOf Name (ResolveT m) where
 
 /--
 Recursively visits the workspace dependency graph, starting from `root`.
-At each package, performs `f` to resolve the dependencies of a package,
-recurses, then adds the package to workspace's package set.
-Errors if a cycle is encountered.
+At each package, loops through each direct dependency performing just `breath`.
+Them, loops again through the results applying `depth`, recursing, and adding
+the package to workspace's package set. Errors if a cycle is encountered.
 
 **Traversal Order**
 
@@ -87,12 +87,13 @@ the order `R`, `A`, `B`, `X`, `Y`, `C`. If `X` and `C` are both the package
 `foo`, Lake would use the configuration of `foo` found in `B` rather than in
 the root `R`, which would likely confuse the user.
 -/
-@[inline] def Workspace.resolveDeps
+@[specialize] def Workspace.resolveDeps
   [Monad m] [MonadError m] (ws : Workspace)
-  (f : Package → Dependency → ResolveT m Package)
+  (breadth : Package → Dependency → ResolveT m Package)
+  (depth : Package → m PUnit := fun _ => pure ())
 : m Workspace := do
   let (root, ws) ← ResolveT.run ws <| StateT.run' (s := {}) <|
-    recFetchAcyclic (·.name) go ws.root
+    inline <| recFetchAcyclic (·.name) go ws.root
   return {ws with root}
 where
   @[specialize] go pkg resolve : StateT (NameMap Package) (ResolveT m) Package := do
@@ -103,12 +104,13 @@ where
         return -- already resolved in another branch
       if pkg.name = dep.name then
         error s!"{pkg.name}: package requires itself (or a package with the same name)"
-      let dep ← f pkg dep -- package w/o dependencies
-      store dep.name dep
+      let pre ← breadth pkg dep -- package w/o dependencies
+      store dep.name pre
     let deps ← pkg.depConfigs.mapM fun dep => do
-      if let some dep ← fetch? dep.name then
+      if let some pre ← fetch? dep.name then
         modifyThe (NameMap Package) (·.erase dep.name) -- for `dep` linearity
-        return OpaquePackage.mk (← resolve dep)
+        depth pre
+        return OpaquePackage.mk (← resolve pre)
       if let some dep ← findPackage? dep.name then
         return OpaquePackage.mk dep -- already resolved in another branch
       error s!"{dep.name}: impossible resolution state reached"
@@ -171,6 +173,19 @@ def reuseManifest (ws : Workspace) (toUpdate : NameSet) : UpdateT LogIO PUnit :=
       liftM (m := IO) <| throw e -- only ignore manifest on a bare `lake update`
     logWarning s!"{rootName}: ignoring previous manifest because it failed to load: {e}"
 
+/-- Add a package dependency's manifest entries to the update state. -/
+def addDependencyEntries (pkg : Package) : UpdateT LogIO PUnit := do
+  match (← Manifest.load pkg.manifestFile |>.toBaseIO) with
+  | .ok manifest =>
+    manifest.packages.forM fun entry => do
+      unless (← getThe (NameMap PackageEntry)).contains entry.name do
+        let entry := entry.setInherited.inDirectory pkg.relDir
+        store entry.name entry
+  | .error (.noFileOrDirectory ..) =>
+    logWarning s!"{pkg.name}: ignoring missing manifest '{pkg.manifestFile}'"
+  | .error e =>
+    logWarning s!"{pkg.name}: ignoring manifest because it failed to load: {e}"
+
 /-- Update a single dependency. -/
 def updateDep
   (pkg : Package) (dep : Dependency) (leanOpts : Options := {})
@@ -199,17 +214,6 @@ def updateDep
       logError s!"'{dep.name}' was downloaded incorrectly; \
         you will need to manually delete '{depPkg.dir}': {e}"
     error s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
-  -- Add the dependencies' locked dependencies to the manifest
-  match (← Manifest.load depPkg.manifestFile |>.toBaseIO) with
-  | .ok manifest =>
-    manifest.packages.forM fun entry => do
-      unless (← getThe (NameMap PackageEntry)).contains entry.name do
-        let entry := entry.setInherited.inDirectory depPkg.relDir
-        store entry.name entry
-  | .error (.noFileOrDirectory ..) =>
-    logWarning s!"{depPkg.name}: ignoring missing dependency manifest '{depPkg.manifestFile}'"
-  | .error e =>
-    logWarning s!"{depPkg.name}: ignoring dependency manifest because it failed to load: {e}"
   return depPkg
 
 /--
@@ -227,7 +231,7 @@ def Workspace.updateAndMaterialize
 : LogIO Workspace := do
   let (ws, entries) ← UpdateT.run do
     reuseManifest ws toUpdate
-    ws.resolveDeps fun pkg dep => updateDep pkg dep leanOpts
+    ws.resolveDeps (updateDep · · leanOpts) (addDependencyEntries ·)
   let manifestEntries := ws.packages.foldl (init := #[]) fun arr pkg =>
     match entries.find? pkg.name with
     | some entry => arr.push <|
diff --git a/src/lake/tests/order/test.sh b/src/lake/tests/order/test.sh
index 9f94ecf765..f69f93e994 100755
--- a/src/lake/tests/order/test.sh
+++ b/src/lake/tests/order/test.sh
@@ -26,3 +26,9 @@ $LAKE exe Y | grep --color root
 cp lake-manifest.json lake-manifest-1.json
 $LAKE update foo
 diff --strip-trailing-cr lake-manifest-1.json lake-manifest.json
+
+# Tests that order does not change in the presence of dep manifests
+$LAKE -d foo update
+$LAKE -d bar update
+$LAKE update
+diff --strip-trailing-cr lake-manifest-1.json lake-manifest.json