feat: lake: cleaner release handling & related touchups (#4735)

Improves a number of elements related to Git checkouts, cloud releases,
and related error handling.

* On error, Lake now prints all top-level logs. Top-level logs are those
produced by Lake outside of the job monitor (e.g., when cloning
dependencies).
* When fetching a remote for a dependency, Lake now forcibly fetches
tags. This prevents potential errors caused by a repository recreating
tags already fetched.
* Tweaked Git error handling to hopefully be more informative.
* The builtin package facets `release`, `optRelease`, `extraDep` are now
caption in the same manner as other facets. Previously, they were
attempting to be too clever.
* `afterReleaseSync` and `afterReleaseAsync` now fetch `optRelease`
rather than `release`.
* Added support for optional jobs, whose failure does not cause the
whole build to failure (and made `optRelease` such a job).

Closes #4302.

src/lake/Lake/Build/Basic.lean

@@ -51,8 +51,24 @@ Whether the build should show progress information.
 def BuildConfig.showProgress (cfg : BuildConfig) : Bool :=
   (cfg.noBuild ∧ cfg.verbosity == .verbose) ∨ cfg.verbosity != .quiet
 
+/-- The core structure of a Lake job. -/
+structure JobCore (α : Type u)  where
+  /-- The Lean `Task` object for the job. -/
+  task : α
+  /--
+  A caption for the job in Lake's build monitor.
+  Will be formatted like `✔ [3/5] Ran <caption>`.
+  -/
+  caption : String
+  /-- Whether this job failing should cause the build to fail. -/
+  optional : Bool := false
+  deriving Inhabited
+
+/-- A Lake job task with an opaque value type in `Type`. -/
+declare_opaque_type OpaqueJobTask
+
 /-- A Lake job with an opaque value type in `Type`. -/
-declare_opaque_type OpaqueJob
+abbrev OpaqueJob := JobCore OpaqueJobTask
 
 /-- A Lake context with a build configuration and additional build data. -/
 structure BuildContext extends BuildConfig, Context where

src/lake/Lake/Build/Facets.lean

@@ -118,12 +118,15 @@ module_data o.noexport : BuildJob FilePath
 
 /--
 A package's *optional* cloud build release.
-Does not fail if the release cannot be fetched.
+Will not cause the whole build to fail if the release cannot be fetched.
 -/
 abbrev Package.optReleaseFacet := `optRelease
 package_data optRelease : BuildJob Bool
 
-/-- A package's cloud build release. -/
+/--
+A package's cloud build release.
+Will cause the whole build to fail if the release cannot be fetched.
+-/
 abbrev Package.releaseFacet := `release
 package_data release : BuildJob Unit
 

src/lake/Lake/Build/Fetch.lean

@@ -104,8 +104,8 @@ def ensureJob (x : FetchM (Job α))
 Registers the job for the top-level build monitor,
 (e.g., the Lake CLI progress UI), assigning it `caption`.
 -/
-def registerJob (caption : String) (job : Job α) : FetchM (Job α) := do
-  let job := job.setCaption caption
+def registerJob (caption : String) (job : Job α) (optional := false) : FetchM (Job α) := do
+  let job : Job α := {job with caption, optional}
   (← getBuildContext).registeredJobs.modify (·.push job)
   return job.renew
 
@@ -116,10 +116,10 @@ Registers the produced job for the top-level build monitor
 Stray I/O, logs, and errors produced by `x` will be wrapped into the job.
 -/
 def withRegisterJob
-  (caption : String) (x : FetchM (Job α))
+  (caption : String) (x : FetchM (Job α)) (optional := false)
 : FetchM (Job α) := do
   let job ← ensureJob x
-  registerJob caption job
+  registerJob caption job optional
 
 /--
 Registers the produced job for the top-level build monitor

src/lake/Lake/Build/Job.lean

@@ -101,33 +101,32 @@ abbrev SpawnM := BuildT BaseIO
 @[deprecated SpawnM (since := "2024-05-21")] abbrev SchedulerM := SpawnM
 
 /-- A Lake job. -/
-structure Job (α : Type u)  where
-  task : JobTask α
-  caption : String
+abbrev Job (α : Type u)  := JobCore (JobTask α)
+
+structure BundledJobTask where
+  {Result : Type u}
+  task : JobTask Result
   deriving Inhabited
 
-structure BundledJob where
-  {type : Type u}
-  job : Job type
-  deriving Inhabited
+instance : CoeOut (JobTask α) BundledJobTask := ⟨.mk⟩
 
-instance : CoeOut (Job α) BundledJob := ⟨.mk⟩
+hydrate_opaque_type OpaqueJobTask BundledJobTask
 
-hydrate_opaque_type OpaqueJob BundledJob
+abbrev OpaqueJob.Result (job : OpaqueJob) : Type :=
+  job.task.get.Result
 
-abbrev OpaqueJob.type (job : OpaqueJob) : Type :=
-  job.get.type
+nonrec abbrev OpaqueJob.task (job : OpaqueJob) : JobTask job.Result :=
+  job.task.get.task
 
-abbrev OpaqueJob.toJob (job : OpaqueJob) : Job job.type :=
-  job.get.job
+abbrev OpaqueJob.ofJob (job : Job α) : OpaqueJob :=
+  {job with task := job.task}
 
-abbrev OpaqueJob.task (job : OpaqueJob) : JobTask job.type :=
-  job.toJob.task
+instance : CoeOut (Job α) OpaqueJob := ⟨.ofJob⟩
 
-abbrev OpaqueJob.caption (job : OpaqueJob) : String :=
-  job.toJob.caption
+abbrev OpaqueJob.toJob (job : OpaqueJob) : Job job.Result :=
+  {job with task := job.task}
 
-instance : CoeDep OpaqueJob job (Job job.type) := ⟨job.toJob⟩
+instance : CoeDep OpaqueJob job (Job job.Result) := ⟨job.toJob⟩
 
 namespace Job
 

src/lake/Lake/Build/Package.lean

@@ -24,23 +24,27 @@ def Package.recComputeDeps (self : Package) : FetchM (Array Package) := do
 def Package.depsFacetConfig : PackageFacetConfig depsFacet :=
   mkFacetConfig Package.recComputeDeps
 
+/-- Tries to download and unpack the package's prebuilt release archive (from GitHub). -/
+def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Unit) := do
+  (← self.optRelease.fetch).bindSync fun success t => do
+    unless success do
+      logWarning s!"building from source; \
+        failed to fetch cloud release (see '{self.name}:optRelease' for details)"
+    return ((), t)
+
 /--
 Build the `extraDepTargets` for the package and its transitive dependencies.
 Also fetch pre-built releases for the package's' dependencies.
 -/
