chore: ensure jobs have captions & fix fetch release

src/lake/Lake/Build/Basic.lean

@@ -39,11 +39,12 @@ abbrev JobTask α := BaseIOTask (JobResult α)
 /-- A Lake job. -/
 structure Job (α : Type u)  where
   task : JobTask α
+  caption : String
 
 /-- A Lake context with a build configuration and additional build data. -/
 structure BuildContext extends BuildConfig, Context where
   leanTrace : BuildTrace
-  registeredJobs : IO.Ref (Array (String × Job Unit))
+  registeredJobs : IO.Ref (Array (Job Unit))
 
 /-- A transformer to equip a monad with a `BuildContext`. -/
 abbrev BuildT := ReaderT BuildContext
@@ -81,11 +82,21 @@ instance [Pure m] : MonadLift LakeM (BuildT m) where
 /-- The internal core monad of Lake builds.  Not intended for user use. -/
 abbrev CoreBuildM := BuildT LogIO
 
-/-- The monad of asynchronous Lake jobs. -/
+/-- The monad of asynchronous Lake jobs. Lifts into `FetchM`. -/
 abbrev JobM := CoreBuildM
 
 /-- The monad used to spawn asynchronous Lake build jobs. Lifts into `FetchM`. -/
 abbrev SpawnM := BuildT BaseIO
 
 /-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/
 @[deprecated SpawnM] abbrev SchedulerM := SpawnM
+
+/--
+Logs a build step with `message`.
+
+**Deprecated:**  Build steps are now managed by a top-level build monitor.
+As a result, this no longer functions the way it used to. It now just logs the
+`message` via `logVerbose`.
+-/
+@[deprecated] def logStep (message : String) : JobM Unit := do
+  logVerbose message

src/lake/Lake/Build/Facets.lean

@@ -116,6 +116,13 @@ module_data o.noexport : BuildJob FilePath
 
 /-! ## Package Facets -/
 
+/--
+A package's *optional* cloud build release.
+Does not fail if the release cannot be fetched.
+-/
+abbrev Package.optReleaseFacet := `optRelease
+package_data optRelease : BuildJob Bool
+
 /-- A package's cloud build release. -/
 abbrev Package.releaseFacet := `release
 package_data release : BuildJob Unit

src/lake/Lake/Build/Fetch.lean

@@ -72,19 +72,46 @@ abbrev FetchM := IndexT RecBuildM
 
 export BuildInfo (fetch)
 
-/-- Register the produced job for the CLI progress UI.  -/
-def withRegisterJob
-  (caption : String) (x : FetchM (Job α))
+/-- Wraps stray I/O, logs, and errors in `x` into the produced job.  -/
+def ensureJob (x : FetchM (Job α))
 : FetchM (Job α) := fun fetch stack ctx log store => do
   let iniPos := log.endPos
   match (← (withLoggedIO x) fetch stack ctx log store) with
   | (.ok job log, store) =>
     let (log, jobLog) := log.split iniPos
-    let regJob := job.mapResult (discard <| ·.modifyState (jobLog ++  ·))
-    ctx.registeredJobs.modify (·.push (caption, regJob))
-    return (.ok job.clearLog log, store)
+    let job := if jobLog.isEmpty then job else
+      job.mapResult (sync := true) (·.modifyState (jobLog ++  ·))
+    return (.ok job log, store)
   | (.error _ log, store) =>
     let (log, jobLog) := log.split iniPos
-    let regJob := ⟨Task.pure <| .error 0 jobLog⟩
-    ctx.registeredJobs.modify (·.push (caption, regJob))
-    return (.ok .error log, store)
+    return (.ok (.error jobLog) log, store)
+
+/--
+Registers the produced job for the top-level build monitor
+(e.g., the Lake CLI progress UI), assigning it `caption`.
+
+Stray I/O, logs, and errors produced by `x` will be wrapped into the job.
+-/
+@[inline] def withRegisterJob
+  (caption : String) (x : FetchM (Job α))
+: FetchM (Job α) := do
+  let job ← ensureJob x
+  let job := job.setCaption caption
+  let regJob := job.mapResult (sync := true) discard
+  (← readThe BuildContext).registeredJobs.modify (·.push regJob)
+  return job.clearLog
+
+/--
+Registers the produced job for the top-level build monitor
+if it is not already (i.e., it has an empty caption).
+-/
+@[inline] def maybeRegisterJob
+  (fallbackCaption : String) (job : Job α)
+: FetchM (Job α) := do
+  if job.caption.isEmpty then
+    let job := job.setCaption fallbackCaption
+    let regJob := job.mapResult (sync := true) discard
+    (← readThe BuildContext).registeredJobs.modify (·.push regJob)
+    return job.clearLog
+  else
+    return job

