def Lake.JobAction.verb (failed : Bool) : Lake.JobAction → String

Equations

• Lake.JobAction.verb failed Lake.JobAction.unknown = if failed = true then "Running" else "Ran"
• Lake.JobAction.verb failed Lake.JobAction.replay = if failed = true then "Replaying" else "Replayed"
• Lake.JobAction.verb failed Lake.JobAction.fetch = if failed = true then "Fetching" else "Fetched"
• Lake.JobAction.verb failed Lake.JobAction.build = if failed = true then "Building" else "Built"

@[inline]

def Lake.JobState.renew (s : Lake.JobState) : Lake.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.

Equations

• s.renew = { log := ∅, action := Lake.JobAction.unknown, trace := s.trace }

def Lake.JobState.merge (a b : Lake.JobState) : Lake.JobState

Equations

• a.merge b = { log := a.log ++ b.log, action := a.action.merge b.action, trace := Lake.mixTrace a.trace b.trace }

@[inline]

def Lake.JobState.modifyLog (f : Lake.Log → Lake.Log) (s : Lake.JobState) : Lake.JobState

Equations

• Lake.JobState.modifyLog f s = { log := f s.log, action := s.action, trace := s.trace }

def Lake.JobResult.prependLog {α : Type u_1} (log : Lake.Log) (self : Lake.JobResult α) : Lake.JobResult α

Add log entries to the beginning of the job's log.

Equations

• Lake.JobResult.prependLog log (Lake.EResult.ok a s) = Lake.EResult.ok a (Lake.JobState.modifyLog (fun (x : Lake.Log) => log ++ x) s)
• Lake.JobResult.prependLog log (Lake.EResult.error e s) = Lake.EResult.error { val := log.size + e.val } (Lake.JobState.modifyLog (fun (x : Lake.Log) => log ++ x) s)

@[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.BuildT (Lake.EStateT Lake.Log.Pos Lake.JobState BaseIO)

instance Lake.instMonadLiftLakeMBuildTOfPure {m : Type → Type u_1} [Pure m] : MonadLift Lake.LakeM (Lake.BuildT m)

Equations

• Lake.instMonadLiftLakeMBuildTOfPure = { monadLift := fun {α : Type} (x : Lake.LakeM α) (ctx : Lake.BuildContext) => pure (Lake.LakeM.run ctx.toContext x) }

instance Lake.instMonadStateOfLogJobM : MonadStateOf Lake.Log Lake.JobM

Equations

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

instance Lake.instMonadStateOfJobStateJobM : MonadStateOf Lake.JobState Lake.JobM

Equations

• Lake.instMonadStateOfJobStateJobM = inferInstance

instance Lake.instMonadLogJobM : Lake.MonadLog Lake.JobM

Equations

• Lake.instMonadLogJobM = Lake.MonadLog.ofMonadState

instance Lake.instMonadErrorJobM : Lake.MonadError Lake.JobM

Equations

• Lake.instMonadErrorJobM = Lake.ELog.monadError

instance Lake.instAlternativeJobM : Alternative Lake.JobM

Equations

• Lake.instAlternativeJobM = Lake.ELog.alternative

instance Lake.instMonadLiftLogIOJobM : MonadLift Lake.LogIO Lake.JobM

Equations

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

@[inline]

def Lake.updateAction (action : Lake.JobAction) : Lake.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 }

@[inline]

def Lake.getTrace : Lake.JobM Lake.BuildTrace

Returns the current job's build trace.

Equations

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

@[inline]

def Lake.setTrace (trace : Lake.BuildTrace) : Lake.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 }

@[inline]

def Lake.addTrace (trace : Lake.BuildTrace) : Lake.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 }

@[inline]

def Lake.takeTrace : Lake.JobM Lake.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 })

@[reducible, inline]

abbrev Lake.SpawnM (α : Type) : Type

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

Equations

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

@[inline]

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

Equations

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

