Job Monad

This module contains additional definitions for Lake Job. In particular, it defines JobM, which uses BuildContext, which contains OpaqueJobs, hence the module split.

@[reducible, inline]

abbrev Lake.JobM (α : Type) : Type

The monad of asynchronous Lake jobs.

While this can be lifted into FetchM, job action should generally be wrapped into an asynchronous job (e.g., via Job.async) instead of being run directly in FetchM.

Equations

• Lake.JobM = Lake.FetchT (Lake.EStateT Lake.Log.Pos Lake.JobState BaseIO)

@[inline]

def Lake.JobM.ofFn {α : Type} (f : IndexBuildFn RecBuildM → Option Package → CallStack BuildKey → IO.Ref BuildStore → BuildContext → JobState → BaseIO (EResult Log.Pos JobState α)) : JobM α

Construct a FetchM monad from its full functional representation.

Equations

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

@[inline]

def Lake.JobM.toFn {α : Type} (self : JobM α) : IndexBuildFn RecBuildM → Option Package → CallStack BuildKey → IO.Ref BuildStore → BuildContext → JobState → BaseIO (EResult Log.Pos JobState α)

Convert a JobM monad to its full functional representation.

Equations

• self.toFn fetch pkg? stack store ctx s = Lake.EStateT.run s (Lake.EquipT.run self fetch pkg? stack store ctx)

@[instance 10000]

instance Lake.instMonadStateOfJobStateJobM : MonadStateOf JobState JobM

Equations

• Lake.instMonadStateOfJobStateJobM = inferInstance

instance Lake.instMonadStateOfLogJobM : MonadStateOf Log JobM

Equations

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

instance Lake.instMonadLogJobM : MonadLog JobM

Equations

• Lake.instMonadLogJobM = Lake.MonadLog.ofMonadState

instance Lake.instMonadErrorJobM : MonadError JobM

Equations

• Lake.instMonadErrorJobM = Lake.ELog.monadError

instance Lake.instAlternativeJobM : Alternative JobM

Equations

• Lake.instAlternativeJobM = Lake.ELog.alternative

instance Lake.instMonadLiftLogIOJobM : MonadLift LogIO JobM

Equations

• Lake.instMonadLiftLogIOJobM = { monadLift := fun {α : Type} => Lake.ELogT.takeAndRun }

@[inline]

def Lake.updateAction (action : JobAction) : JobM PUnit

Record that this job is trying to perform some action.

Equations

• Lake.updateAction action = modify fun (s : Lake.JobState) => { log := s.log, action := s.action.merge action, trace := s.trace, buildTime := s.buildTime }

@[inline]

def Lake.getTrace : JobM BuildTrace

Returns the current job's build trace.

Equations

• Lake.getTrace = (fun (x : Lake.JobState) => x.trace) <$> get

@[inline]

def Lake.setTrace (trace : BuildTrace) : JobM PUnit

Sets the current job's build trace.

Equations

• Lake.setTrace trace = modify fun (s : Lake.JobState) => { log := s.log, action := s.action, trace := trace, buildTime := s.buildTime }

@[inline]

def Lake.newTrace (caption : String := "<nil>") : JobM PUnit

Replace the job's build trace with a new empty trace.

Equations

• Lake.newTrace caption = Lake.setTrace (Lake.BuildTrace.nil caption)

@[inline]

def Lake.modifyTrace (f : BuildTrace → BuildTrace) : JobM PUnit

Mutates the job's trace, applying f to it.

Equations

• Lake.modifyTrace f = modify fun (s : Lake.JobState) => { log := s.log, action := s.action, trace := f s.trace, buildTime := s.buildTime }

@[inline]

def Lake.setTraceCaption (caption : String) : JobM PUnit

Set the caption of the job's build trace.

Equations

• Lake.setTraceCaption caption = Lake.modifyTrace fun (x : Lake.BuildTrace) => { caption := caption, inputs := x.inputs, hash := x.hash, mtime := x.mtime }

@[inline]