-def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) := do
+def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
+  withRegisterJob s!"{self.name}:extraDep" do
   let mut job := BuildJob.nil
   -- Build dependencies' extra dep targets
   for dep in self.deps do
     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 <| ←
-      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)
+    job := job.add <| ← self.fetchOptRelease
   -- Build this package's extra dep targets
   for target in self.extraDepTargets do
     job := job.mix <| ← self.fetchTargetJob target
@@ -50,17 +54,19 @@ def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
 def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
   mkFacetJobConfig Package.recBuildExtraDepTargets
 
-/-- Download and unpack the package's prebuilt release archive (from GitHub). -/
-def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.async do
+/-- Tries to download and unpack the package's prebuilt release archive (from GitHub). -/
+def Package.fetchOptReleaseCore (self : Package) : FetchM (BuildJob Bool) :=
+  withRegisterJob s!"{self.name}:optRelease" (optional := true) <| Job.async do
   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 repository URL not known; the package may need to set 'releaseRepo'"
+    | logError s!"release 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 no tag found for revision"
+    | let rev ← if let some rev ← repo.getHeadRevision? then pure s!" '{rev}'" else pure ""
+      logError s!"no release tag found for revision{rev}"
       updateAction .fetch
       return (false, .nil)
   let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
@@ -77,7 +83,7 @@ def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.asy
 
 /-- The `PackageFacetConfig` for the builtin `optReleaseFacet`. -/
 def Package.optReleaseFacetConfig : PackageFacetConfig optReleaseFacet :=
-  mkFacetJobConfig (·.fetchOptRelease)
+  mkFacetJobConfig (·.fetchOptReleaseCore)
 
 /-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/
 def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=
@@ -85,20 +91,20 @@ def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=
     withRegisterJob s!"{pkg.name}:release" do
       (← pkg.optRelease.fetch).bindSync fun success t => do
         unless success do
