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.

source

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

Instances For

source

@[instance 10000]

instance Lake.instMonadStateOfJobStateJobM :

MonadStateOf JobState JobM

Equations

Lake.instMonadStateOfJobStateJobM = inferInstance

source

instance Lake.instMonadStateOfLogJobM :

MonadStateOf Log JobM

Equations

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

source

instance Lake.instMonadLogJobM :

MonadLog JobM

Equations

Lake.instMonadLogJobM = Lake.MonadLog.ofMonadState

source

instance Lake.instMonadErrorJobM :

MonadError JobM

Equations

Lake.instMonadErrorJobM = Lake.ELog.monadError

source

instance Lake.instAlternativeJobM :

Alternative JobM

Equations

Lake.instAlternativeJobM = Lake.ELog.alternative

source

instance Lake.instMonadLiftLogIOJobM :

MonadLift LogIO JobM

Equations

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

source

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

source

@[inline]

def Lake.getTrace :

JobM BuildTrace

Returns the current job's build trace.

Equations

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

source

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

source

@[inline]

def Lake.addTrace (trace : BuildTrace) :

JobM PUnit

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

Equations

Lake.addTrace trace = modify fun (s : Lake.JobState) => { log := s.log, action := s.action, trace := s.trace.mix trace }

source

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

source

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

Instances For

Lake.instMonadLiftSpawnMJobM

source

@[inline]

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

JobM α

Equations

Lake.JobM.runSpawnM x fn stack store ctx s = do let __do_lift ← x fn stack store ctx s.trace pure (Lake.EResult.ok __do_lift s)

source

instance Lake.instMonadLiftSpawnMJobM :

MonadLift SpawnM JobM

Equations

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

source

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

source

instance Lake.instMonadLiftJobMFetchM :

MonadLift JobM FetchM

Equations

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

source

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

source

instance Lake.instMonadLiftFetchMJobM :

MonadLift FetchM JobM

Equations

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

source

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

source

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

Lake.Job.async act prio caption fetch stack store ctx = (fun (task : Lake.JobTask α) => Lake.Job.ofTask task caption) <$> liftM ((Lake.withLoggedIO act fetch stack store ctx { }).asTask prio)

source

@[inline]

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

BaseIO (JobResult α)

Wait a the job to complete and return the result.

Equations

self.wait = IO.wait self.task

source

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

source

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

source

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.

source

@[reducible, inline, deprecated Lake.Job.mapM (since := "2024-12-06")]

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

SpawnM (Job β)

Equations

self.bindSync f prio sync = self.mapM f prio sync

source

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.

source

@[reducible, inline, deprecated Lake.Job.bindM (since := "2024-12-06")]

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

SpawnM (Job β)

Equations

self.bindAsync f prio sync = self.bindM (fun (a : α) => liftM (f a)) prio sync

source

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

source

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