Job Primitives

This module contains the basic definitions of a Lake Job. In particular, it defines OpaqueJob, which is needed for BuildContext. More complex utilities are defined in Lake.Build.Job.Monad, which depends on BuildContext.

JobAction

inductive Lake.JobAction : Type

Information on what this job did.

• unknown : JobAction

  No information about this job's action is available.

• replay : JobAction

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

• fetch : JobAction

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

• build : JobAction

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

instance Lake.instInhabitedJobAction : Inhabited JobAction

Equations

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

instance Lake.instReprJobAction : Repr JobAction

Equations

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

instance Lake.instDecidableEqJobAction : DecidableEq JobAction

Equations

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

instance Lake.instOrdJobAction : Ord JobAction

Equations

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

instance Lake.instLTJobAction : LT JobAction

Equations

• Lake.instLTJobAction = ltOfOrd

instance Lake.instLEJobAction : LE JobAction

Equations

• Lake.instLEJobAction = leOfOrd

instance Lake.instMinJobAction : Min JobAction

Equations

• Lake.instMinJobAction = minOfLe

instance Lake.instMaxJobAction : Max JobAction

Equations

• Lake.instMaxJobAction = maxOfLe

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

Equations

• a.merge b = max a b

def Lake.JobAction.verb (failed : Bool) : 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"

JobState

structure Lake.JobState : Type

Mutable state of a Lake job.

• log : Log

  The job's log.

• action : JobAction

  Tracks whether this job performed any significant build action.

• trace : BuildTrace

  Current trace of a build job.

instance Lake.instInhabitedJobState : Inhabited JobState

Equations

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

def Lake.JobState.merge (a b : JobState) : 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 : Log → Log) (s : JobState) : JobState

Equations

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

@[inline]

def Lake.JobState.logEntry (e : LogEntry) (s : JobState) : JobState

Equations

• Lake.JobState.logEntry e s = Lake.JobState.modifyLog (fun (x : Lake.Log) => x.push e) s

JobTask

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

def Lake.JobResult.prependLog {α : Type u_1} (log : Log) (self : JobResult α) : 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.JobTask (α : Type u_1) : Type u_1

The Task of a Lake job.

Equations

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

Job

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

A Lake job.

• task : JobTask α

  The Lean Task object for the job.

• caption : String

  A caption for the job in Lake's build monitor. Will be formatted like ✔ [3/5] Ran <caption>.

• optional : Bool

  Whether this job failing should cause the build to fail.

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Lake.Job.pure {α : Type u_1} (a : α) (log : Log := ∅) (caption : String := "") : 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 Job

Equations

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

@[inline]

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

Equations

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

@[inline]

def Lake.Job.nil : Job Unit

Equations

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

@[inline]

def Lake.Job.setCaption {α : Type u_1} (caption : String) (job : Job α) : 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 : Job α) : 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 : JobResult α → JobResult β) (self : Job α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : 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 : α → JobState → JobResult β) (self : Job α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : Job β

Equations

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

@[inline]

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

Equations

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

OpaqueJob

@[reducible, inline]

abbrev Lake.OpaqueJob : Type

A Lake job with an opaque value in Type.

Equations

• Lake.OpaqueJob = Lake.Job Opaque

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

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

Equations

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