Build Runner

This module defines the top-level functions used to execute a Lake build, monitor its progress, and await the result.

@[deprecated "Deprecated without replacement." (since := "2025-01-08")]

def Lake.mkBuildContext (ws : Workspace) (config : BuildConfig) : BaseIO BuildContext

Create a fresh build context from a workspace and a build configuration.

structure Lake.MonitorResult : Type

For internal use only.

• wantsRebuild : Bool
• failures : Array String
• numJobs : Nat

@[inline, deprecated "Deprecated without replacement." (since := "2025-01-08")]

def Lake.monitorJobs (initJobs : Array OpaqueJob) (jobs : IO.Ref (Array OpaqueJob)) (out : IO.FS.Stream) (failLv outLv : LogLevel) (minAction : JobAction) (showOptional useAnsi showProgress showTime : Bool) (resetCtrl : String := "") (initFailures : Array String := #[]) (updateFrequency : Nat := 100) : BaseIO MonitorResult

The job monitor function. An auxiliary definition for runFetchM.

def Lake.noBuildCode : ExitCode

Exit code to return if --no-build is set and a build is required.

def Lake.Workspace.runFetchM {α : Type} (ws : Workspace) (build : FetchM α) (cfg : BuildConfig := { }) (caption : String := "job computation") : IO α

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).

def Lake.Workspace.checkNoBuild {α : Type} (ws : Workspace) (build : FetchM (Job α)) : BaseIO Bool

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.

def Lake.Workspace.runBuild {α : Type} (ws : Workspace) (build : FetchM (Job α)) (cfg : BuildConfig := { }) : IO α

Run a build function in the Workspace's context and await the result.

@[inline]

def Lake.runBuild {α : Type} (build : FetchM (Job α)) (cfg : BuildConfig := { }) : LakeT IO α

Produce a build job in the Lake monad's workspace and await the result.