diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index da268d950e60..53a0f82fbc6b 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/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`. -/ diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean index 2f7e0e63ca21..6ca3671a9b48 100644 --- a/src/lake/Lake/Build/Run.lean +++ b/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,7 +99,7 @@ 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 @@ -106,7 +107,10 @@ def reportJob (job : OpaqueJob) : MonitorM PUnit := do 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 diff --git a/src/lake/Lake/Config/Monad.lean b/src/lake/Lake/Config/Monad.lean index ab5154db55b7..7baed06838e5 100644 --- a/src/lake/Lake/Config/Monad.lean +++ b/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 diff --git a/src/lake/tests/noRelease/test.sh b/src/lake/tests/noRelease/test.sh index 26b361740b9d..d2a5c0c51852 100755 --- a/src/lake/tests/noRelease/test.sh +++ b/src/lake/tests/noRelease/test.sh @@ -30,12 +30,9 @@ $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 @@ -43,10 +40,8 @@ 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 @@ -54,7 +49,7 @@ 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 diff --git a/src/lake/tests/online/git.toml b/src/lake/tests/online/git.toml new file mode 100644 index 000000000000..2891ab196b34 --- /dev/null +++ b/src/lake/tests/online/git.toml @@ -0,0 +1,6 @@ +name = "test" + +[[require]] +name = "Cli" +git = "https://github.com/leanprover/lean4-cli" +rev = "main" diff --git a/src/lake/tests/online/test.sh b/src/lake/tests/online/test.sh index b1b94f3a5b73..f8eab62c51b2 100755 --- a/src/lake/tests/online/test.sh +++ b/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