src/lake/Lake/Build/Info.lean

@@ -220,6 +220,10 @@ abbrev Package.facet (facet : Name) (self : Package) : BuildInfo :=
 abbrev Package.release (self : Package) : BuildInfo :=
   self.facet releaseFacet
 
+@[inherit_doc optReleaseFacet]
+abbrev Package.optRelease (self : Package) : BuildInfo :=
+  self.facet optReleaseFacet
+
 @[inherit_doc extraDepFacet]
 abbrev Package.extraDep (self : Package) : BuildInfo :=
   self.facet extraDepFacet

src/lake/Lake/Build/Job.lean

@@ -12,23 +12,39 @@ namespace Lake
 
 namespace Job
 
-@[inline] protected def pure (a : α) : Job α :=
-  {task := Task.pure (.ok a {})}
+@[inline] def ofTask (task : JobTask α) (caption := "") : Job α :=
+  {task, caption}
+
+@[inline] protected def error (l : Log := {}) (caption := "") : Job α :=
+  {task := Task.pure (.error 0 l), caption}
+
+@[inline] protected def pure (a : α) (l : Log := {}) (caption := "") : Job α :=
+  {task := Task.pure (.ok a l), caption}
 
 instance : Pure Job := ⟨Job.pure⟩
 instance [Inhabited α] : Inhabited (Job α) := ⟨pure default⟩
 
-@[inline] protected def nop : Job Unit :=
-  pure ()
+@[inline] protected def nop (l : Log := {}) (caption := "") : Job Unit :=
+  .pure () l caption
 
-@[inline] protected def error (l : Log := {}) : Job α :=
-  {task := Task.pure (.error 0 l)}
+/-- Sets the job's caption. -/
+@[inline] def setCaption (caption : String) (job : Job α) : Job α :=
+  {job with caption}
+
+/-- Sets the job's caption if the job's current caption is empty. -/
+@[inline] def setCaption? (caption : String) (job : Job α) : Job α :=
+  if job.caption.isEmpty then {job with caption} else job
 
 @[inline] def mapResult
   (f : JobResult α → JobResult β) (self : Job α)
   (prio := Task.Priority.default) (sync := false)
 : Job β :=
-  {task := self.task.map f prio sync}
+  {self with task := self.task.map f prio sync}
+
+@[inline] def bindTask [Monad m]
+  (f : JobTask α → m (JobTask β)) (self : Job α)
+: m (Job β) :=
+  return {self with task := ← f self.task}
 
 @[inline] protected def map
   (f : α → β) (self : Job α)
@@ -56,7 +72,7 @@ instance : Functor Job where map := Job.map
 /-- Spawn a job that asynchronously performs `act`. -/
 @[inline] protected def async
   (act : JobM α) (prio := Task.Priority.default)
-: SpawnM (Job α) := fun ctx => Job.mk <$> do
+: SpawnM (Job α) := fun ctx => .ofTask <$> do
   BaseIO.asTask (prio := prio) do (withLoggedIO act) ctx {}
 
 /-- Wait a the job to complete and return the result. -/
@@ -86,8 +102,8 @@ after the job `a` completes.
 @[inline] protected def bindSync
   (self : Job α) (f : α → JobM β)
   (prio := Task.Priority.default) (sync := false)
-: SpawnM (Job β) := fun ctx => Job.mk <$> do
-  BaseIO.mapTask (t := self.task) (prio := prio) (sync := sync) fun
+: SpawnM (Job β) := fun ctx => self.bindTask fun task => do
+  BaseIO.mapTask (t := task) (prio := prio) (sync := sync) fun
     | EResult.ok a l => (withLoggedIO (f a)) ctx l
     | EResult.error n l => return .error n l
 
@@ -98,8 +114,8 @@ after the job `a` completes and then merges into the job produced by `b`.
 @[inline] protected def bindAsync
   (self : Job α) (f : α → SpawnM (Job β))
   (prio := Task.Priority.default) (sync := false)
-: SpawnM (Job β) := fun ctx => Job.mk <$> do
-  BaseIO.bindTask self.task (prio := prio) (sync := sync) fun
+: SpawnM (Job β) := fun ctx => self.bindTask fun task => do
+  BaseIO.bindTask task (prio := prio) (sync := sync) fun
     | .ok a l => do
       let job ← f a ctx
       if l.isEmpty then return job.task else
