feat: add lake shake command

script/lakefile.toml

@@ -3,9 +3,3 @@ name = "scripts"
 [[lean_exe]]
 name = "modulize"
 root = "Modulize"
-
-[[lean_exe]]
-name = "shake"
-root = "Shake"
-# needed by `Lake.loadWorkspace`
-supportInterpreter = true

src/lake/Lake/Build/Context.lean

@@ -36,10 +36,18 @@ Whether the build should show progress information.
 public def BuildConfig.showProgress (cfg : BuildConfig) : Bool :=
   (cfg.noBuild ∧ cfg.verbosity == .verbose) ∨ cfg.verbosity != .quiet
 
+/-- Mutable reference of registered build jobs. -/
+@[expose] -- for codegen
+public def JobQueue := IO.Ref (Array OpaqueJob)
+
+/-- Returns a new empty job queue. -/
+@[inline] public def mkJobQueue : BaseIO JobQueue :=
+  IO.mkRef #[]
+
 /-- A Lake context with a build configuration and additional build data. -/
 public structure BuildContext extends BuildConfig, Context where
   leanTrace : BuildTrace
-  registeredJobs : IO.Ref (Array OpaqueJob)
+  registeredJobs : JobQueue
 
 /-- A transformer to equip a monad with a `BuildContext`. -/
 public abbrev BuildT := ReaderT BuildContext

src/lake/Lake/Build/Run.lean

@@ -22,6 +22,7 @@ open System
 namespace Lake
 
 /-- Create a fresh build context from a workspace and a build configuration. -/