def Lake.takeTrace : JobM BuildTrace

Returns the current job's build trace and removes it from the state.

Equations

• Lake.takeTrace = modifyGet fun (s : Lake.JobState) => (s.trace, { log := s.log, action := s.action, trace := Lake.nilTrace, buildTime := s.buildTime })

@[inline]

def Lake.swapTrace (trace : BuildTrace) : JobM BuildTrace

Sets the current job's trace and returns the previous one.

Equations

• Lake.swapTrace trace = modifyGet fun (s : Lake.JobState) => (s.trace, { log := s.log, action := s.action, trace := trace, buildTime := s.buildTime })

@[inline]

def Lake.addTrace (trace : BuildTrace) : JobM PUnit

Mix a trace into the current job's build trace.

Equations

• Lake.addTrace trace = Lake.modifyTrace fun (x : Lake.BuildTrace) => x.mix trace

@[inline]

def Lake.addSubTrace {α : Type} (caption : String) (x : JobM α) : JobM α

Runs x with a new trace and then mixes it into the original trace.

Equations

• Lake.addSubTrace caption x = do let oldTrace ← Lake.swapTrace (Lake.BuildTrace.nil caption) let a ← x Lake.modifyTrace fun (x : Lake.BuildTrace) => oldTrace.mix x pure a

@[reducible, inline]

abbrev Lake.SpawnM (α : Type) : Type

The monad used to spawn asynchronous Lake build jobs. Lifts into FetchM.

Equations

• Lake.SpawnM = Lake.FetchT (ReaderT Lake.BuildTrace BaseIO)

@[inline]

def Lake.SpawnM.ofFn {α : Type} (f : IndexBuildFn RecBuildM → Option Package → CallStack BuildKey → IO.Ref BuildStore → BuildContext → BuildTrace → BaseIO α) : SpawnM α

Construct a SpawnM monad from its full functional representation.

Equations

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

@[inline]

def Lake.SpawnM.toFn {α : Type} (self : SpawnM α) : IndexBuildFn RecBuildM → Option Package → CallStack BuildKey → IO.Ref BuildStore → BuildContext → BuildTrace → BaseIO α

Convert a SpawnM monad to its full functional representation.

Equations

• self.toFn fetch pkg? stack store ctx s = (Lake.EquipT.run self fetch pkg? stack store ctx).run s

@[inline]

def Lake.JobM.runSpawnM {α : Type} (x : SpawnM α) : JobM α

Equations

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

instance Lake.instMonadLiftSpawnMJobM : MonadLift SpawnM JobM

Equations

• Lake.instMonadLiftSpawnMJobM = { monadLift := fun {α : Type} => Lake.JobM.runSpawnM }

@[inline]

def Lake.FetchM.runJobM {α : Type} (x : JobM α) : FetchM α

Run a JobM action in FetchM.

Generally, this should not be done, and instead a job action should be run asynchronously in a Job (e.g., via Job.async).

Equations

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

instance Lake.instMonadLiftJobMFetchM : MonadLift JobM FetchM

Equations

• Lake.instMonadLiftJobMFetchM = { monadLift := fun {α : Type} => Lake.FetchM.runJobM }

@[inline]

def Lake.JobM.runFetchM {α : Type} (x : FetchM α) : JobM α

Run a FetchM action in JobM.

Equations

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

instance Lake.instMonadLiftFetchMJobM : MonadLift FetchM JobM

Equations

• Lake.instMonadLiftFetchMJobM = { monadLift := fun {α : Type} => Lake.JobM.runFetchM }

@[inline]

def Lake.Job.bindTask {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] [OptDataKind β] (f : JobTask α → m (JobTask β)) (self : Job α) : m (Job β)

Equations

• Lake.Job.bindTask f self = do let __do_lift ← f self.task pure { task := __do_lift, kind := inferInstance, caption := self.caption, optional := self.optional }

@[inline]

def Lake.Job.async {α : Type} [OptDataKind α] (act : JobM α) (prio : Task.Priority := Task.Priority.default) (caption : String := "") : SpawnM (Job α)

