diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index fb2f49887e..f7ff0174c6 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/src/lake/Lake/Build/Package.lean @@ -50,7 +50,7 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet := /-- Download and unpack the package's prebuilt release archive (from GitHub). -/ def Package.fetchRelease (self : Package) : SpawnM (BuildJob Unit) := - withRegisterJob "Fetching {self.name} cloud release" <| Job.async do + withRegisterJob s!"Fetching {self.name} cloud release" <| Job.async do let repo := GitRepo.mk self.dir let repoUrl? := self.releaseRepo? <|> self.remoteUrl? let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?) diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean index 0c80c07dc9..a795bf2817 100644 --- a/src/lake/Lake/Build/Run.lean +++ b/src/lake/Lake/Build/Run.lean @@ -48,7 +48,8 @@ def Workspace.runFetchM let failLv : LogLevel := if ctx.failIfWarnings then .warning else .error let failed := log.any (·.level ≥ failLv) if !failed && io.isEmpty && !log.hasVisibleEntries verbosity then - if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n" + if showProgress then + if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n" else unless showProgress do out.putStr header @@ -72,7 +73,8 @@ def Workspace.runFetchM let failed := log.any (·.level ≥ failLv) if failed then modify (·.push caption) if !(failed || log.hasVisibleEntries verbosity) then - if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n" + if showProgress then + if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n" else unless showProgress do out.putStr header diff --git a/src/lake/examples/hello/test.sh b/src/lake/examples/hello/test.sh index b75faaa375..b086e2f6e4 100755 --- a/src/lake/examples/hello/test.sh +++ b/src/lake/examples/hello/test.sh @@ -8,6 +8,9 @@ $LAKE exe hello $LAKE exe hello Bob Bill .lake/build/bin/hello +# Tests that quiet mode (-q) produces no output on no-op build +$LAKE -q build hello 2>&1 | diff - /dev/null + # Tests that build produces a manifest if there is none. # Related: https://github.com/leanprover/lean4/issues/2549 test -f lake-manifest.json