From 7942b9eaae3b4c57b1069c0107ddca14766e0f43 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Tue, 8 Oct 2024 19:20:05 -0400
Subject: [PATCH] fix: lake: make package `extraDep` intransitive (#5641)

A Lake build of target within a a package will no longer build a
package's dependencies package-level extra targets dependencies. At the
technical level, a package's `extraDep` facet no longer transitively
builds its dependencies' `extraDep` facet.

Closes #5633.
---
 src/lake/Lake/Build/Package.lean           | 7 ++-----
 src/lake/tests/noRelease/Test.lean         | 1 +
 src/lake/tests/noRelease/dep/Dep.lean      | 0
 src/lake/tests/noRelease/dep/lakefile.lean | 2 ++
 src/lake/tests/noRelease/test.sh           | 7 ++++---
 src/lake/tests/online/test.sh              | 3 +++
 6 files changed, 12 insertions(+), 8 deletions(-)
 create mode 100644 src/lake/tests/noRelease/dep/Dep.lean

diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean
index cc79c1f9be..39a1ff261e 100644
--- a/src/lake/Lake/Build/Package.lean
+++ b/src/lake/Lake/Build/Package.lean
@@ -79,15 +79,12 @@ def Package.maybeFetchBuildCacheWithWarning (self : Package) := do
 def Package.fetchOptRelease := @maybeFetchBuildCacheWithWarning
 
 /--
-Build the `extraDepTargets` for the package and its transitive dependencies.
-Also fetch pre-built releases for the package's' dependencies.
+Build the `extraDepTargets` for the package.
+Also, if the package is a dependency, maybe fetch its build cache.
 -/
 def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
   withRegisterJob s!"{self.name}:extraDep" do
   let mut job := BuildJob.nil
-  -- Build dependencies' extra dep targets
-  for dep in self.deps do
-    job := job.mix <| ← dep.extraDep.fetch
   -- Fetch build cache if this package is a dependency
   if self.name ≠ (← getWorkspace).root.name then
     job := job.add <| ← self.maybeFetchBuildCacheWithWarning
diff --git a/src/lake/tests/noRelease/Test.lean b/src/lake/tests/noRelease/Test.lean
index e69de29bb2..f341d235af 100644
--- a/src/lake/tests/noRelease/Test.lean
+++ b/src/lake/tests/noRelease/Test.lean
@@ -0,0 +1 @@
+import Dep
diff --git a/src/lake/tests/noRelease/dep/Dep.lean b/src/lake/tests/noRelease/dep/Dep.lean
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/src/lake/tests/noRelease/dep/lakefile.lean b/src/lake/tests/noRelease/dep/lakefile.lean
index 824a7b876e..ebc2578d29 100644
--- a/src/lake/tests/noRelease/dep/lakefile.lean
+++ b/src/lake/tests/noRelease/dep/lakefile.lean
@@ -5,3 +5,5 @@ package dep where
   preferReleaseBuild := true
   releaseRepo := "https://example.com"
   buildArchive := "release.tgz"
+
+lean_lib Dep
diff --git a/src/lake/tests/noRelease/test.sh b/src/lake/tests/noRelease/test.sh
index 433eff467d..002c7c3ac5 100755
--- a/src/lake/tests/noRelease/test.sh
+++ b/src/lake/tests/noRelease/test.sh
@@ -40,9 +40,10 @@ EOF
 
 # Test that an indirect fetch on the release does not cause the build to fail
 $LAKE build Test | diff -u --strip-trailing-cr <(cat << EOF
-⚠ [2/5] Ran dep:extraDep
+⚠ [3/6] Ran dep:extraDep
 warning: building from source; failed to fetch GitHub release (run with '-v' for details)
-✔ [4/5] Built Test
+✔ [4/6] Built Dep
+✔ [5/6] Built Test
 Build completed successfully.
 EOF
 ) -
@@ -56,7 +57,7 @@ mkdir -p .lake/packages/dep/.lake/build
 $LAKE -d .lake/packages/dep pack 2>&1 | grep --color "packing"
 test -f .lake/packages/dep/.lake/release.tgz
 echo 4225503363911572621 > .lake/packages/dep/.lake/release.tgz.trace
-rmdir .lake/packages/dep/.lake/build
+rm -rf .lake/packages/dep/.lake/build
 $LAKE build dep:release -v | grep --color "tar"
 test -d .lake/packages/dep/.lake/build
 
diff --git a/src/lake/tests/online/test.sh b/src/lake/tests/online/test.sh
index fad35121dd..0b54313672 100755
--- a/src/lake/tests/online/test.sh
+++ b/src/lake/tests/online/test.sh
@@ -18,6 +18,9 @@ $LAKE -v -f git.toml build @Cli:extraDep |
 
 ./clean.sh
 $LAKE -f barrel.lean update
+# Test that a barrel is not fetched for an unbuilt dependency
+$LAKE -v -f barrel.lean build @test:extraDep |
+  grep --color "Cli:optBarrel" && exit 1 || true
 # Test that barrels are not fetched after the build directory is created.
 mkdir -p .lake/packages/Cli/.lake/build
 ($LAKE -v -f barrel.lean build @Cli:extraDep) |