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.

• kind : OptDataKind α

  The kind of data this job produces.

• 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 {α : Type u_1} : Inhabited (Job α)

Equations

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

def Lake.Job.cast {α : Type u_1} (self : Job α) (h : ¬self.kind.isAnonymous = true) : Job (DataType (OptDataKind.name α))

Equations

• self.cast h = cast ⋯ self

@[inline]

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

Equations

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

@[inline]

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

Equations

• Lake.Job.error log caption = Lake.Job.ofTask { get := Lake.EResult.error 0 { log := log } } caption

@[inline]

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

Equations

• Lake.Job.pure a log caption = Lake.Job.ofTask { get := Lake.EResult.ok a { log := log } } caption

instance Lake.Job.instPure : Pure Job

Equations

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

@[inline]

def Lake.Job.traceRoot {α : Type u_1} (a : α) (caption : String := "<root>") : Job α

For internal use.

Equations

• Lake.Job.traceRoot a caption = Lake.Job.ofTask { get := Lake.EResult.ok a { trace := Lake.BuildTrace.nil caption } }

@[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 (traceCaption : String := "<nil>") : Job Unit

Equations

• Lake.Job.nil traceCaption = Lake.Job.traceRoot () traceCaption

@[inline]

def Lake.Job.getTrace {α : Type u_1} (job : Job α) : BuildTrace

Waits for the job and returns it trace. Useful if the job is already known to be completed.

Equations

• job.getTrace = (Lake.EResult.state job.task.get).trace

@[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, kind := job.kind, 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, kind := job.kind, caption := caption, optional := job.optional } else job

@[inline]

def Lake.Job.mapResult {β : Type u_1} {α : Type u_2} [OptDataKind β] (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, kind := inferInstance, caption := self.caption, optional := self.optional }

@[inline]

def Lake.Job.mapOk {β : Type u_1} {α : Type u_2} [OptDataKind β] (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} [OptDataKind β] (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

• Lake.Job.instFunctor = { map := fun {α β : Type ?u.12} (f : α → β) (self : Lake.Job α) => Lake.Job.map f self }

OpaqueJob

@[reducible, inline]

abbrev Lake.OpaqueJobTask : Type

A Lake job task with an opaque value in Type.

Equations

• Lake.OpaqueJobTask = Lake.JobTask Opaque

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

def Lake.JobTask.toOpaque {α : Type u_1} (self : JobTask α) : OpaqueJobTask

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

Equations

• self.toOpaque = Task.map (fun (x : Lake.JobResult α) => Lake.EResult.map Opaque.mk x) self

instance Lake.instCoeOutJobTaskOpaqueJobTask {α : Type u_1} : CoeOut (JobTask α) OpaqueJobTask

Equations

• Lake.instCoeOutJobTaskOpaqueJobTask = { coe := Lake.JobTask.toOpaque }

@[reducible, inline]

abbrev Lake.OpaqueJob : Type

A Lake job with an opaque value in Type.

Equations

• Lake.OpaqueJob = Lake.Job Opaque

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

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

Equations

• job.toOpaque = { task := job.task.toOpaque, kind := Lake.OptDataKind.anonymous, caption := job.caption, optional := job.optional }

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

Equations

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