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 #
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?
)
Equations
- Lake.instInhabitedJobAction = { default := Lake.JobAction.unknown }
Equations
- Lake.instReprJobAction = { reprPrec := Lake.reprJobAction✝ }
Equations
- Lake.instOrdJobAction = { compare := Lake.ordJobAction✝ }
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 #
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.
Equations
- Lake.JobState.logEntry e s = Lake.JobState.modifyLog (fun (x : Lake.Log) => x.push e) s
JobTask #
The result of a Lake job.
Equations
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)
Job #
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.
Equations
- Lake.instInhabitedJob = { default := { task := default, kind := Lake.OptDataKind.anonymous, caption := default } }
Equations
- Lake.Job.ofTask task caption = { task := task, kind := inst✝, caption := caption }
Equations
- Lake.Job.error log caption = Lake.Job.ofTask { get := Lake.EResult.error 0 { log := log } } caption
Equations
- Lake.Job.pure a log caption = Lake.Job.ofTask { get := Lake.EResult.ok a { log := log } } caption
Equations
- Lake.Job.instPure = { pure := fun {α : Type ?u.5} (a : α) => Lake.Job.pure a }
For internal use.
Equations
- Lake.Job.traceRoot a caption = Lake.Job.ofTask { get := Lake.EResult.ok a { trace := Lake.BuildTrace.nil caption } }
Equations
- Lake.Job.nop log caption = Lake.Job.pure () log caption
Equations
- Lake.Job.nil traceCaption = Lake.Job.traceRoot () traceCaption
Waits for the job and returns it trace. Useful if the job is already known to be completed.
Sets the job's caption if the job's current caption is empty.
Equations
- Lake.Job.mapResult f self prio sync = { task := Task.map f self.task prio sync, kind := inferInstance, caption := self.caption, optional := self.optional }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lake.Job.map f self prio sync = Lake.Job.mapResult (fun (x : Lake.JobResult α) => Lake.EResult.map f x) self prio sync
Equations
- Lake.Job.instFunctor = { map := fun {α β : Type ?u.12} (f : α → β) (self : Lake.Job α) => Lake.Job.map f self }
OpaqueJob #
A Lake job task with an opaque value in Type
.
Equations
Instances For
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
Equations
A Lake job with an opaque value in Type
.