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 : Lake.Workspace) (config : Lake.BuildConfig) : BaseIO Lake.BuildContext

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

Equations

• One or more equations did not get rendered due to their size.

def Lake.Monitor.spinnerFrames : Array Char

Unicode icons that make up the spinner in animation order.

Equations

• Lake.Monitor.spinnerFrames = #['⣾', '⣷', '⣯', '⣟', '⡿', '⢿', '⣻', '⣽']

structure Lake.MonitorContext : Type

Context of the Lake build monitor.

• totalJobs : Nat
• out : IO.FS.Stream
• outLv : Lake.LogLevel
• failLv : Lake.LogLevel
• minAction : Lake.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
• failures : Array String
• resetCtrl : String
• lastUpdate : Nat
• spinnerIdx : Fin Lake.Monitor.spinnerFrames.size

@[reducible, inline]

abbrev Lake.MonitorM (α : Type) : Type

Monad of the Lake build monitor.

Equations

• Lake.MonitorM = ReaderT Lake.MonitorContext (StateT Lake.MonitorState BaseIO)

@[inline]

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

Equations

• Lake.MonitorM.run ctx s self = self ctx s

def Lake.Ansi.resetLine : String

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

Equations

• Lake.Ansi.resetLine = "\x1b[2K\x0d"

@[inline]

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

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

Equations

• Lake.flush out = EIO.catchExceptions out.flush fun (x : IO.Error) => pure ()

@[inline]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• Lake.Monitor.print s = do let __do_lift ← read liftM (Lake.print! __do_lift.out s)

@[inline]

def Lake.Monitor.flush : Lake.MonitorM PUnit

Equations

• Lake.Monitor.flush = do let __do_lift ← read liftM (Lake.flush __do_lift.out)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Lake.Monitor.sleep : Lake.MonitorM PUnit

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

The job monitor function. An auxiliary definition for runFetchM.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Workspace.runFetchM {α : Type} (ws : Lake.Workspace) (build : Lake.FetchM α) (cfg : Lake.BuildConfig := { oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal, failLv := Lake.LogLevel.error, outLv := Lake.Verbosity.normal.minLogLv, out := Lake.OutStream.stderr, ansiMode := Lake.AnsiMode.auto }) : 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).

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.Workspace.runBuild {α : Type} (ws : Lake.Workspace) (build : Lake.FetchM (Lake.BuildJob α)) (cfg : Lake.BuildConfig := { oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal, failLv := Lake.LogLevel.error, outLv := Lake.Verbosity.normal.minLogLv, out := Lake.OutStream.stderr, ansiMode := Lake.AnsiMode.auto }) : IO α

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

Equations

• ws.runBuild build cfg = do let job ← ws.runFetchM build cfg let __discr ← liftM job.wait? match __discr with | some a => pure a | x => Lake.error "build failed"

@[inline]

def Lake.runBuild {α : Type} (build : Lake.FetchM (Lake.BuildJob α)) (cfg : Lake.BuildConfig := { oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal, failLv := Lake.LogLevel.error, outLv := Lake.Verbosity.normal.minLogLv, out := Lake.OutStream.stderr, ansiMode := Lake.AnsiMode.auto }) : Lake.LakeT IO α

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

Equations

• Lake.runBuild build cfg = do let __do_lift ← Lake.getWorkspace liftM (__do_lift.runBuild build cfg)