inductive Lake.JobAction : Type

Information on what this job did.

• unknown : Lake.JobAction

  No information about this job's action is available.

• replay : Lake.JobAction

  Tried to replay a cached build action (set by buildFileUnlessUpToDate)

• fetch : Lake.JobAction

  Tried to fetch a build from a store (can be set by buildUnlessUpToDate?)

• build : Lake.JobAction

  Tried to perform a build action (set by buildUnlessUpToDate?)

instance Lake.instInhabitedJobAction : Inhabited Lake.JobAction

Equations

• Lake.instInhabitedJobAction = { default := Lake.JobAction.unknown }

instance Lake.instReprJobAction : Repr Lake.JobAction

Equations

• Lake.instReprJobAction = { reprPrec := Lake.reprJobAction✝ }

instance Lake.instDecidableEqJobAction : DecidableEq Lake.JobAction

Equations

• Lake.instDecidableEqJobAction x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Lake.instOrdJobAction : Ord Lake.JobAction

Equations

• Lake.instOrdJobAction = { compare := Lake.ordJobAction✝ }

instance Lake.instLTJobAction : LT Lake.JobAction

Equations

• Lake.instLTJobAction = ltOfOrd

instance Lake.instLEJobAction : LE Lake.JobAction

Equations

• Lake.instLEJobAction = leOfOrd

instance Lake.instMinJobAction : Min Lake.JobAction

Equations

• Lake.instMinJobAction = minOfLe

instance Lake.instMaxJobAction : Max Lake.JobAction

Equations

• Lake.instMaxJobAction = maxOfLe

@[inline]

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

Equations

• a.merge b = max a b

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"

structure Lake.JobState : Type

Mutable state of a Lake job.

• log : Lake.Log

  The job's log.

• action : Lake.JobAction

  Tracks whether this job performed any significant build action.

instance Lake.instInhabitedJobState : Inhabited Lake.JobState

Equations

• Lake.instInhabitedJobState = { default := { log := default, action := default } }

@[inline]

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

• x✝.renew = { log := ∅, action := Lake.JobAction.unknown }

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 }

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

@[reducible, inline]

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

The result of a Lake job.

Equations

• Lake.JobResult α = Lake.EResult Lake.Log.Pos Lake.JobState α

@[reducible, inline]

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

The Task of a Lake job.

Equations

• Lake.JobTask α = Lake.BaseIOTask (Lake.JobResult α)

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

@[reducible, inline]

abbrev Lake.SpawnM (α : Type) : Type

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

Equations

• Lake.SpawnM = Lake.BuildT BaseIO

@[reducible, inline, deprecated Lake.SpawnM]

abbrev Lake.SchedulerM (α : Type) : Type

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

Equations

• Lake.SchedulerM = Lake.SpawnM

@[reducible, inline]

abbrev Lake.Job (α : Type u) : Type u

A Lake job.

Equations

• Lake.Job α = Lake.JobCore (Lake.JobTask α)

structure Lake.BundledJobTask : Type (u + 1)

• Result : Type u
• task : Lake.JobTask self.Result

instance Lake.instInhabitedBundledJobTask : Inhabited Lake.BundledJobTask

Equations

• Lake.instInhabitedBundledJobTask = { default := Lake.BundledJobTask.mk default }

instance Lake.instCoeOutJobTaskBundledJobTask {α : Type u_1} : CoeOut (Lake.JobTask α) Lake.BundledJobTask

Equations

• Lake.instCoeOutJobTaskBundledJobTask = { coe := Lake.BundledJobTask.mk }

unsafe def Lake.OpaqueJobTask.unsafeMk : Lake.BundledJobTask → Lake.OpaqueJobTask

Equations

• Lake.OpaqueJobTask.unsafeMk = unsafeCast

@[implemented_by Lake.OpaqueJobTask.unsafeMk]

opaque Lake.OpaqueJobTask.mk : Lake.BundledJobTask → Lake.OpaqueJobTask

unsafe def Lake.OpaqueJobTask.unsafeGet : Lake.OpaqueJobTask → Lake.BundledJobTask

Equations

• Lake.OpaqueJobTask.unsafeGet = unsafeCast

@[implemented_by Lake.OpaqueJobTask.unsafeGet]