-          error "failed to fetch cloud release"
+          error s!"failed to fetch cloud release (see '{pkg.name}:optRelease' for details)"
         return ((), t)
 
-/-- Perform a build job after first checking for a cloud release for the package. -/
+/-- Perform a build job after first checking for an (optional) cloud release for the package. -/
 def Package.afterReleaseAsync (self : Package) (build : SpawnM (Job α)) : FetchM (Job α) := do
   if self.preferReleaseBuild ∧ self.name ≠ (← getRootPackage).name then
-    (← self.release.fetch).bindAsync fun _ _ => build
+    (← self.optRelease.fetch).bindAsync fun _ _ => build
   else
     build
 
-/-- Perform a build after first checking for a cloud release for the package. -/
+/-- Perform a build after first checking for an (optional) cloud release for the package. -/
 def Package.afterReleaseSync (self : Package) (build : JobM α) : FetchM (Job α) := do
   if self.preferReleaseBuild ∧ self.name ≠ (← getRootPackage).name then
-    (← self.release.fetch).bindSync fun _ _ => build
+    (← self.optRelease.fetch).bindSync fun _ _ => build
   else
     Job.async build
 

src/lake/Lake/Build/Run.lean

@@ -99,17 +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 {task, caption} := job.toJob
+  let {task, caption, optional} := job.toJob
   let {log, action, ..} := task.get.state
   let maxLv := log.maxLv
   let failed := log.hasEntries ∧ maxLv ≥ failLv
-  if failed then
+  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 verb := action.verb failed
     let icon := if hasOutput then maxLv.icon else '✔'
-    let caption := s!"{icon} [{jobNo}/{totalJobs}] {verb} {caption}"
+    let opt := if optional then " (Optional)" else ""
+    let caption := s!"{icon} [{jobNo}/{totalJobs}]{opt} {verb} {caption}"
     let caption :=
       if useAnsi then
         let color := if hasOutput then maxLv.ansiColor else "32"
@@ -235,7 +236,7 @@ def Workspace.runFetchM
       | error "top-level build failed"
     return a
   else
-    print! out "Some builds logged failures:\n"
+    print! out "Some required builds logged failures:\n"
     failures.forM (print! out s!"- {·}\n")
     flush out
     error "build failed"

src/lake/Lake/Util/Git.lean

@@ -47,9 +47,6 @@ def cwd : GitRepo := ⟨"."⟩
 @[inline] def dirExists (repo : GitRepo) : BaseIO Bool :=
   repo.dir.isDir
 
-@[inline] def captureGit (args : Array String) (repo : GitRepo) : LogIO String :=
-  captureProc {cmd := "git", args, cwd := repo.dir}
-
 @[inline] def captureGit? (args : Array String) (repo : GitRepo) : BaseIO (Option String) :=
   captureProc? {cmd := "git", args, cwd := repo.dir}
 
@@ -66,31 +63,30 @@ def cwd : GitRepo := ⟨"."⟩
   repo.execGit #["init", "-q"]
 
 @[inline] def fetch (repo : GitRepo) (remote := Git.defaultRemote) : LogIO PUnit  :=
-  repo.execGit #["fetch", remote]
+  repo.execGit #["fetch", "--tags", "--force", remote]
 
 @[inline] def checkoutBranch (branch : String) (repo : GitRepo) : LogIO PUnit :=
   repo.execGit #["checkout", "-B", branch]
 
 @[inline] def checkoutDetach (hash : String) (repo : GitRepo) : LogIO PUnit  :=
-  repo.execGit #["checkout", "--detach", hash]
+  repo.execGit #["checkout", "--detach", hash, "--"]
 
 @[inline] def resolveRevision? (rev : String) (repo : GitRepo) : BaseIO (Option String) := do
-  repo.captureGit? #["rev-parse", "--verify", rev]
-
-@[inline] def resolveRevision (rev : String) (repo : GitRepo) : LogIO String := do
-  repo.captureGit #["rev-parse", "--verify", rev]
-
-@[inline] def getHeadRevision (repo : GitRepo) : LogIO String :=
-  repo.resolveRevision "HEAD"
+  repo.captureGit? #["rev-parse", "--verify", "--end-of-options", rev]
 
 @[inline] def getHeadRevision? (repo : GitRepo) : BaseIO (Option String) :=
   repo.resolveRevision? "HEAD"
 
