chore: lake: cloud release build output fixes & related touchups (#4220)

Fixes two output bugs with cloud releases: (1) the fetch as part of an
`extraDep` was not properly isolated in a job, and (2) the release job
would be shown even if the release had already been successfully
fetched.

Also includes some related touchups, including the addition of show all
jobs on `-v` which helps with debugging job counts.

(cherry picked from commit 6171070)

src/lake/Lake/Build/Actions.lean

@@ -115,7 +115,7 @@ def download  (url : String) (file : FilePath) : LogIO PUnit := do
     createParentDirs file
   proc (quiet := true) {
     cmd := "curl"
-    args := #["-f", "-o", file.toString, "-L", url]
+    args := #["-s", "-S", "-f", "-o", file.toString, "-L", url]
   }
 
 /-- Unpack an archive `file` using `tar` into the directory `dir`. -/

src/lake/Lake/Build/Common.lean

@@ -71,8 +71,9 @@ of the `traceFile`. If rebuilt, save the new `depTrace` to the `tracefile`.
 @[inline] def buildUnlessUpToDate
   [CheckExists ι] [GetMTime ι] (info : ι)
   (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
+  (action : JobAction := .build) (oldTrace := depTrace)
 : JobM PUnit := do
-  discard <| buildUnlessUpToDate? info depTrace traceFile build
+  discard <| buildUnlessUpToDate? info depTrace traceFile build action oldTrace
 
 /-- Fetch the trace of a file that may have its hash already cached in a `.hash` file. -/
 def fetchFileTrace (file : FilePath) : JobM BuildTrace := do

src/lake/Lake/Build/Package.lean

@@ -35,10 +35,12 @@ def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
     job := job.mix <| ← dep.extraDep.fetch
   -- Fetch pre-built release if desired and this package is a dependency
   if self.name ≠ (← getWorkspace).root.name ∧ self.preferReleaseBuild then
-    job := job.add <| ← (← self.optRelease.fetch).bindSync fun success t => do
-      unless success do
-        logWarning "failed to fetch cloud release; falling back to local build"
-      return ((), t)
+    job := job.add <| ←
+      withRegisterJob s!"{self.name}:optRelease" do
+        (← self.optRelease.fetch).bindSync fun success t => do
+          unless success do
+            logWarning "failed to fetch cloud release; falling back to local build"
+          return ((), t)
   -- Build this package's extra dep targets
   for target in self.extraDepTargets do
     job := job.mix <| ← self.fetchTargetJob target
@@ -50,26 +52,26 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
 
 /-- Download and unpack the package's prebuilt release archive (from GitHub). -/
 def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.async do
-  updateAction .fetch
   let repo := GitRepo.mk self.dir
   let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
   let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)
     | logInfo s!"{self.name}: wanted prebuilt release, \
-        but package's repository URL was not known; it may need to set 'releaseRepo'"
+        but repository URL not known; the package may need to set 'releaseRepo'"
+      updateAction .fetch
       return (false, .nil)
   let some tag ← repo.findTag?
-    | logInfo s!"{self.name}: wanted prebuilt release, \
-        but could not find an associated tag for the package's revision"
+    | logInfo s!"{self.name}: wanted prebuilt release, but no tag found for revision"
+      updateAction .fetch
       return (false, .nil)
   let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
-  let logName := s!"{self.name}/{tag}/{self.buildArchive}"
   let depTrace := Hash.ofString url
   let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace"
   let upToDate ← buildUnlessUpToDate? (action := .fetch) self.buildArchiveFile depTrace traceFile do
-    logVerbose s!"downloading {logName}"
+    logVerbose s!"downloading {url}"
     download url self.buildArchiveFile
   unless upToDate && (← self.buildDir.pathExists) do
-    logVerbose s!"unpacking {logName}"
+    updateAction .fetch
+    logVerbose s!"unpacking {self.name}/{tag}/{self.buildArchive}"
     untar self.buildArchiveFile self.buildDir
   return (true, .nil)
 

src/lake/Lake/Build/Run.lean

@@ -31,8 +31,9 @@ structure MonitorContext where
   out : IO.FS.Stream
   outLv : LogLevel
   failLv : LogLevel
-  showProgress : Bool
+  minAction : JobAction
   useAnsi : Bool
+  showProgress : Bool
   /-- How often to poll jobs (in milliseconds). -/
   updateFrequency : Nat := 100
 
@@ -83,19 +84,19 @@ def renderProgress : MonitorM PUnit := do
     if h : 0 < jobs.size then
       let caption := jobs[0]'h |>.caption
       let resetCtrl ← modifyGet fun s => (s.resetCtrl, {s with resetCtrl := Ansi.resetLine})
-      print s!"{resetCtrl}[{jobNo}/{totalJobs}] Checking {caption}"
+      print s!"{resetCtrl}[{jobNo}/{totalJobs}] Running {caption}"
       flush
 
 def reportJob (job : Job Unit) : MonitorM PUnit := do
   let {jobNo, ..} ← get
-  let {totalJobs, failLv, outLv, out, useAnsi, showProgress, ..} ← read
+  let {totalJobs, failLv, outLv, out, useAnsi, showProgress, minAction, ..} ← read
   let {log, action, ..} := job.task.get.state
   let maxLv := log.maxLv
   let failed := log.hasEntries ∧ maxLv ≥ failLv
   if failed then
     modify fun s => {s with failures := s.failures.push job.caption}
   let hasOutput := failed ∨ (log.hasEntries ∧ maxLv ≥ outLv)
-  if hasOutput ∨ (showProgress ∧ action ≥ .fetch) then
+  if hasOutput ∨ (showProgress ∧ (action ≥ minAction)) then
     let verb := action.verb failed
     let icon := if hasOutput then maxLv.icon else '✔'
     let caption := s!"{icon} [{jobNo}/{totalJobs}] {verb} {job.caption}"
@@ -151,14 +152,15 @@ def monitorJobs
   (jobs : Array (Job Unit))
   (out : IO.FS.Stream)
   (failLv outLv : LogLevel)
+  (minAction : JobAction)
   (useAnsi showProgress : Bool)
   (resetCtrl : String := "")
   (initFailures : Array String := #[])
   (totalJobs := jobs.size)
   (updateFrequency := 100)
 : BaseIO (Array String) := do
   let ctx := {
-    totalJobs, out, failLv, outLv,
+    totalJobs, out, failLv, outLv, minAction
     useAnsi, showProgress, updateFrequency
   }
   let s := {
@@ -211,7 +213,8 @@ def Workspace.runFetchM
   -- Job Monitor
   let jobs ← ctx.registeredJobs.get
   let resetCtrl := if showAnsiProgress then Ansi.resetLine else ""
-  let failures ← monitorJobs jobs out failLv outLv useAnsi showProgress
+  let minAction := if cfg.verbosity = .verbose then .unknown else .fetch
+  let failures ← monitorJobs jobs out failLv outLv minAction useAnsi showProgress
     (resetCtrl := resetCtrl) (initFailures := failures)
   -- Failure Report
   if failures.isEmpty then

src/lake/tests/noRelease/clean.sh

@@ -1 +1 @@
-rm -rf .lake lake-manifest.json
+rm -rf .lake lake-manifest.json dep/.lake dep/.git

src/lake/tests/noRelease/dep/lakefile.lean

@@ -4,3 +4,4 @@ open Lake DSL
 package dep where
   preferReleaseBuild := true
   releaseRepo := "https://example.com"
+  buildArchive := "release.tgz"

src/lake/tests/noRelease/lakefile.lean

@@ -3,3 +3,5 @@ open Lake DSL
 
 package test
 require dep from "dep"
+
+lean_lib Test

src/lake/tests/noRelease/test.sh

@@ -12,18 +12,58 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # Test that a direct invocation fo `lake build *:release` fails
 ($LAKE build dep:release && exit 1 || true) | diff -u --strip-trailing-cr <(cat << 'EOF'
 ✖ [1/1] Fetching dep:release
-info: dep: wanted prebuilt release, but could not find an associated tag for the package's revision
+info: dep: wanted prebuilt release, but no tag found for revision
 error: failed to fetch cloud release
 Some builds logged failures:
 - dep:release
 EOF
 ) -
 
 # Test that an indirect fetch on the release does not cause the build to fail
-$LAKE build -v test:extraDep | diff -u --strip-trailing-cr <(cat << 'EOF'
-⚠ [1/1] Fetched test:extraDep
-info: dep: wanted prebuilt release, but could not find an associated tag for the package's revision
+$LAKE build Test | diff -u --strip-trailing-cr <(cat << 'EOF'
+⚠ [1/3] Fetched dep:optRelease
+info: dep: wanted prebuilt release, but no tag found for revision
 warning: failed to fetch cloud release; falling back to local build
+✔ [2/3] Built Test
 Build completed successfully.
 EOF
 ) -
+
+# Since committing a Git repository to a Git repository is not well-supported,
+# We reinitialize the bar repository on each test. This requires updating the
+# locked manifest to the new hash to ensure things work properly.
+pushd dep
+git init
+git checkout -b master
+git config user.name test
+git config user.email [email protected]
+git add --all
+git commit -m "initial commit"
+git tag release
+popd
+
+# Test download failure
+($LAKE build dep:release && exit 1 || true) | grep --color "downloading"
+
+# Test unpacking
+mkdir -p dep/.lake/build
+tar -cz -f dep/.lake/release.tgz -C dep/.lake/build .
+echo 4225503363911572621 > dep/.lake/release.tgz.trace
+rmdir dep/.lake/build
+$LAKE build dep:release -v | grep --color "unpacking"
+test -d dep/.lake/build
+
+# Test that the job prints nothing if the archive is already fetched and unpacked
+$LAKE build dep:release | diff -u --strip-trailing-cr <(cat << 'EOF'
+Build completed successfully.
+EOF
+) -
+
+# Test that releases do not contaminate downstream jobs
+$LAKE build Test | diff -u --strip-trailing-cr <(cat << 'EOF'
+Build completed successfully.
+EOF
+) -
+
+# Cleanup git repo
+rm -rf dep/.git