@@ -115,7 +131,7 @@ results of `a` and `b`. The job `c` errors if either `a` or `b` error.
 @[inline] def zipWith
   (f : α → β → γ) (x : Job α) (y : Job β)
   (prio := Task.Priority.default) (sync := false)
-: BaseIO (Job γ) := Job.mk <$> do
+: BaseIO (Job γ) := Job.ofTask <$> do
   BaseIO.bindTask x.task (prio := prio) (sync := true) fun rx =>
   BaseIO.mapTask (t := y.task) (prio := prio) (sync := sync) fun ry =>
   match rx, ry with
@@ -147,14 +163,14 @@ namespace BuildJob
 instance : Pure BuildJob := ⟨BuildJob.pure⟩
 
 @[inline] def attempt (self : BuildJob α) : BuildJob Bool :=
-  {task := self.toJob.task.map fun
+  self.mapResult fun
     | .error _ l => .ok (false, nilTrace) l
-    | .ok (_, t) l => .ok (true, t) l}
+    | .ok (_, t) l => .ok (true, t) l
 
 @[inline] def attempt? (self : BuildJob α) : BuildJob (Option α) :=
-  {task := self.toJob.task.map fun
+  self.mapResult fun
     | .error _ l => .ok (none, nilTrace) l
-    | .ok (a, t) l => .ok (some a, t) l}
+    | .ok (a, t) l => .ok (some a, t) l
 
 @[inline] protected def map (f : α → β) (self : BuildJob α) : BuildJob β :=
   mk <| (fun (a,t) => (f a,t)) <$> self.toJob

src/lake/Lake/Build/Key.lean

@@ -23,6 +23,18 @@ def toString : (self : BuildKey) → String
 | targetFacet p t f => s!"{p}/{t}:{f}"
 | customTarget p t => s!"{p}/{t}"
 
+/-- Like the default `toString`, but without disambiguation markers. -/
+def toSimpleString : (self : BuildKey) → String
+| moduleFacet m f => s!"{m}:{f}"
+| packageFacet p f => s!"{p}:{f}"
+| targetFacet p t f => s!"{p}/{t}:{eraseHead f}"
+| customTarget p t => s!"{p}/{t}"
+where
+  eraseHead : Name → Name
+    | .anonymous | .str .anonymous _  | .num .anonymous _  => .anonymous
+    | .str p s => .str (eraseHead p) s
+    | .num p s => .num (eraseHead p) s
+
 instance : ToString BuildKey := ⟨(·.toString)⟩
 
 def quickCmp (k k' : BuildKey) : Ordering :=

src/lake/Lake/Build/Package.lean

@@ -35,9 +35,9 @@ 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.release.fetch).attempt.bindSync fun success t => do
+    job ← job.add <| ← (← self.optRelease.fetch).bindSync fun success t => do
       unless success do
-        logWarning "fetching cloud release failed; falling back to local build"
+        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
@@ -49,16 +49,17 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
   mkFacetJobConfig Package.recBuildExtraDepTargets
 
 /-- Download and unpack the package's prebuilt release archive (from GitHub). -/
-def Package.fetchRelease (self : Package) : FetchM (BuildJob Unit) :=
-  withRegisterJob s!"Fetching {self.name} cloud release" <| Job.async do
+def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.async do
   let repo := GitRepo.mk self.dir
   let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
   let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)
-    | error <| s!"{self.name}: wanted prebuilt release, " ++
-      "but package's repository URL was not known; it may need to set `releaseRepo?`"
+    | logInfo s!"{self.name}: wanted prebuilt release, \
+        but package's repository URL was not known; it may need to set 'releaseRepo'"
+      return (false, .nil)
   let some tag ← repo.findTag?
-    | error <| 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 could not find an associated tag for the package's revision"
+      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
@@ -69,11 +70,20 @@ def Package.fetchRelease (self : Package) : FetchM (BuildJob Unit) :=
   unless upToDate && (← self.buildDir.pathExists) do
     logVerbose s!"unpacking {logName}"
     untar self.buildArchiveFile self.buildDir
-  return ((), .nil)
+  return (true, .nil)
+
+/-- The `PackageFacetConfig` for the builtin `optReleaseFacet`. -/
+def Package.optReleaseFacetConfig : PackageFacetConfig optReleaseFacet :=
+  mkFacetJobConfig (·.fetchOptRelease)
 
 /-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/
 def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=