+@[deprecated "Deprecated without replacement." (since := "2025-01-08")]
 public def mkBuildContext (ws : Workspace) (config : BuildConfig) : BaseIO BuildContext := do
   return {
     opaqueWs := ws,
@@ -37,7 +38,7 @@ private def Monitor.spinnerFrames :=
 
 /-- Context of the Lake build monitor. -/
 private structure MonitorContext where
-  jobs : IO.Ref (Array OpaqueJob)
+  jobs : JobQueue
   out : IO.FS.Stream
   outLv : LogLevel
   failLv : LogLevel
@@ -49,6 +50,9 @@ private structure MonitorContext where
   /-- How often to poll jobs (in milliseconds). -/
   updateFrequency : Nat
 
+@[inline] def MonitorContext.logger (ctx : MonitorContext) : MonadLog IO :=
+  .stream ctx.out ctx.outLv ctx.useAnsi
+
 /-- State of the Lake build monitor. -/
 private structure MonitorState where
   jobNo : Nat := 0
@@ -189,12 +193,51 @@ private def main (init : Array OpaqueJob) : MonitorM PUnit := do
 
 end Monitor
 
+/-- **For internal use only.** -/
 public structure MonitorResult where
   didBuild : Bool
   failures : Array String
   numJobs : Nat
 
+@[inline] def MonitorResult.isOk (self : MonitorResult) : Bool :=
+  self.failures.isEmpty
+
+def mkMonitorContext (cfg : BuildConfig) (jobs : JobQueue) : BaseIO MonitorContext := do
+  let out ← cfg.out.get
+  let useAnsi ← cfg.ansiMode.isEnabled out
+  let outLv := cfg.outLv
+  let failLv := cfg.failLv
+  let isVerbose := cfg.verbosity = .verbose
+  let showProgress := cfg.showProgress
+  let minAction := if isVerbose then .unknown else .fetch
+  let showOptional := isVerbose
+  let showTime := isVerbose || !useAnsi
+  let updateFrequency := 100
+  return {
+    jobs, out, failLv, outLv, minAction, showOptional
+    useAnsi, showProgress, showTime, updateFrequency
+  }
+
+def monitorJobs'
+  (ctx : MonitorContext)
+  (initJobs : Array OpaqueJob)
+  (initFailures : Array String := #[])
+  (resetCtrl : String := "")
+: BaseIO MonitorResult := do
+  let s := {
+    resetCtrl
+    lastUpdate := ← IO.monoMsNow
+    failures := initFailures
+  }
+  let (_,s) ← Monitor.main initJobs |>.run ctx s
+  return {
+    failures := s.failures
+    numJobs := s.totalJobs
+    didBuild := s.didBuild
+  }
+
 /-- The job monitor function. An auxiliary definition for `runFetchM`. -/
+@[inline, deprecated "Deprecated without replacement" (since := "2025-01-08")]
 public def monitorJobs
   (initJobs : Array OpaqueJob)
   (jobs : IO.Ref (Array OpaqueJob))
@@ -210,99 +253,148 @@ public def monitorJobs
     jobs, out, failLv, outLv, minAction, showOptional
     useAnsi, showProgress, showTime, updateFrequency
   }
-  let s := {
-    resetCtrl
-    lastUpdate := ← IO.monoMsNow
-    failures := initFailures
-  }
-  let (_,s) ← Monitor.main initJobs |>.run ctx s
-  return {
-    failures := s.failures
-    numJobs := s.totalJobs
-    didBuild := s.didBuild
-  }
+  monitorJobs' ctx initJobs initFailures resetCtrl
 
 /-- Exit code to return if `--no-build` is set and a build is required. -/
 public def noBuildCode : ExitCode := 3
 
-/--
-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
-failing build jobs (e.g., when using `-q` or non-verbose `--no-build`).
--/
-public def Workspace.runFetchM
-  (ws : Workspace) (build : FetchM α) (cfg : BuildConfig := {})
-: IO α := do
-  -- Configure
-  let out ← cfg.out.get
-  let useAnsi ← cfg.ansiMode.isEnabled out
-  let outLv := cfg.outLv
-  let failLv := cfg.failLv
-  let isVerbose := cfg.verbosity = .verbose
-  let showProgress := cfg.showProgress
-  let showSuccess := cfg.showSuccess
-  let ctx ← mkBuildContext ws cfg
-  -- Job Computation
-  let caption := "job computation"
-  let compute := Job.async build (caption := caption)
-  let job ← compute.run.run'.run ctx |>.run nilTrace
-  -- Job Monitor
-  let minAction := if isVerbose then .unknown else .fetch
-  let showOptional := isVerbose
-  let showTime := isVerbose || !useAnsi
-  let {failures, numJobs, didBuild} ← monitorJobs #[job] ctx.registeredJobs
-    out failLv outLv minAction showOptional useAnsi showProgress showTime
-  -- Save input-to-output mappings
-  if let some outputsFile := cfg.outputsFile? then
-    let logger := .stream out outLv useAnsi
-    unless ws.isRootArtifactCacheEnabled do
-      logger.logEntry <| .warning s!"{ws.root.prettyName}: \
-        the artifact cache is not enabled for this package, so the artifacts described \
-        by the mappings produced by `-o` will not necessarily be available in the cache."
-    if let some ref := ws.root.outputsRef? then
-      match (← (← ref.get).writeFile outputsFile {}) with
-      | .ok _ log =>
-        if !log.isEmpty && isVerbose then
-          print! out "There were issues saving input-to-output mappings from the build:\n"
-          log.replay (logger := logger)
-      | .error _ log =>
-        print! out "Failed to save input-to-output mappings from the build.\n"
-        if isVerbose then
-          log.replay (logger := logger)
-    else
-      print! out "Workspace missing input-to-output mappings from build. (This is likely a bug in Lake.)\n"
-  -- Report
-  let isNoBuild := cfg.noBuild
-  if failures.isEmpty then
-    let some a ← job.wait?
-      | print! out "Uncaught top-level build failure (this is likely a bug in Lake).\n"
-        error "build failed"
-    if showProgress && showSuccess then
+def Workspace.saveOutputs
+  [logger : MonadLog IO] (ws : Workspace)
+  (out : IO.FS.Stream) (outputsFile : FilePath) (isVerbose : Bool)
+: IO Unit := do
+  unless ws.isRootArtifactCacheEnabled do
+    logWarning s!"{ws.root.prettyName}: \
+      the artifact cache is not enabled for this package, so the artifacts described \
+      by the mappings produced by `-o` will not necessarily be available in the cache."
+  if let some ref := ws.root.outputsRef? then
+    match (← (← ref.get).writeFile outputsFile {}) with
+    | .ok _ log =>
+      if !log.isEmpty && isVerbose then
+        print! out "There were issues saving input-to-output mappings from the build:\n"
+        log.replay
+    | .error _ log =>
+      print! out "Failed to save input-to-output mappings from the build.\n"
+      if isVerbose then
+        log.replay
+  else
+    print! out "Workspace missing input-to-output mappings from build. (This is likely a bug in Lake.)\n"
+
+def reportResult (cfg : BuildConfig) (out : IO.FS.Stream) (result : MonitorResult) : BaseIO Unit := do
+  if result.failures.isEmpty then
+    if cfg.showProgress && cfg.showSuccess then
+      let numJobs := result.numJobs
       let jobs := if numJobs == 1 then "1 job" else s!"{numJobs} jobs"
-      if isNoBuild then
+      if cfg.noBuild then
         print! out s!"All targets up-to-date ({jobs}).\n"
       else
         print! out s!"Build completed successfully ({jobs}).\n"
-    return a
   else
     print! out "Some required targets logged failures:\n"
-    failures.forM (print! out s!"- {·}\n")
+    result.failures.forM (print! out s!"- {·}\n")
     flush out
-    if isNoBuild && didBuild then
-      IO.Process.exit noBuildCode.toUInt8
+
+structure BuildResult (α : Type u) extends MonitorResult where
+  out : Except String α
+
+instance : CoeOut (BuildResult α) MonitorResult := ⟨BuildResult.toMonitorResult⟩
+
+@[inline] def BuildResult.isOk (self : BuildResult α) : Bool :=
+  self.out.isOk
+
+def monitorJob (ctx : MonitorContext) (job : Job α) : BaseIO (BuildResult α) := do
+  let result ← monitorJobs' ctx #[job]
+  if result.isOk then
+    if let some a ← job.wait? then
+      return {toMonitorResult := result, out := .ok a}
     else
-      error "build failed"
+      -- Computation job failed but was unreported in the monitor. This should be impossible.
+      return {toMonitorResult := result, out := .error <|
+        "uncaught top-level build failure (this is likely a bug in Lake)"}
+  else
+    return {toMonitorResult := result, out := .error "build failed"}
+
+def monitorFetchM
+  (mctx : MonitorContext) (bctx : BuildContext) (build : FetchM α)
+  (caption := "job computation")
+: BaseIO (BuildResult α) := do
+  let compute := Job.async build (caption := caption)
+  let job ← compute.run.run'.run bctx |>.run nilTrace
+  monitorJob mctx job
+
+def Workspace.finalizeBuild
+  (ws : Workspace) (cfg : BuildConfig) (ctx : MonitorContext) (result : BuildResult α)
+: IO α := do
+  reportResult cfg ctx.out result
+  if let some outputsFile := cfg.outputsFile? then
+    ws.saveOutputs (logger := ctx.logger) ctx.out outputsFile (cfg.verbosity matches .verbose)
+  if cfg.noBuild && result.didBuild then
+    IO.Process.exit noBuildCode.toUInt8
+  else
+    IO.ofExcept result.out
+
+def mkBuildContext' (ws : Workspace) (cfg : BuildConfig) (jobs : JobQueue) : BuildContext where
+  opaqueWs := ws
+  toBuildConfig := cfg
+  registeredJobs := jobs
+  leanTrace := .ofHash (pureHash ws.lakeEnv.leanGithash)
+    s!"Lean {Lean.versionStringCore}, commit {ws.lakeEnv.leanGithash}"
+
+/--
+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
+failing build jobs (e.g., when using `-q` or non-verbose `--no-build`).
+-/
+public def Workspace.runFetchM
+  (ws : Workspace) (build : FetchM α) (cfg : BuildConfig := {}) (caption := "job computation")
+: IO α := do
+  let jobs ← mkJobQueue
+  let mctx ← mkMonitorContext cfg jobs
+  let bctx := mkBuildContext' ws cfg jobs
+  let result ← monitorFetchM mctx bctx build caption
+  ws.finalizeBuild cfg mctx result
+
+def monitorBuild
+  (mctx : MonitorContext) (bctx : BuildContext) (build : FetchM (Job α))
+  (caption := "job computation")
+: BaseIO (BuildResult α) := do
+  let result ← monitorFetchM mctx bctx build caption
+   match result.out with
+  | .ok job =>
+    if let some a ← job.wait? then
+      return {result with out := .ok a}
+    else
+      -- Job failed but was unreported in the monitor. It was likely not properly registered.
+      return {result with out := .error <|
+        "uncaught top-level build failure (this is likely a bug in the build script)"}
+  | .error e =>
+    return {result with out := .error e}
+
+/--
+Returns whether a build is needed to validate `build`. Does not report on the attempted build.
+
+This is equivalent to checking whether `lake build --no-build` exits with code 0.
+-/
+@[inline] public def Workspace.checkNoBuild
+  (ws : Workspace) (build : FetchM (Job α))
+: BaseIO Bool := do
+  let jobs ← mkJobQueue
+  let cfg := {noBuild := true}
+  let mctx ← mkMonitorContext cfg jobs
+  let bctx := mkBuildContext' ws cfg jobs
+  let result ← monitorBuild mctx bctx build
+  return result.isOk && !result.didBuild
 
 /-- Run a build function in the Workspace's context and await the result. -/
 @[inline] public def Workspace.runBuild
   (ws : Workspace) (build : FetchM (Job α)) (cfg : BuildConfig := {})
 : IO α := do
-  let job ← ws.runFetchM build cfg
-  let some a ← job.wait? | error "build failed"
-  return a
+  let jobs ← mkJobQueue
+  let mctx ← mkMonitorContext cfg jobs
+  let bctx := mkBuildContext' ws cfg jobs
+  let result ← monitorBuild mctx bctx build
+  ws.finalizeBuild cfg mctx result
 
 /-- Produce a build job in the Lake monad's workspace and await the result. -/
 @[inline] public def runBuild
   (build : FetchM (Job α)) (cfg : BuildConfig := {})
-: LakeT IO α := do
-  (← getWorkspace).runBuild build cfg
+: LakeT IO α := do (← getWorkspace).runBuild build cfg

src/lake/Lake/CLI.lean

@@ -13,6 +13,7 @@ public import Lake.CLI.Help
 public import Lake.CLI.Init
 public import Lake.CLI.Main
 public import Lake.CLI.Serve
+public import Lake.CLI.Shake
 public import Lake.CLI.Translate
 public import Lake.CLI.Translate.Lean
 public import Lake.CLI.Translate.Toml