Lake.Build.Job

source

@[inline, reducible]

abbrev Lake.Job (α : Type u_1) :

Type u_1

A Lake job.

Instances For

source

@[inline, reducible]

abbrev Lake.JobM (α : Type) :

Type

The monad of Lake jobs.

Instances For

source

@[inline, reducible]

abbrev Lake.ResultM :

Type → Type

The monad of a finished Lake job.

Instances For

source

@[inline]

def Lake.Job.nil :

Lake.Job Unit

Instances For

source

@[inline]

def Lake.Job.async {α : Type} (act : Lake.JobM α) :

Lake.SchedulerM (Lake.Job α)

Instances For

source

@[inline]

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

Lake.ResultM α

Instances For

source

@[inline]

def Lake.Job.bindSync {α : Type} {β : Type} (self : Lake.Job α) (f : α → Lake.JobM β) (prio : optParam Task.Priority Task.Priority.default) :

Lake.SchedulerM (Lake.Job β)

Instances For

source

@[inline]

def Lake.Job.bindAsync {α : Type} {β : Type} (self : Lake.Job α) (f : α → Lake.SchedulerM (Lake.Job β)) :

Lake.SchedulerM (Lake.Job β)

Instances For

source

@[inline, reducible]

abbrev Lake.BuildJob (α : Type u_1) :

Type u_1

A Lake build job.

Instances For

source

@[inline]

def Lake.BuildJob.mk {α : Type u_1} (job : Lake.Job (α × Lake.BuildTrace)) :

Lake.BuildJob α

Instances For

source

@[inline]

def Lake.BuildJob.ofJob (self : Lake.Job Lake.BuildTrace) :

Lake.BuildJob Unit

Instances For

source

@[inline]

def Lake.BuildJob.toJob {α : Type u_1} (self : Lake.BuildJob α) :

Lake.Job (α × Lake.BuildTrace)

Instances For

source

@[inline]

def Lake.BuildJob.nil :

Lake.BuildJob Unit

Instances For

source

@[inline]

def Lake.BuildJob.pure {α : Type u_1} (a : α) :

Lake.BuildJob α

Instances For

source

instance Lake.BuildJob.instPureBuildJob :

Pure Lake.BuildJob

source

@[inline]

def Lake.BuildJob.map {α : Type u_1} {β : Type u_1} (f : α → β) (self : Lake.BuildJob α) :

Lake.BuildJob β

Instances For

source

instance Lake.BuildJob.instFunctorBuildJob :

Functor Lake.BuildJob

source

@[inline]

def Lake.BuildJob.mapWithTrace {α : Type u_1} {β : Type u_1} (f : α → Lake.BuildTrace → β × Lake.BuildTrace) (self : Lake.BuildJob α) :

Lake.BuildJob β

Instances For

source

@[inline]

def Lake.BuildJob.bindSync {α : Type} {β : Type} (self : Lake.BuildJob α) (f : α → Lake.BuildTrace → Lake.JobM β) (prio : optParam Task.Priority Task.Priority.default) :

Lake.SchedulerM (Lake.Job β)

Instances For

source

@[inline]

def Lake.BuildJob.bindAsync {α : Type} {β : Type} (self : Lake.BuildJob α) (f : α → Lake.BuildTrace → Lake.SchedulerM (Lake.Job β)) :

Lake.SchedulerM (Lake.Job β)

Instances For

source

@[inline]

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

Lake.ResultM α

Instances For

source

instance Lake.BuildJob.instAwaitBuildJobResultM :

Lake.Await Lake.BuildJob Lake.ResultM

source

@[inline]

def Lake.BuildJob.materialize {α : Type} (self : Lake.BuildJob α) :

Lake.ResultM Unit

Instances For

source

def Lake.BuildJob.mix {α : Type} {β : Type} (t1 : Lake.BuildJob α) (t2 : Lake.BuildJob β) :

BaseIO (Lake.BuildJob Unit)

Instances For

source

def Lake.BuildJob.mixList {α : Type} (jobs : List (Lake.BuildJob α)) :

BaseIO (Lake.BuildJob Unit)

Instances For

source

def Lake.BuildJob.mixArray {α : Type} (jobs : Array (Lake.BuildJob α)) :

BaseIO (Lake.BuildJob Unit)

Instances For

source

def Lake.BuildJob.seqWithAsync {α : Type} {β : Type} {γ : Type} (f : α → β → γ) (t1 : Lake.BuildJob α) (t2 : Lake.BuildJob β) :

BaseIO (Lake.BuildJob γ)

Instances For

source

instance Lake.BuildJob.instSeqWithAsyncBaseIOBuildJob :

Lake.SeqWithAsync BaseIO Lake.BuildJob

source

def Lake.BuildJob.collectList {α : Type} (jobs : List (Lake.BuildJob α)) :

BaseIO (Lake.BuildJob (List α))

Instances For

source

def Lake.BuildJob.collectArray {α : Type} (jobs : Array (Lake.BuildJob α)) :

BaseIO (Lake.BuildJob (Array α))

Instances For