Job Registration

@[inline]

def Lake.JobState.renew (s : JobState) : JobState

Resets the job state after a checkpoint (e.g., registering the job). Preserves state that downstream jobs want to depend on while resetting job-local state that should not be inherited by downstream jobs.

Equations

• s.renew = { log := ∅, action := Lake.JobAction.unknown, trace := s.trace }

def Lake.Job.renew {α : Type u_1} (self : Job α) : Job α

Resets the job's state after a checkpoint (e.g., registering the job). Preserves information that downstream jobs want to depend on while resetting job-local information that should not be inherited by downstream jobs.

Equations

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

@[inline]

def Lake.registerJob {m : Type → Type} {α : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadBuild m] (caption : String) (job : Job α) (optional : Bool := false) : m (Job α)

Registers the job for the top-level build monitor, (e.g., the Lake CLI progress UI), assigning it caption.

Equations

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

def Lake.ensureJob {α : Type} (x : FetchM (Job α)) : FetchM (Job α)

Wraps stray I/O, logs, and errors in x into the produced job.

Equations

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

def Lake.withRegisterJob {α : Type} (caption : String) (x : FetchM (Job α)) (optional : Bool := false) : FetchM (Job α)

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.

Equations

• Lake.withRegisterJob caption x optional = do let job ← Lake.ensureJob x Lake.registerJob caption job optional

@[inline]

def Lake.maybeRegisterJob {α : Type} (caption : String) (job : Job α) : FetchM (Job α)

Registers the produced job for the top-level build monitor if it is not already (i.e., it has an empty caption).

Equations

• Lake.maybeRegisterJob caption job = if job.caption.isEmpty = true then Lake.registerJob caption job else pure job