# Job Registration #

source
@[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 = { trace := s.trace.withoutInputs }

Instances For

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

Instances For

source
@[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.

Instances For

source
def Lake.ensureJob {α : Type} [OptDataKind α] (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.

Instances For

source
@[inline]
def Lake.withRegisterJob {α : Type} [OptDataKind α] (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

Instances For

source
@[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

Instances For