+def getHeadRevision (repo : GitRepo) : LogIO String := do
+  if let some rev ← repo.getHeadRevision? then return rev
+  error s!"{repo}: could not resolve 'HEAD' to a commit; \
+    the repository may be corrupt, so you may need to remove it and try again"
+
 def resolveRemoteRevision (rev : String) (remote := Git.defaultRemote) (repo : GitRepo) : LogIO String := do
   if Git.isFullObjectName rev then return rev
   if let some rev ← repo.resolveRevision? s!"{remote}/{rev}"  then return rev
   if let some rev ← repo.resolveRevision? rev then return rev
-  error s!"cannot find revision {rev} in repository {repo}"
+  error s!"{repo}: revision not found '{rev}'"
 
 def findRemoteRevision (repo : GitRepo) (rev? : Option String := none) (remote := Git.defaultRemote) : LogIO String := do
   repo.fetch remote; repo.resolveRemoteRevision (rev?.getD Git.upstreamBranch) remote

src/lake/Lake/Util/MainM.lean

@@ -79,10 +79,9 @@ instance : MonadLift IO MainM := ⟨MonadError.runIO⟩
 @[inline] def runLogIO (x : LogIO α)
   (minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr)
 : MainM α := do
-  let logger ← out.getLogger minLv ansiMode
   match (← x {}) with
-  | .ok a  log => replay log logger; return a
-  | .error _ log => replay log logger; exit 1
+  | .ok a  log => replay log (← out.getLogger minLv ansiMode); return a
+  | .error _ log => replay log (← out.getLogger .trace ansiMode); exit 1
 where
   -- avoid specialization of this call at each call site
   replay (log : Log) (logger : MonadLog BaseIO) : BaseIO Unit :=

src/lake/tests/noRelease/lakefile.lean

@@ -2,6 +2,7 @@ import Lake
 open Lake DSL
 
 package test
-require dep from "dep"
+
+require dep from git "dep" @ "release"
 
 lean_lib Test

src/lake/tests/noRelease/test.sh

@@ -19,40 +19,51 @@ git config user.name test
 git config user.email test@example.com
 git add --all
 git commit -m "initial commit"
+git tag release
+INIT_REV=`git rev-parse release`
+git commit --allow-empty -m "second commit"
 popd
 
+# Clone dependency
+$LAKE update
+# Remove the release tag from the local copy
+git -C .lake/packages/dep tag -d release
+
 # 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 no tag found for revision
-error: failed to fetch cloud release
-Some builds logged failures:
+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 cloud release (see 'dep:optRelease' 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/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
+$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)
+✔ [4/5] Built Test
 Build completed successfully.
 EOF
 ) -
 
 # Test download failure
-git -C dep tag release
+$LAKE update # re-fetch release tag
 ($LAKE build dep:release && exit 1 || true) | grep --color "downloading"
 
 # Test automatic cloud release unpacking
-mkdir -p dep/.lake/build
-$LAKE -d dep pack 2>&1 | grep --color "packing"
-test -f dep/.lake/release.tgz
-echo 4225503363911572621 > dep/.lake/release.tgz.trace
-rmdir dep/.lake/build
+mkdir -p .lake/packages/dep/.lake/build
+$LAKE -d .lake/packages/dep pack 2>&1 | grep --color "packing"
+test -f .lake/packages/dep/.lake/release.tgz
+echo 4225503363911572621 > .lake/packages/dep/.lake/release.tgz.trace
+rmdir .lake/packages/dep/.lake/build
 $LAKE build dep:release -v | grep --color "unpacking"
-test -d dep/.lake/build
+test -d .lake/packages/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'
@@ -66,5 +77,15 @@ Build completed successfully.
 EOF
 ) -
 
+# Test retagging
+git -C dep tag -d release
+git -C dep tag release
+NEW_REV=`git -C dep rev-parse release`
+test ! "$INIT_REV" = "$NEW_REV"
+test `git -C .lake/packages/dep rev-parse HEAD` = "$INIT_REV"
+$LAKE update
+test `git -C .lake/packages/dep rev-parse HEAD` = "$NEW_REV"
+$LAKE build dep:release
+
 # Cleanup git repo
 rm -rf dep/.git