feat: lake: selective build cache fetch & display (#5572)

Lake no longer attempts to fetch Reservoir build caches (barrels) for
non-Reservoir dependencies, and it will only fetch them for Reservoir
dependencies in the presence of a known toolchain.

Also, optional build job failures are now only displayed in verbose
mode.

src/lake/Lake/Build/Package.lean

@@ -41,10 +41,21 @@ def Package.optBuildCacheFacetConfig : PackageFacetConfig optBuildCacheFacet :=
 
 /-- Tries to download the package's build cache (if configured). -/
 def Package.maybeFetchBuildCache (self : Package) : FetchM (BuildJob Bool) := do
-  if (← getNoCache) then
+  let shouldFetch :=
+    (← getTryCache) &&
+    (self.preferReleaseBuild || -- GitHub release
+      (!self.scope.isEmpty && !(← getElanToolchain).isEmpty)) -- Reservoir
+  if shouldFetch then
+    self.optBuildCache.fetch
+  else
     return pure true
+
+@[inline]
+private def Package.optFacetDetails (self : Package) (facet : Name) : JobM String := do
+  if (← getIsVerbose) then
+    return s!" (see '{self.name}:{facet}' for details)"
   else
-    self.optBuildCache.fetch
+    return " (run with '-v' for details)"
 
 /--
 Tries to download and unpack the package's cached build archive
@@ -54,10 +65,9 @@ def Package.maybeFetchBuildCacheWithWarning (self : Package) := do
   let job ← self.maybeFetchBuildCache
   job.bindSync fun success t => do
     unless success do
-      let facet := if self.preferReleaseBuild then
-        optGitHubReleaseFacet else optReservoirBarrelFacet
-      logWarning s!"building from source; \
-        failed to fetch cloud release (see '{self.name}:{facet}' for details)"
+      let details ← self.optFacetDetails <| if self.preferReleaseBuild then
+          optGitHubReleaseFacet else optReservoirBarrelFacet
+      logWarning s!"building from source; failed to fetch cloud build{details}"
     return ((), t)
 
 @[deprecated maybeFetchBuildCacheWithWarning (since := "2024-09-27")]
@@ -150,7 +160,7 @@ private def Package.mkBuildArchiveFacetConfig
     withRegisterJob s!"{pkg.name}:{facet}" do
       (← fetch <| pkg.facet optFacet).bindSync fun success t => do
         unless success do
-          error s!"failed to fetch {what} (see '{pkg.name}:{optFacet}' for details)"
+          error s!"failed to fetch {what}{← pkg.optFacetDetails optFacet}"
         return ((), t)
 
 /-- The `PackageFacetConfig` for the builtin `buildCacheFacet`. -/

src/lake/Lake/Build/Run.lean

@@ -36,6 +36,7 @@ structure MonitorContext where
   outLv : LogLevel
   failLv : LogLevel
   minAction : JobAction
+  showOptional : Bool
   useAnsi : Bool
   showProgress : Bool
   /-- How often to poll jobs (in milliseconds). -/
@@ -98,15 +99,18 @@ def renderProgress (running unfinished : Array OpaqueJob) (h : 0 < unfinished.si
 
 def reportJob (job : OpaqueJob) : MonitorM PUnit := do
   let {jobNo, ..} ← get
-  let {totalJobs, failLv, outLv, out, useAnsi, showProgress, minAction, ..} ← read
+  let {totalJobs, failLv, outLv, showOptional, out, useAnsi, showProgress, minAction, ..} ← read
   let {task, caption, optional} := job.toJob
   let {log, action, ..} := task.get.state
   let maxLv := log.maxLv
   let failed := log.hasEntries ∧ maxLv ≥ failLv
   if failed ∧ ¬optional then
     modify fun s => {s with failures := s.failures.push caption}
   let hasOutput := failed ∨ (log.hasEntries ∧ maxLv ≥ outLv)
-  if hasOutput ∨ (showProgress ∧ ¬ useAnsi ∧ action ≥ minAction) then
+  let showJob :=
+    (¬ optional ∨ showOptional) ∧
+    (hasOutput ∨ (showProgress ∧ ¬ useAnsi ∧ action ≥ minAction))
+  if showJob then
     let verb := action.verb failed
     let icon := if hasOutput then maxLv.icon else '✔'
     let opt := if optional then " (Optional)" else ""
@@ -167,14 +171,14 @@ def monitorJobs
   (out : IO.FS.Stream)
   (failLv outLv : LogLevel)
   (minAction : JobAction)
-  (useAnsi showProgress : Bool)
+  (showOptional useAnsi showProgress : Bool)
   (resetCtrl : String := "")
   (initFailures : Array String := #[])
   (totalJobs := jobs.size)
   (updateFrequency := 100)
 : BaseIO (Array String) := do
   let ctx := {
-    totalJobs, out, failLv, outLv, minAction
+    totalJobs, out, failLv, outLv, minAction, showOptional
     useAnsi, showProgress, updateFrequency
   }
   let s := {
@@ -228,7 +232,8 @@ def Workspace.runFetchM
   let jobs ← ctx.registeredJobs.get
   let resetCtrl := if showAnsiProgress then Ansi.resetLine else ""
   let minAction := if cfg.verbosity = .verbose then .unknown else .fetch
-  let failures ← monitorJobs jobs out failLv outLv minAction useAnsi showProgress
+  let showOptional := cfg.verbosity = .verbose
+  let failures ← monitorJobs jobs out failLv outLv minAction showOptional useAnsi showProgress
     (resetCtrl := resetCtrl) (initFailures := failures)
   -- Failure Report
   if failures.isEmpty then

src/lake/Lake/Config/Monad.lean

@@ -128,10 +128,14 @@ variable [MonadLakeEnv m]
 
 variable [Functor m]
 
-/-- Get the `LAKE_NO_CACHE`/`--no-cache` LAke configuration. -/
+/-- Get the `LAKE_NO_CACHE`/`--no-cache` Lake configuration. -/
 @[inline] def getNoCache [Functor m] [MonadBuild m] : m Bool :=
   (·.noCache) <$> getLakeEnv
 
+/-- Get whether the `LAKE_NO_CACHE`/`--no-cache` Lake configuration is **NOT** set. -/
+@[inline] def getTryCache [Functor m] [MonadBuild m] : m Bool :=
+  (!·.noCache) <$> getLakeEnv
+
 /-- Get the `LAKE_PACKAGE_URL_MAP` for the Lake environment. Empty if none. -/
 @[inline] def getPkgUrlMap : m (NameMap String) :=
   (·.pkgUrlMap) <$> getLakeEnv

src/lake/tests/noRelease/test.sh

@@ -30,31 +30,26 @@ $LAKE update
 git -C .lake/packages/dep tag -d release
 
 # Test that a direct invocation fo `lake build *:release` fails
-REV_STR="'${INIT_REV}'"
 ($LAKE build dep:release && exit 1 || true) | diff -u --strip-trailing-cr <(cat << EOF
-✖ [1/2] (Optional) Fetching dep:optRelease
-error: no release tag found for revision ${REV_STR}
 ✖ [2/2] Running dep:release
-error: failed to fetch GitHub release (see 'dep:optRelease' for details)
+error: failed to fetch GitHub release (run with '-v' for details)
 Some required builds logged failures:
 - dep:release
 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
-✖ [1/5] (Optional) Fetching dep:optRelease
-error: no release tag found for revision ${REV_STR}
 ⚠ [2/5] Ran dep:extraDep
-warning: building from source; failed to fetch cloud release (see 'dep:optRelease' for details)
+warning: building from source; failed to fetch cloud build (run with '-v' for details)
 ✔ [4/5] Built Test
 Build completed successfully.
 EOF
 ) -
 
 # Test download failure
 $LAKE update # re-fetch release tag
-($LAKE  build dep:release && exit 1 || true) | grep --color "curl"
+($LAKE -v build dep:release && exit 1 || true) | grep --color "curl"
 
 # Test automatic cloud release unpacking
 mkdir -p .lake/packages/dep/.lake/build

src/lake/tests/online/git.toml

@@ -0,0 +1,6 @@
+name = "test"
+
+[[require]]
+name = "Cli"
+git = "https://github.com/leanprover/lean4-cli"
+rev = "main"

src/lake/tests/online/test.sh

@@ -3,30 +3,49 @@ set -exo pipefail
 
 LAKE=${LAKE:-../../.lake/build/bin/lake}
 
+export ELAN_TOOLCHAIN=test
+
+./clean.sh
+# Tests requiring a package not in the index
+($LAKE -f bogus-dep.toml update 2>&1 && exit 1 || true) |
+  grep --color "error: bogus/bogus: could not materialize package: dependency has no explicit source and was not found on Reservoir"
+
+./clean.sh
+$LAKE -f git.toml update
+# Test that barrels are not fetched for non-Reservoir dependencies
+$LAKE -v -f git.toml build @Cli:extraDep |
+  grep --color "Cli:optBarrel" && exit 1 || true
+
 ./clean.sh
 $LAKE -f barrel.lean update
+# Test that narrels 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) |
+  grep --color "toolchain=test"
+# Test that fetch failures are only shown in verbose mode
+$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 -f barrel.lean build @Cli:extraDep | grep --color "Cli:optBarrel"
-(LAKE_NO_CACHE=1 $LAKE -f barrel.lean build @Cli:extraDep) |
+(LAKE_NO_CACHE=1 $LAKE -v -f barrel.lean build @Cli:extraDep) |
   grep --color "Cli:optBarrel" && exit 1 || true
-($LAKE -f barrel.lean build @Cli:extraDep --no-cache) |
+($LAKE -v -f barrel.lean build @Cli:extraDep --no-cache) |
   grep --color "Cli:optBarrel" && exit 1 || true
-(LAKE_NO_CACHE=1 $LAKE -f barrel.lean build @Cli:extraDep --try-cache) |
+(LAKE_NO_CACHE=1 $LAKE -v -f barrel.lean build @Cli:extraDep --try-cache) |
   grep --color "Cli:optBarrel"
 # Test barrel download
-(ELAN_TOOLCHAIN= $LAKE -f barrel.lean build @Cli:barrel -v && exit 1 || true) |
+(ELAN_TOOLCHAIN= $LAKE -v -f barrel.lean build @Cli:barrel && exit 1 || true) |
   grep --color "Lean toolchain not known"
 ELAN_TOOLCHAIN=leanprover/lean4:v4.11.0 \
-  $LAKE -f barrel.lean build @Cli:barrel -v
+  $LAKE -v -f barrel.lean build @Cli:barrel
 ELAN_TOOLCHAIN=leanprover/lean4:v4.11.0 \
 LEAN_GITHASH=ec3042d94bd11a42430f9e14d39e26b1f880f99b \
   $LAKE -f barrel.lean build Cli --no-build
 
-./clean.sh
-# Tests requiring a package not in the index
-($LAKE -f bogus-dep.toml update 2>&1 && exit 1 || true) |
-  grep --color "error: bogus/bogus: could not materialize package: dependency has no explicit source and was not found on Reservoir"
-
 ./clean.sh
 $LAKE -f require.lean update -v
 test -d .lake/packages/doc-gen4