@[inline]

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

Equations

• Lake.Job.pure a = { task := { get := Lake.EResult.ok a ∅ } }

instance Lake.Job.instPure : Pure Lake.Job

Equations

• Lake.Job.instPure = { pure := fun {α : Type u_1} => Lake.Job.pure }

instance Lake.Job.instInhabited {α : Type u_1} [Inhabited α] : Inhabited (Lake.Job α)

Equations

• Lake.Job.instInhabited = { default := pure default }

@[inline]

def Lake.Job.nop : Lake.Job Unit

Equations

• Lake.Job.nop = pure ()

@[inline]

def Lake.Job.error {α : Type u_1} (l : Lake.Log) : Lake.Job α

Equations

• Lake.Job.error l = { task := { get := Lake.EResult.error 0 l } }

@[inline]

def Lake.Job.mapResult {α : Type u_1} {β : Type u_2} (f : Lake.JobResult α → Lake.JobResult β) (self : Lake.Job α) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) : Lake.Job β

Equations

• Lake.Job.mapResult f self prio sync = { task := Task.map f self.task prio sync }

@[inline]

def Lake.Job.map {α : Type u_1} {β : Type u_2} (f : α → β) (self : Lake.Job α) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) : Lake.Job β

Equations

• Lake.Job.map f self prio sync = Lake.Job.mapResult (fun (x : Lake.JobResult α) => Lake.EResult.map f x) self prio sync

instance Lake.Job.instFunctor : Functor Lake.Job

Equations

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

@[inline]

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

Equations

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

@[inline]

def Lake.Job.attempt {α : Type u_1} (self : Lake.Job α) : Lake.Job Bool

Equations

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

@[inline]

def Lake.Job.attempt? {α : Type u_1} (self : Lake.Job α) : Lake.Job (Option α)

Equations

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

@[inline]

def Lake.Job.async {α : Type} (act : Lake.JobM α) (prio : optParam Task.Priority Task.Priority.default) : Lake.SpawnM (Lake.Job α)

Spawn a job that asynchronously performs act.

Equations

• Lake.Job.async act prio ctx = Lake.Job.mk <$> (act ctx ∅).asTask prio

@[inline]

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

Wait a the job to complete and return the result.

Equations

• self.wait = IO.wait self.task

@[inline]

def Lake.Job.wait? {α : Type} (self : Lake.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 : Lake.Job α) : Lake.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.

@[inline]

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

let c ← a.bindSync b asynchronously performs the action b after the job a completes.

Equations

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

@[inline]

def Lake.Job.bindAsync {α : Type u_1} {β : Type} (self : Lake.Job α) (f : α → Lake.SpawnM (Lake.Job β)) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) : Lake.SpawnM (Lake.Job β)

let c ← a.bindAsync b asynchronously performs the action b after the job a completes and then merges into the job produced by b.

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} (f : α → β → γ) (x : Lake.Job α) (y : Lake.Job β) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) : BaseIO (Lake.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.withRegisterJob {m : Type → Type u_1} {α : Type} [Monad m] [MonadReaderOf Lake.BuildContext m] [MonadLiftT BaseIO m] (caption : String) (x : m (Lake.Job α)) : m (Lake.Job α)

Register the produced job for the CLI progress UI.

Equations

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

@[reducible, inline]

abbrev Lake.BuildJob (α : Type u_1) : Type u_1

A Lake build job.

Equations

• Lake.BuildJob α = Lake.Job (α × Lake.BuildTrace)

@[inline]

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

Equations

• Lake.BuildJob.mk job = job

@[inline]

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

Equations

• Lake.BuildJob.ofJob self = Lake.BuildJob.mk ((fun (x : Lake.BuildTrace) => ((), x)) <$> self)

@[inline]

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

Equations

• self.toJob = self

@[inline]

def Lake.BuildJob.nil : Lake.BuildJob Unit

Equations

• Lake.BuildJob.nil = Lake.BuildJob.mk (pure ((), Lake.nilTrace))

@[inline]

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

Equations

• Lake.BuildJob.pure a = Lake.BuildJob.mk (pure (a, Lake.nilTrace))

instance Lake.BuildJob.instPure : Pure Lake.BuildJob

Equations

• Lake.BuildJob.instPure = { pure := fun {α : Type u_1} => Lake.BuildJob.pure }

@[inline]

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

Equations

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

@[inline]

def Lake.BuildJob.attempt? {α : Type u_1} (self : Lake.BuildJob α) : Lake.BuildJob (Option α)

Equations

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

@[inline]

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

Equations

• Lake.BuildJob.map f self = Lake.BuildJob.mk ((fun (x : α × Lake.BuildTrace) => match x with | (a, t) => (f a, t)) <$> self.toJob)

instance Lake.BuildJob.instFunctor : Functor Lake.BuildJob

Equations

• Lake.BuildJob.instFunctor = { map := fun {α β : Type u_1} => Lake.BuildJob.map, mapConst := fun {α β : Type u_1} => Lake.BuildJob.map ∘ Function.const β }

@[inline]

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

Equations

• Lake.BuildJob.mapWithTrace f self = Lake.BuildJob.mk ((fun (x : α × Lake.BuildTrace) => match x with | (a, t) => f a t) <$> self.toJob)

@[inline]

def Lake.BuildJob.bindSync {α : Type u_1} {β : Type} (self : Lake.BuildJob α) (f : α → Lake.BuildTrace → Lake.JobM β) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) : Lake.SpawnM (Lake.Job β)

Equations

• self.bindSync f prio sync = self.toJob.bindSync (fun (x : α × Lake.BuildTrace) => match x with | (a, t) => f a t) prio sync

@[inline]

def Lake.BuildJob.bindAsync {α : Type u_1} {β : Type} (self : Lake.BuildJob α) (f : α → Lake.BuildTrace → Lake.SpawnM (Lake.Job β)) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) : Lake.SpawnM (Lake.Job β)

Equations

• self.bindAsync f prio sync = self.toJob.bindAsync (fun (x : α × Lake.BuildTrace) => match x with | (a, t) => f a t) prio sync

@[inline]

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

Equations

• self.wait? = (fun (x : Option (α × Lake.BuildTrace)) => Option.map (fun (x : α × Lake.BuildTrace) => x.fst) x) <$> self.toJob.wait?

def Lake.BuildJob.add {α : Type} {β : Type u_1} (t1 : Lake.BuildJob α) (t2 : Lake.BuildJob β) : BaseIO (Lake.BuildJob α)

Equations

• t1.add t2 = Lake.BuildJob.mk <$> Lake.Job.zipWith (fun (a : α × Lake.BuildTrace) (x : β × Lake.BuildTrace) => a) t1.toJob t2.toJob Task.Priority.default

def Lake.BuildJob.mix {α : Type u_1} {β : Type u_2} (t1 : Lake.BuildJob α) (t2 : Lake.BuildJob β) : BaseIO (Lake.BuildJob Unit)

Equations

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

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

Equations

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

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

Equations

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

def Lake.BuildJob.zipWith {α : Type u_1} {β : Type u_2} {γ : Type} (f : α → β → γ) (t1 : Lake.BuildJob α) (t2 : Lake.BuildJob β) : BaseIO (Lake.BuildJob γ)

Equations

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

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

Equations

• Lake.BuildJob.collectList jobs = List.foldrM (Lake.BuildJob.zipWith List.cons) (pure []) jobs

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

Equations

• Lake.BuildJob.collectArray jobs = Array.foldlM (Lake.BuildJob.zipWith Array.push) (pure #[]) jobs 0