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.

• reuse : JobAction

  Tried to reuse a cached build (e.g., can be set by replayCachedIfUpToDate).

• replay : JobAction

  Tried to replay a completed build action (e.g., can be set by replayIfUpToDate).

• unpack : JobAction

  Tried to unpack a build from an archive (e.g., unpacking a module ltar).

• fetch : JobAction

  Tried to fetch a build from a remote store (e.g., set when downloading an artifact on-demand from a cache service in buildArtifactUnlessUpToDate).

• build : JobAction

  Tried to perform a build action (e.g., set by buildAction).

@[instance_reducible]

instance Lake.instInhabitedJobAction : Inhabited JobAction

Equations

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

def Lake.instReprJobAction.repr : JobAction → Nat → Std.Format

Equations

• Lake.instReprJobAction.repr Lake.JobAction.unknown prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.JobAction.unknown")).group prec✝
• Lake.instReprJobAction.repr Lake.JobAction.reuse prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.JobAction.reuse")).group prec✝
• Lake.instReprJobAction.repr Lake.JobAction.replay prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.JobAction.replay")).group prec✝
• Lake.instReprJobAction.repr Lake.JobAction.unpack prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.JobAction.unpack")).group prec✝
• Lake.instReprJobAction.repr Lake.JobAction.fetch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.JobAction.fetch")).group prec✝
• Lake.instReprJobAction.repr Lake.JobAction.build prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.JobAction.build")).group prec✝

@[instance_reducible]

instance Lake.instReprJobAction : Repr JobAction

Equations

• Lake.instReprJobAction = { reprPrec := Lake.instReprJobAction.repr }

@[instance_reducible]

instance Lake.instDecidableEqJobAction : DecidableEq JobAction

Equations

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

@[instance_reducible]

instance Lake.instOrdJobAction : Ord JobAction

Equations

• Lake.instOrdJobAction = { compare := Lake.instOrdJobAction.ord }

def Lake.instOrdJobAction.ord : JobAction → JobAction → Ordering

Equations

• Lake.instOrdJobAction.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[instance_reducible]

instance Lake.JobAction.instLT : LT JobAction

Equations

• Lake.JobAction.instLT = ltOfOrd

@[instance_reducible]

instance Lake.JobAction.instLE : LE JobAction

Equations

• Lake.JobAction.instLE = leOfOrd

@[instance_reducible]

instance Lake.JobAction.instMin : Min JobAction

Equations

• Lake.JobAction.instMin = minOfLe

@[instance_reducible]

instance Lake.JobAction.instMax : Max JobAction

Equations

• Lake.JobAction.instMax = maxOfLe

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

Equations

• a.merge b = max a b

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

Equations

• Lake.JobAction.verb failed Lake.JobAction.unknown = if failed = true then "Running" else "Ran"
• Lake.JobAction.verb failed Lake.JobAction.reuse = if failed = true then "Reusing" else "Reused"
• Lake.JobAction.verb failed Lake.JobAction.replay = if failed = true then "Replaying" else "Replayed"
• Lake.JobAction.verb failed Lake.JobAction.unpack = if failed = true then "Unpacking" else "Unpacked"
• 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.

• wantsRebuild : Bool

  Whether this job failed due to a request to rebuild for --no-build.

• trace : BuildTrace

  Current trace of a build job.

• buildTime : Nat

  How long the job spent building (in milliseconds).

@[instance_reducible]

instance Lake.instInhabitedJobState : Inhabited JobState

Equations

• Lake.instInhabitedJobState = { default := Lake.instInhabitedJobState.default }

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

Equations

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

@[inline]

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

Equations

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

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

def Lake.cancelMessage : String

For internal use only. Log message marking a job continuation canceled by the build's cancellation token. Do not match this directly; use JobResult.isCanceled.

Equations

• Lake.cancelMessage = "canceled after earlier build failure"

def Lake.JobResult.isCanceled {α : Type u_1} : JobResult α → Bool

Whether this result is a cancellation.

Also correct on merged results (e.g., from zipResultWith, mix, collectArray): a result that contains both a genuine failure and cancellations is classified as failed.

Equations

• One or more equations did not get rendered due to their size.
• Lake.JobResult.isCanceled (Lake.EResult.ok a a_1) = false

@[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_reducible]

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_reducible]

instance Lake.Job.instPure : Pure Job

Equations

• Lake.Job.instPure = { pure := fun {α : Type ?u.1} (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_reducible]

instance Lake.Job.instFunctor : Functor Job

Equations

• Lake.Job.instFunctor = { map := fun {α β : Type ?u.1} (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 Lake.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 Lake.Opaque.mk x) self

@[instance_reducible]

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 Lake.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_reducible]

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

Equations

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