opaque Lake.OpaqueJobTask.get : Lake.OpaqueJobTask → Lake.BundledJobTask

instance Lake.OpaqueJobTask.instInhabitedOfBundledJobTask [Inhabited Lake.BundledJobTask] : Inhabited Lake.OpaqueJobTask

Equations

• Lake.OpaqueJobTask.instInhabitedOfBundledJobTask = { default := Lake.OpaqueJobTask.mk default }

instance Lake.OpaqueJobTask.instCoeBundledJobTask_1 : Coe Lake.OpaqueJobTask Lake.BundledJobTask

Equations

• Lake.OpaqueJobTask.instCoeBundledJobTask_1 = { coe := Lake.OpaqueJobTask.get }

instance Lake.OpaqueJobTask.instCoeBundledJobTask : Coe Lake.BundledJobTask Lake.OpaqueJobTask

Equations

• Lake.OpaqueJobTask.instCoeBundledJobTask = { coe := Lake.OpaqueJobTask.mk }

@[reducible, inline]

abbrev Lake.OpaqueJob.Result (job : Lake.OpaqueJob) : Type

Equations

• job.Result = job.task.get.Result

@[reducible, inline]

abbrev Lake.OpaqueJob.task (job : Lake.OpaqueJob) : Lake.JobTask job.Result

Equations

• job.task = job.task.get.task

@[reducible, inline]

abbrev Lake.OpaqueJob.ofJob {α : Type u_1} (job : Lake.Job α) : Lake.OpaqueJob

Equations

• Lake.OpaqueJob.ofJob job = { task := Lake.OpaqueJobTask.mk (Lake.BundledJobTask.mk job.task), caption := job.caption, optional := job.optional }

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

Equations

• Lake.instCoeOutJobOpaqueJob = { coe := Lake.OpaqueJob.ofJob }

@[reducible, inline]

abbrev Lake.OpaqueJob.toJob (job : Lake.OpaqueJob) : Lake.Job job.Result

Equations

• job.toJob = { task := job.task, caption := job.caption, optional := job.optional }

instance Lake.instCoeDepOpaqueJobJobResult {job : Lake.OpaqueJob} : CoeDep Lake.OpaqueJob job (Lake.Job job.Result)

Equations

• Lake.instCoeDepOpaqueJobJobResult = { coe := job.toJob }

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

• Lake.Job.error log caption = { task := { get := Lake.EResult.error 0 { log := log, action := Lake.JobAction.unknown } }, caption := caption, optional := false }

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

• Lake.Job.async act prio ctx = (fun (task : Lake.JobTask α) => Lake.Job.ofTask task) <$> (Lake.withLoggedIO act ctx { log := ∅, action := Lake.JobAction.unknown }).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 : Task.Priority := Task.Priority.default) (sync : 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 : Task.Priority := Task.Priority.default) (sync : 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 u_3} (f : α → β → γ) (x : Lake.Job α) (y : Lake.Job β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : 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.

@[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.5} => Lake.BuildJob.pure }

@[inline]

def Lake.BuildJob.map {α β : 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.10} => Lake.BuildJob.map, mapConst := fun {α β : Type ?u.10} => Lake.BuildJob.map ∘ Function.const β }

@[inline]

def Lake.BuildJob.mapWithTrace {α β : 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 : Task.Priority := Task.Priority.default) (sync : 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 : Task.Priority := Task.Priority.default) (sync : 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 u_1} {β : Type u_2} (self : Lake.BuildJob α) (other : Lake.BuildJob β) : Lake.BuildJob α

Equations

• self.add other = Lake.BuildJob.mk (Lake.Job.zipWith (fun (a : α × Lake.BuildTrace) (x : β × Lake.BuildTrace) => a) self.toJob other.toJob)

def Lake.BuildJob.mix {α : Type u_1} {β : Type u_2} (self : Lake.BuildJob α) (other : Lake.BuildJob β) : 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 α)) : Id (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 α)) : Id (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 u_3} (f : α → β → γ) (self : Lake.BuildJob α) (other : Lake.BuildJob β) : Lake.BuildJob γ

Equations

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

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

Equations

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

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

Equations

• Lake.BuildJob.collectArray jobs = pure (Array.foldl (Lake.BuildJob.zipWith Array.push) (pure (Array.mkEmpty jobs.size)) jobs)