-  mkFacetJobConfig (·.fetchRelease)
+  mkFacetJobConfig fun pkg =>
+    withRegisterJob s!"Fetching {pkg.name} cloud release" do
+      (← pkg.optRelease.fetch).bindSync fun success t => do
+        unless success do
+          error "failed to fetch cloud release"
+        return ((), t)
 
 /-- Perform a build job after first checking for a cloud release for the package. -/
 def Package.afterReleaseAsync (self : Package) (build : SpawnM (Job α)) : FetchM (Job α) := do
@@ -98,4 +108,5 @@ def initPackageFacetConfigs : DNameMap PackageFacetConfig :=
   DNameMap.empty
   |>.insert depsFacet depsFacetConfig
   |>.insert extraDepFacet extraDepFacetConfig
+  |>.insert optReleaseFacet optReleaseFacetConfig
   |>.insert releaseFacet releaseFacetConfig

src/lake/Lake/Build/Run.lean

@@ -27,7 +27,7 @@ def mkBuildContext (ws : Workspace) (config : BuildConfig) : BaseIO BuildContext
 
 /-- The job monitor function. An auxiliary definition for `runFetchM`. -/
 partial def monitorJobs
-  (jobs : Array (String × Job Unit))
+  (jobs : Array (Job Unit))
   (out : IO.FS.Stream)
   (failLv outLv : LogLevel)
   (showANSIProgress : Bool)
@@ -42,25 +42,25 @@ where
     let mut unfinishedJobs := #[]
     let mut failures := initFailures
     let mut resetCtrl := resetCtrl
-    for jobEntry@(caption, job) in jobs do
+    for job in jobs do
       if (← IO.hasFinished job.task) then
         let log := job.task.get.state
         let failed := log.hasEntriesGe failLv
         if failed then
-          failures := failures.push caption
+          failures := failures.push job.caption
         if log.hasEntriesGe outLv then
           let jobsDone := totalJobs - jobs.size + unfinishedJobs.size + 1
-          out.putStr s!"{resetCtrl}[{jobsDone}/{totalJobs}] {caption}\n"
+          out.putStr s!"{resetCtrl}[{jobsDone}/{totalJobs}] {job.caption}\n"
           resetCtrl := ""
           let outLv := if failed then .trace else outLv
           log.replay (logger := MonadLog.stream out outLv)
           out.flush
       else
-        unfinishedJobs := unfinishedJobs.push jobEntry
+        unfinishedJobs := unfinishedJobs.push job
     if h : 0 < unfinishedJobs.size then
       if showANSIProgress then
         let jobsDone := totalJobs - jobs.size
-        let (caption, _) := unfinishedJobs[0]'h
+        let caption := unfinishedJobs[0]'h |>.caption
         out.putStr s!"{resetCtrl}[{jobsDone}/{totalJobs}] {caption}"
         resetCtrl := "\x1B[2K\r"
         out.flush
@@ -74,6 +74,15 @@ where
         out.putStr resetCtrl
       return failures
 
+/--
+Whether the build should show progress information.
+
+`Verbosity.quiet` hides progress and, for a `noBuild`,
+`Verbosity.verbose` shows progress.
+-/
+def BuildConfig.showProgress (cfg : BuildConfig) : Bool :=
+  (cfg.noBuild ∧ cfg.verbosity == .verbose) ∨ cfg.verbosity != .quiet
+
 /--
 Run a build function in the Workspace's context using the provided configuration.
 Reports incremental build progress and build logs. In quiet mode, only reports
@@ -86,12 +95,9 @@ def Workspace.runFetchM
   let ctx ← mkBuildContext ws cfg
   let out ← if cfg.useStdout then IO.getStdout else IO.getStderr
   let useANSI ← out.isTty
-  let verbosity := cfg.verbosity
-  let outLv := verbosity.minLogLevel
-  let failLv : LogLevel := if ctx.failIfWarnings then .warning else .error
-  let showProgress :=
-    (cfg.noBuild ∧ verbosity == .verbose) ∨
-    verbosity != .quiet
+  let outLv := cfg.verbosity.minLogLevel
+  let failLv : LogLevel := if cfg.failIfWarnings then .warning else .error
+  let showProgress := cfg.showProgress
   let showANSIProgress := showProgress ∧ useANSI
   -- Job Computation
   let caption := "Computing build jobs"
@@ -104,7 +110,7 @@ def Workspace.runFetchM
   if log.hasEntriesGe outLv then
     unless showANSIProgress do
       out.putStr header
-      out.putStr "\n"
+    out.putStr "\n"
     let outLv := if failed then .trace else outLv
     log.replay (logger := MonadLog.stream out outLv)
     out.flush