instance Lake.instMonadLiftSpawnMJobM : MonadLift Lake.SpawnM Lake.JobM

Equations

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

@[reducible, inline, deprecated Lake.SpawnM (since := "2024-05-21")]

abbrev Lake.SchedulerM (α : Type) : Type

The monad used to spawn asynchronous Lake build jobs. Replaced by SpawnM.

Equations

• Lake.SchedulerM = Lake.SpawnM

@[implemented_by _private.Lake.Build.Job.0.Lake.Job.toOpaqueImpl]

def Lake.Job.toOpaque {α : Type u_1} (job : Lake.Job α) : Lake.OpaqueJob

Forget the value of a job. Implemented as a no-op cast.

Equations

• job.toOpaque = { task := Task.map (fun (x : Lake.JobResult α) => Lake.EResult.map Opaque.mk x) job.task, caption := job.caption, optional := job.optional }

instance Lake.instCoeOutJobOpaqueJob {α : Type u_1} : CoeOut (Lake.Job α) Lake.OpaqueJob

Equations

• Lake.instCoeOutJobOpaqueJob = { coe := Lake.Job.toOpaque }

@[inline]

def Lake.Job.ofTask {α : Type u_1} (task : Lake.JobTask α) (caption : String := "") : Lake.Job α

Equations

• Lake.Job.ofTask task caption = { task := task, caption := caption, optional := false }

@[inline]

def Lake.Job.error {α : Type u_1} (log : Lake.Log := ∅) (caption : String := "") : Lake.Job α

Equations

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

@[inline]

def Lake.Job.pure {α : Type u_1} (a : α) (log : Lake.Log := ∅) (caption : String := "") : Lake.Job α

Equations

• Lake.Job.pure a log caption = { task := { get := Lake.EResult.ok a { log := log, action := Lake.JobAction.unknown, trace := Lake.BuildTrace.nil } }, caption := caption, optional := false }

instance Lake.Job.instPure : Pure Lake.Job

Equations

• Lake.Job.instPure = { pure := fun {α : Type ?u.6} (a : α) => Lake.Job.pure a }

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

Equations

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

@[inline]

def Lake.Job.nop (log : Lake.Log := ∅) (caption : String := "") : Lake.Job Unit

Equations

• Lake.Job.nop log caption = Lake.Job.pure () log caption

@[inline]

def Lake.Job.nil : Lake.Job Unit

Equations

• Lake.Job.nil = Lake.Job.pure ()

@[inline]

def Lake.Job.setCaption {α : Type u_1} (caption : String) (job : Lake.Job α) : Lake.Job α

Sets the job's caption.

Equations

• Lake.Job.setCaption caption job = { task := job.task, caption := caption, optional := job.optional }

@[inline]

def Lake.Job.setCaption? {α : Type u_1} (caption : String) (job : Lake.Job α) : Lake.Job α

Sets the job's caption if the job's current caption is empty.

Equations

