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

instance Lake.instReprJobAction : Repr JobAction

instance Lake.instDecidableEqJobAction : DecidableEq JobAction

instance Lake.instOrdJobAction : Ord JobAction

instance Lake.instLTJobAction : LT JobAction

instance Lake.instLEJobAction : LE JobAction

instance Lake.instMinJobAction : Min JobAction

instance Lake.instMaxJobAction : Max JobAction

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

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

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

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

@[inline]

def Lake.JobState.modifyLog (f : Log → Log) (s : JobState) : JobState

@[inline]

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

JobTask

@[reducible, inline]

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

The result of a Lake job.

def Lake.JobResult.prependLog {α : Type u_1} (log : Log) (self : JobResult α) : JobResult α

Add log entries to the beginning of the job's log.

@[reducible, inline]

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

The Task of a Lake job.

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

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

@[inline]

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

@[inline]

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

@[inline]

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

instance Lake.Job.instPure : Pure Job

@[inline]

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

For internal use.

@[inline]

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

@[inline]

def Lake.Job.nil (traceCaption : String := "<nil>") : Job Unit

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

@[inline]

def Lake.Job.setCaption {α : Type u_1} (caption : String) (job : Job α) : Job α

Sets the job's caption.

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

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

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

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

instance Lake.Job.instFunctor : Functor Job

OpaqueJob

@[reducible, inline]

abbrev Lake.OpaqueJobTask : Type

A Lake job task with an opaque value in Type.

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

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

@[reducible, inline]

abbrev Lake.OpaqueJob : Type

A Lake job with an opaque value in Type.

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.

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