refactor: reduce Reservoir build fetch attempts & warnings (#5600)

Lake no longer attempts to fetch the Reservoir build cache if the build
directory is already present. Plus, failure of the automatic fetch now
only produces a trace message, not a warning.

src/lake/Lake/Build/Package.lean

@@ -44,7 +44,9 @@ def Package.maybeFetchBuildCache (self : Package) : FetchM (BuildJob Bool) := do
   let shouldFetch :=
     (← getTryCache) &&
     (self.preferReleaseBuild || -- GitHub release
-      (!self.scope.isEmpty && !(← getElanToolchain).isEmpty)) -- Reservoir
+      !(self.scope.isEmpty -- no Reservoir
+        || (← getElanToolchain).isEmpty
+        || (← self.buildDir.pathExists)))
   if shouldFetch then
     self.optBuildCache.fetch
   else
@@ -65,9 +67,12 @@ def Package.maybeFetchBuildCacheWithWarning (self : Package) := do
   let job ← self.maybeFetchBuildCache
   job.bindSync fun success t => do
     unless success do
-      let details ← self.optFacetDetails <| if self.preferReleaseBuild then
-          optGitHubReleaseFacet else optReservoirBarrelFacet
-      logWarning s!"building from source; failed to fetch cloud build{details}"
+      if self.preferReleaseBuild then
+        let details ← self.optFacetDetails optGitHubReleaseFacet
+        logWarning s!"building from source; failed to fetch GitHub release{details}"
+      else
+        let details ← self.optFacetDetails optReservoirBarrelFacet
+        logVerbose s!"building from source; failed to fetch Reservoir build{details}"
     return ((), t)
 
 @[deprecated maybeFetchBuildCacheWithWarning (since := "2024-09-27")]
@@ -173,7 +178,7 @@ def Package.optBarrelFacetConfig : PackageFacetConfig optReservoirBarrelFacet :=
 
 /-- The `PackageFacetConfig` for the builtin `reservoirBarrelFacet`. -/
 def Package.barrelFacetConfig : PackageFacetConfig reservoirBarrelFacet :=
-  mkBuildArchiveFacetConfig optReservoirBarrelFacet "Reservoir barrel"
+  mkBuildArchiveFacetConfig optReservoirBarrelFacet "Reservoir build"
 
 /-- The `PackageFacetConfig` for the builtin `optGitHubReleaseFacet`. -/
 def Package.optGitHubReleaseFacetConfig : PackageFacetConfig optGitHubReleaseFacet :=

src/lake/tests/noRelease/test.sh

@@ -41,7 +41,7 @@ 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
-warning: building from source; failed to fetch cloud build (run with '-v' for details)
+warning: building from source; failed to fetch GitHub release (run with '-v' for details)
 ✔ [4/5] Built Test
 Build completed successfully.
 EOF

src/lake/tests/online/test.sh

@@ -18,7 +18,12 @@ $LAKE -v -f git.toml build @Cli:extraDep |
 
 ./clean.sh
 $LAKE -f barrel.lean update
-# Test that narrels are not fetched without a toolchain
+# 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) |
+  grep --color "Cli:optBarrel" && exit 1 || true
+rmdir .lake/packages/Cli/.lake/build
+# Test that barrels are not fetched without a toolchain
 (ELAN_TOOLCHAIN= $LAKE -v -f barrel.lean build @Cli:extraDep) |
   grep --color "Cli:optBarrel" && exit 1 || true
 ($LAKE -v -f barrel.lean build @Cli:barrel && exit 1 || true) |
@@ -28,8 +33,6 @@ $LAKE -v -f barrel.lean build @Cli:extraDep |
   grep --color "Cli:optBarrel"
 $LAKE -f barrel.lean build @Cli:extraDep |
   grep --color "Cli:optBarrel" && exit 1 || true
-$LAKE -f barrel.lean build @Cli:extraDep |
-  grep --color "(run with '-v' for details)"
 # Test cache toggle
 (LAKE_NO_CACHE=1 $LAKE -v -f barrel.lean build @Cli:extraDep) |
   grep --color "Cli:optBarrel" && exit 1 || true