Documentation

Lake.Build.Job

inductive Lake.JobAction :

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?)

Instances For
Equations
@[inline]
Equations
Equations
structure Lake.JobState :

Mutable state of a Lake job.

  • log : Lake.Log

    The job's log.

  • Tracks whether this job performed any significant build action.

Instances For
Equations
@[inline]

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
Equations
  • a.merge b = { log := a.log ++ b.log, action := a.action.merge b.action }
@[inline]
Equations
@[reducible, inline]
abbrev Lake.JobResult (α : Type u_1) :
Type u_1

The result of a Lake job.

Equations
@[reducible, inline]
abbrev Lake.JobTask (α : Type u_1) :
Type u_1

The Task of a Lake job.

Equations
Instances For
@[reducible, inline]
abbrev Lake.JobM (α : 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
Instances For
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
@[inline]

Record that this job is trying to perform some action.

Equations
@[reducible, inline]
abbrev Lake.SpawnM (α : Type) :

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

Equations
@[reducible, inline, deprecated Lake.SpawnM]
abbrev Lake.SchedulerM (α : Type) :

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

Equations
Equations
  • Lake.instCoeOutJobTaskBundledJobTask = { coe := Lake.BundledJobTask.mk }
@[implemented_by Lake.OpaqueJobTask.unsafeMk]
@[implemented_by Lake.OpaqueJobTask.unsafeGet]
Equations
@[reducible, inline]
Equations
  • job.Result = job.task.get.Result
@[reducible, inline]
Equations
  • job.task = job.task.get.task
@[reducible, inline]
abbrev Lake.OpaqueJob.ofJob {α : Type u_1} (job : Lake.Job α) :
Equations
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 }
Equations
  • Lake.instCoeDepOpaqueJobJobResult = { coe := job.toJob }
@[inline]
def Lake.Job.ofTask {α : Type u_1} (task : Lake.JobTask α) (caption : String := "") :
Equations
@[inline]
def Lake.Job.error {α : Type u_1} (log : Lake.Log := ) (caption : String := "") :
Equations
@[inline]
def Lake.Job.pure {α : Type u_1} (a : α) (log : Lake.Log := ) (caption : String := "") :
Equations
Equations
instance Lake.Job.instInhabited {α : Type u_1} [Inhabited α] :
Equations
  • Lake.Job.instInhabited = { default := pure default }
@[inline]
def Lake.Job.nop (log : Lake.Log := ) (caption : String := "") :
Equations
@[inline]
def Lake.Job.setCaption {α : Type u_1} (caption : String) (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 α) :

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) :
Equations
@[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_liftf 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) :
Equations
Equations
  • One or more equations did not get rendered due to their size.
def Lake.Job.renew {α : Type u_1} (self : 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]

Spawn a job that asynchronously performs act.

Equations
@[inline]
def Lake.Job.wait {α : Type} (self : Lake.Job α) :

Wait a the job to complete and return the result.

Equations
@[inline]
def Lake.Job.wait? {α : Type} (self : Lake.Job α) :

Wait for a job to complete and return the produced value. If an error occurred, return none and discarded any logs produced.

Equations
@[inline]
def Lake.Job.await {α : Type} (self : Lake.Job α) :

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) :

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) :

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) :

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
Instances For
@[inline]
Equations
@[inline]
Equations
  • self.toJob = self
@[inline]
def Lake.BuildJob.pure {α : Type u_1} (a : α) :
Equations
Equations
@[inline]
def Lake.BuildJob.map {α β : Type u_1} (f : αβ) (self : Lake.BuildJob α) :
Equations
Equations
@[inline]
def Lake.BuildJob.mapWithTrace {α β : Type u_1} (f : αLake.BuildTraceβ × Lake.BuildTrace) (self : Lake.BuildJob α) :
Equations
@[inline]
def Lake.BuildJob.bindSync {α : Type u_1} {β : Type} (self : Lake.BuildJob α) (f : αLake.BuildTraceLake.JobM β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
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.BuildTraceLake.SpawnM (Lake.Job β)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
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 α) :
Equations
def Lake.BuildJob.add {α : Type u_1} {β : Type u_2} (self : Lake.BuildJob α) (other : Lake.BuildJob β) :
Equations
def Lake.BuildJob.mix {α : Type u_1} {β : Type u_2} (self : Lake.BuildJob α) (other : Lake.BuildJob β) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
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 β) :
Equations
  • One or more equations did not get rendered due to their size.