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 : Lake.JobAction) (b : Lake.JobAction) : Lake.JobAction

Equations

• a.merge b = max a b

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

Equations

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

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 : Lake.JobState) (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. Lifts into 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

@[deprecated]

def Lake.logStep (message : String) : Lake.JobM Unit

Logs a build step with message.

Deprecated: Build steps are now managed by a top-level build monitor. As a result, this no longer functions the way it used to. It now just logs the message via logVerbose.

Equations

• Lake.logStep message = Lake.logVerbose message

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

A Lake job.

• task : Lake.JobTask α
• caption : String

instance Lake.instInhabitedJob : {a : Type u_1} → Inhabited (Lake.Job a)

Equations

• Lake.instInhabitedJob = { default := { task := default, caption := default } }

structure Lake.BundledJob : Type (u + 1)

• type : Type u
• job : Lake.Job self.type

instance Lake.instInhabitedBundledJob : Inhabited Lake.BundledJob

Equations

• Lake.instInhabitedBundledJob = { default := Lake.BundledJob.mk default }

instance Lake.instCoeOutJobBundledJob {α : Type u_1} : CoeOut (Lake.Job α) Lake.BundledJob

Equations

• Lake.instCoeOutJobBundledJob = { coe := Lake.BundledJob.mk }

instance Lake.OpaqueJob.instCoeBundledJob_1 : Coe Lake.OpaqueJob Lake.BundledJob

Equations

• Lake.OpaqueJob.instCoeBundledJob_1 = { coe := Lake.OpaqueJob.get }

@[implemented_by Lake.OpaqueJob.unsafeMk]

opaque Lake.OpaqueJob.mk : Lake.BundledJob → Lake.OpaqueJob

@[implemented_by Lake.OpaqueJob.unsafeGet]

opaque Lake.OpaqueJob.get : Lake.OpaqueJob → Lake.BundledJob

unsafe def Lake.OpaqueJob.unsafeMk : Lake.BundledJob → Lake.OpaqueJob

Equations

• Lake.OpaqueJob.unsafeMk = unsafeCast

instance Lake.OpaqueJob.instCoeBundledJob : Coe Lake.BundledJob Lake.OpaqueJob

Equations

• Lake.OpaqueJob.instCoeBundledJob = { coe := Lake.OpaqueJob.mk }

instance Lake.OpaqueJob.instInhabitedOfBundledJob [Inhabited Lake.BundledJob] : Inhabited Lake.OpaqueJob

Equations

• Lake.OpaqueJob.instInhabitedOfBundledJob = { default := Lake.OpaqueJob.mk default }

unsafe def Lake.OpaqueJob.unsafeGet : Lake.OpaqueJob → Lake.BundledJob

Equations

• Lake.OpaqueJob.unsafeGet = unsafeCast

@[reducible, inline]

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

Equations

• job.type = job.get.type

@[reducible, inline]

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

Equations

• job.toJob = job.get.job

@[reducible, inline]

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

Equations

• job.task = job.toJob.task

@[reducible, inline]

abbrev Lake.OpaqueJob.caption (job : Lake.OpaqueJob) : String

Equations

• job.caption = job.toJob.caption

instance Lake.instCoeDepOpaqueJobJobType {job : Lake.OpaqueJob} : CoeDep Lake.OpaqueJob job (Lake.Job job.type)

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

instance Lake.Job.instPure : Pure Lake.Job

Equations

• Lake.Job.instPure = { pure := fun {α : Type u_1} (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 : optParam Lake.Log ∅) (caption : optParam 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 }

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

@[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, caption := self.caption }

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

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

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 : optParam 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 : 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 u_3} (f : α → β → γ) (x : Lake.Job α) (y : Lake.Job β) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam 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_1} => Lake.BuildJob.pure }

@[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 u_1} {β : Type u_2} (t1 : Lake.BuildJob α) (t2 : Lake.BuildJob β) : 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 β) : 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 : α → β → γ) (t1 : Lake.BuildJob α) (t2 : 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 #[]) jobs 0)