diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index cc79c1f9be20..39a1ff261e64 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 e69de29bb2d1..f341d235af05 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 000000000000..e69de29bb2d1 diff --git a/src/lake/tests/noRelease/dep/lakefile.lean b/src/lake/tests/noRelease/dep/lakefile.lean index 824a7b876e81..ebc2578d29a8 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 433eff467d43..002c7c3ac59b 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 fad35121dda9..0b54313672a6 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) |