• Lake.Job.setCaption? caption job = if job.caption.isEmpty = true then { task := job.task, caption := caption, optional := job.optional } else job

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Lake.Job.map {α : Type u_1} {β : Type u_2} (f : α → β) (self : Lake.Job α) (prio : Task.Priority := Task.Priority.default) (sync : 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.

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

Equations

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

@[inline]

def Lake.Job.async {α : Type} (act : Lake.JobM α) (prio : Task.Priority := Task.Priority.default) : Lake.SpawnM (Lake.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 : 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.

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

Apply f asynchronously to the job's output.

Equations

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

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

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

Equations

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

def Lake.Job.bindM {α : Type u_1} {β : Type} (self : Lake.Job α) (f : α → Lake.JobM (Lake.Job β)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : Lake.SpawnM (Lake.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.

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

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

Equations

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

@[inline]

def Lake.Job.zipResultWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Lake.JobResult α → Lake.JobResult β → Lake.JobResult γ) (self : Lake.Job α) (other : Lake.Job β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := true) : 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.Job.zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (self : Lake.Job α) (other : Lake.Job β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := true) : 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.

def Lake.Job.add {α : Type u_1} {β : Type u_2} (self : Lake.Job α) (other : Lake.Job β) : Lake.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 : Lake.Job α) (other : Lake.Job β) : Lake.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 (Lake.Job α)) : Lake.Job Unit

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• Lake.Job.collectArray jobs = Array.foldl (fun (self : Lake.Job (Array α)) (other : Lake.Job α) => Lake.Job.zipWith Array.push self other) (pure (Array.mkEmpty jobs.size)) jobs

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

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

A Lake build job.

Equations

• Lake.BuildJob α = Lake.Job α

@[inline, deprecated "Obsolete." (since := "2024-12-06")]

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

Equations

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

@[inline, deprecated "Obsolete." (since := "2024-12-06")]

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

Equations

• Lake.BuildJob.ofJob job = Lake.Job.mapOk (fun (trace : Lake.BuildTrace) (s : Lake.JobState) => Lake.EResult.ok () { log := s.log, action := s.action, trace := trace }) job

@[reducible, inline]

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

Equations

• self.toJob = self

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

abbrev Lake.BuildJob.nil : Lake.BuildJob Unit

Equations

• Lake.BuildJob.nil = Lake.Job.pure ()

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

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

Equations

• Lake.BuildJob.pure a = Lake.Job.pure a

instance Lake.BuildJob.instPure : Pure Lake.BuildJob

Equations

• Lake.BuildJob.instPure = { pure := fun {α : Type ?u.6} (a : α) => Lake.Job.pure a }

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

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

Equations

• Lake.BuildJob.map f self = Lake.Job.map f self.toJob

instance Lake.BuildJob.instFunctor : Functor Lake.BuildJob

Equations

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

@[inline, deprecated "Removed without replacement." (since := "2024-12-06")]

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

Equations

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

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

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

Equations

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

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

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

Equations

• self.bindAsync f prio sync = self.toJob.bindM (fun (a : α) => do let __do_lift ← Lake.getTrace liftM (f a __do_lift)) prio sync

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

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

Equations

• self.wait? = self.toJob.wait?

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

abbrev Lake.BuildJob.add {α : Type u_1} {β : Type u_2} (self : Lake.BuildJob α) (other : Lake.BuildJob β) : Lake.BuildJob α

Equations

• self.add other = self.toJob.add other.toJob

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

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

Equations

• self.mix other = self.toJob.mix other.toJob

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

abbrev Lake.BuildJob.mixList {α : Type u_1} (jobs : List (Lake.BuildJob α)) : Id (Lake.BuildJob Unit)

Equations

• Lake.BuildJob.mixList jobs = pure (Lake.Job.mixList jobs)

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

abbrev Lake.BuildJob.mixArray {α : Type u_1} (jobs : Array (Lake.BuildJob α)) : Id (Lake.BuildJob Unit)

Equations

• Lake.BuildJob.mixArray jobs = pure (Lake.Job.mixArray jobs)

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

abbrev Lake.BuildJob.zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (self : Lake.BuildJob α) (other : Lake.BuildJob β) : Lake.BuildJob γ

Equations

• Lake.BuildJob.zipWith f self other = Lake.Job.zipWith f self.toJob other.toJob

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

abbrev Lake.BuildJob.collectList {α : Type u_1} (jobs : List (Lake.BuildJob α)) : Id (Lake.BuildJob (List α))

Equations

• Lake.BuildJob.collectList jobs = pure (Lake.Job.collectList jobs)

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

abbrev Lake.BuildJob.collectArray {α : Type u_1} (jobs : Array (Lake.BuildJob α)) : Id (Lake.BuildJob (Array α))

Equations

• Lake.BuildJob.collectArray jobs = pure (Lake.Job.collectArray jobs)