Spawn a job that asynchronously performs act.

Equations

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

@[inline]

def Lake.Job.wait {α : Type} (self : Job α) : BaseIO (JobResult α)

Wait for a job to complete and return the result.

Equations

• self.wait = IO.wait self.task

@[inline]

def Lake.Job.wait? {α : Type} (self : Job α) : BaseIO (Option α)

Wait for a job to complete and return the produced value. If an error occurred, return none and discarded any logs produced.

Equations

• self.wait? = do let __do_lift ← self.wait pure (Lake.EResult.result? __do_lift)

@[inline]

def Lake.Job.await {α : Type} (self : Job α) : LogIO α

Wait for a job to complete and return the produced value. Logs the job's log and throws if there was an error.

Equations

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

def Lake.Job.mapM {β : Type} {α : Type u_1} [kind : OptDataKind β] (self : Job α) (f : α → JobM β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : SpawnM (Job β)

Apply f asynchronously to the job's output.

Equations

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

def Lake.Job.bindM {β : Type} {α : Type u_1} [kind : OptDataKind β] (self : Job α) (f : α → JobM (Job β)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : SpawnM (Job β)

Apply f asynchronously to the job's output and asynchronously await the resulting job.

Equations

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

@[inline]

def Lake.Job.zipResultWith {γ : Type u_1} {α : Type u_2} {β : Type u_3} [OptDataKind γ] (f : JobResult α → JobResult β → JobResult γ) (self : Job α) (other : Job β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := true) : Job γ

a.zipWith f b produces a new job c that applies f to the results of a and b. The job c errors if either a or b error.

Equations

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

@[inline]

def Lake.Job.zipWith {γ : Type u_1} {α : Type u_2} {β : Type u_3} [OptDataKind γ] (f : α → β → γ) (self : Job α) (other : Job β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := true) : Job γ

a.zipWith f b produces a new job c that applies f to the results of a and b. The job c errors if either a or b error.

Equations

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

def Lake.Job.add {α : Type u_1} {β : Type u_2} (self : Job α) (other : Job β) : Job α

Merges this job with another, discarding its output and trace.

Equations

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

def Lake.Job.mix {α : Type u_1} {β : Type u_2} (self : Job α) (other : Job β) : Job Unit

Merges this job with another, discarding both outputs.

Equations

• self.mix other = Lake.Job.zipWith (fun (x : α) (x : β) => ()) self other

def Lake.Job.mixList {α : Type u_1} (jobs : List (Job α)) (traceCaption : String := "<collection>") : Job Unit

Merge a List of jobs into one, discarding their outputs.

Equations

• Lake.Job.mixList jobs traceCaption = List.foldr (fun (x1 : Lake.Job α) (x2 : Lake.Job Unit) => x1.mix x2) (Lake.Job.traceRoot () traceCaption) jobs

def Lake.Job.mixArray {α : Type u_1} (jobs : Array (Job α)) (traceCaption : String := "<collection>") : Job Unit

Merge an Array of jobs into one, discarding their outputs.

Equations

• Lake.Job.mixArray jobs traceCaption = Array.foldl (fun (x1 : Lake.Job Unit) (x2 : Lake.Job α) => x1.mix x2) (Lake.Job.traceRoot () traceCaption) jobs

def Lake.Job.collectList {α : Type u_1} (jobs : List (Job α)) (traceCaption : String := "<collection>") : Job (List α)

Merge a List of jobs into one, collecting their outputs into a List.

Equations

• Lake.Job.collectList jobs traceCaption = List.foldr (fun (self : Lake.Job α) (other : Lake.Job (List α)) => Lake.Job.zipWith List.cons self other) (Lake.Job.traceRoot [] traceCaption) jobs

def Lake.Job.collectArray {α : Type u_1} (jobs : Array (Job α)) (traceCaption : String := "<collection>") : Job (Array α)

Merge an Array of jobs into one, collecting their outputs into an Array.

Equations

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