Build Runner

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

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

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

def Lake.Monitor.spinnerFrames : Array Char

Unicode icons that make up the spinner in animation order.

structure Lake.MonitorContext : Type

Context of the Lake build monitor.

• jobs : IO.Ref (Array OpaqueJob)
• out : IO.FS.Stream
• outLv : LogLevel
• failLv : LogLevel
• minAction : JobAction
• showOptional : Bool
• useAnsi : Bool
• showProgress : Bool
• updateFrequency : Nat

  How often to poll jobs (in milliseconds).

structure Lake.MonitorState : Type

State of the Lake build monitor.

• jobNo : Nat
• totalJobs : Nat
• failures : Array String
• resetCtrl : String
• lastUpdate : Nat
• spinnerIdx : Fin Monitor.spinnerFrames.size

@[reducible, inline]

abbrev Lake.MonitorM (α : Type) : Type

Monad of the Lake build monitor.

@[inline]

def Lake.MonitorM.run {α : Type} (ctx : MonitorContext) (s : MonitorState) (self : MonitorM α) : BaseIO (α × MonitorState)

def Lake.Ansi.resetLine : String

The ANSI escape sequence for clearing the current line and resetting the cursor back to the start.

@[inline]

def Lake.flush (out : IO.FS.Stream) : BaseIO PUnit

Like IO.FS.Stream.flush, but ignores errors.

@[inline]

def Lake.print! (out : IO.FS.Stream) (s : String) : BaseIO PUnit

Like IO.FS.Stream.putStr, but panics on errors.

@[inline]

def Lake.Monitor.print (s : String) : MonitorM PUnit

@[inline]

def Lake.Monitor.flush : MonitorM PUnit

def Lake.Monitor.renderProgress (running unfinished : Array OpaqueJob) (h : 0 < unfinished.size) : MonitorM PUnit

def Lake.Monitor.reportJob (job : OpaqueJob) : MonitorM PUnit

def Lake.Monitor.poll (unfinished : Array OpaqueJob) : MonitorM (Array OpaqueJob × Array OpaqueJob)

def Lake.Monitor.sleep : MonitorM PUnit

partial def Lake.Monitor.loop (unfinished : Array OpaqueJob) : MonitorM PUnit

def Lake.Monitor.main (init : Array OpaqueJob) : MonitorM PUnit

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

The job monitor function. An auxiliary definition for runFetchM.

def Lake.Workspace.saveInputs (ws : Workspace) : LogIO Unit

Save input mappings to the local Lake artifact cache (if enabled).

def Lake.Workspace.runFetchM {α : Type} (ws : Workspace) (build : FetchM α) (cfg : BuildConfig := { }) : 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).

@[inline]

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.