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.

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.

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

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

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

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

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