feat: lake: lift FetchM into JobM (and vice versa) (#6771)
This PR enables `FetchM` to be run from `JobM` / `SpawnM` and vice-versa. This allows calls of `fetch` to asynchronously depend on the outputs of other jobs.
This commit is contained in:
Mac Malone
GitHub
parent
c8be581bc8
commit
58c7a4f15e
13 changed files with 626 additions and 550 deletions
|
|
@ -10,3 +10,4 @@ import Lake.Build.Package
|
|||
import Lake.Build.Library
|
||||
import Lake.Build.Imports
|
||||
import Lake.Build.Targets
|
||||
import Lake.Build.Job
|
||||
|
|
|
|||
|
|
@ -5,8 +5,9 @@ Authors: Mac Malone
|
|||
-/
|
||||
prelude
|
||||
import Lake.Config.Monad
|
||||
import Lake.Build.Actions
|
||||
import Lake.Util.JsonObject
|
||||
import Lake.Build.Actions
|
||||
import Lake.Build.Job
|
||||
|
||||
/-! # Common Build Tools
|
||||
This file defines general utilities that abstract common
|
||||
|
|
@ -19,6 +20,9 @@ namespace Lake
|
|||
|
||||
/-! ## General Utilities -/
|
||||
|
||||
/-- Exit code to return if `--no-build` is set and a build is required. -/
|
||||
def noBuildCode : ExitCode := 3
|
||||
|
||||
/--
|
||||
Build trace for the host platform.
|
||||
If an artifact includes this trace, it is platform-dependent
|
||||
|
|
|
|||
|
|
@ -4,20 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Util.Log
|
||||
import Lake.Util.Exit
|
||||
import Lake.Util.Lift
|
||||
import Lake.Util.Task
|
||||
import Lake.Util.Opaque
|
||||
import Lake.Config.Context
|
||||
import Lake.Build.Trace
|
||||
import Lake.Build.Job.Basic
|
||||
|
||||
open System
|
||||
namespace Lake
|
||||
|
||||
/-- Exit code to return if `--no-build` is set and a build is required. -/
|
||||
def noBuildCode : ExitCode := 3
|
||||
|
||||
/-- Configuration options for a Lake build. -/
|
||||
structure BuildConfig where
|
||||
/-- Use modification times for trace checking. -/
|
||||
|
|
@ -55,58 +47,6 @@ Whether the build should show progress information.
|
|||
def BuildConfig.showProgress (cfg : BuildConfig) : Bool :=
|
||||
(cfg.noBuild ∧ cfg.verbosity == .verbose) ∨ cfg.verbosity != .quiet
|
||||
|
||||
/-- Information on what this job did. -/
|
||||
inductive JobAction
|
||||
/-- No information about this job's action is available. -/
|
||||
| unknown
|
||||
/-- Tried to replay a cached build action (set by `buildFileUnlessUpToDate`) -/
|
||||
| replay
|
||||
/-- Tried to fetch a build from a store (can be set by `buildUnlessUpToDate?`) -/
|
||||
| fetch
|
||||
/-- Tried to perform a build action (set by `buildUnlessUpToDate?`) -/
|
||||
| build
|
||||
deriving Inhabited, Repr, DecidableEq, Ord
|
||||
|
||||
instance : LT JobAction := ltOfOrd
|
||||
instance : LE JobAction := leOfOrd
|
||||
instance : Min JobAction := minOfLe
|
||||
instance : Max JobAction := maxOfLe
|
||||
|
||||
def JobAction.merge (a b : JobAction) : JobAction :=
|
||||
max a b
|
||||
|
||||
/-- Mutable state of a Lake job. -/
|
||||
structure JobState where
|
||||
/-- The job's log. -/
|
||||
log : Log := {}
|
||||
/-- Tracks whether this job performed any significant build action. -/
|
||||
action : JobAction := .unknown
|
||||
/-- Current trace of a build job. -/
|
||||
trace : BuildTrace := .nil
|
||||
deriving Inhabited
|
||||
|
||||
/-- The result of a Lake job. -/
|
||||
abbrev JobResult α := EResult Log.Pos JobState α
|
||||
|
||||
/-- The `Task` of a Lake job. -/
|
||||
abbrev JobTask α := BaseIOTask (JobResult α)
|
||||
|
||||
/-- A Lake job. -/
|
||||
structure Job (α : Type u) where
|
||||
/-- The Lean `Task` object for the job. -/
|
||||
task : JobTask α
|
||||
/--
|
||||
A caption for the job in Lake's build monitor.
|
||||
Will be formatted like `✔ [3/5] Ran <caption>`.
|
||||
-/
|
||||
caption : String
|
||||
/-- Whether this job failing should cause the build to fail. -/
|
||||
optional : Bool := false
|
||||
deriving Inhabited
|
||||
|
||||
/-- A Lake job with an opaque value in `Type`. -/
|
||||
abbrev OpaqueJob := Job Opaque
|
||||
|
||||
/-- A Lake context with a build configuration and additional build data. -/
|
||||
structure BuildContext extends BuildConfig, Context where
|
||||
leanTrace : BuildTrace
|
||||
|
|
@ -119,6 +59,9 @@ abbrev BuildT := ReaderT BuildContext
|
|||
abbrev MonadBuild (m : Type → Type u) :=
|
||||
MonadReaderOf BuildContext m
|
||||
|
||||
instance [Pure m] : MonadLift LakeM (BuildT m) where
|
||||
monadLift x := fun ctx => pure <| x.run ctx.toContext
|
||||
|
||||
@[inline] def getBuildContext [MonadBuild m] : m BuildContext :=
|
||||
readThe BuildContext
|
||||
|
||||
|
|
@ -145,17 +88,3 @@ abbrev MonadBuild (m : Type → Type u) :=
|
|||
|
||||
@[inline] def getIsQuiet [Functor m] [MonadBuild m] : m Bool :=
|
||||
(· == .quiet) <$> getVerbosity
|
||||
|
||||
/-- The internal core monad of Lake builds. Not intended for user use. -/
|
||||
abbrev CoreBuildM := BuildT LogIO
|
||||
|
||||
/--
|
||||
Logs a build step with `message`.
|
||||
|
||||
**Deprecated:** Build steps are now managed by a top-level build monitor.
|
||||
As a result, this no longer functions the way it used to. It now just logs the
|
||||
`message` via `logVerbose`.
|
||||
-/
|
||||
@[deprecated "See doc-string for deprecation information." (since := "2024-05-25"), inline]
|
||||
def logStep [Monad m] [MonadLog m] (message : String) : m Unit := do
|
||||
logVerbose message
|
||||
|
|
@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Build.Job
|
||||
import Lake.Build.Data
|
||||
import Lake.Build.Job.Basic
|
||||
|
||||
/-!
|
||||
# Simple Builtin Facet Declarations
|
||||
|
|
|
|||
|
|
@ -4,11 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Util.Lift
|
||||
import Lake.Util.Error
|
||||
import Lake.Util.Cycle
|
||||
import Lake.Util.EquipT
|
||||
import Lake.Build.Info
|
||||
import Lake.Build.Store
|
||||
import Lake.Build.Context
|
||||
|
||||
/-! # Recursive Building
|
||||
|
||||
|
|
@ -20,60 +22,54 @@ using the `fetch` function defined in this module.
|
|||
|
||||
namespace Lake
|
||||
|
||||
/-- A recursive build of a Lake build store that may encounter a cycle. -/
|
||||
abbrev RecBuildM :=
|
||||
CallStackT BuildKey <| BuildT <| ELogT <| StateRefT BuildStore BaseIO
|
||||
|
||||
instance : MonadLift LogIO RecBuildM := ⟨ELogT.takeAndRun⟩
|
||||
/-- The internal core monad of Lake builds. Not intended for user use. -/
|
||||
abbrev CoreBuildM := BuildT LogIO
|
||||
|
||||
/--
|
||||
Run a `JobM` action in `RecBuildM` (and thus `FetchM`).
|
||||
A recursive build of a Lake build store that may encounter a cycle.
|
||||
|
||||
Generally, this should not be done, and instead a job action
|
||||
should be run asynchronously in a Job (e.g., via `Job.async`).
|
||||
An internal monad. Not intended for user use.
|
||||
-/
|
||||
@[inline] def RecBuildM.runJobM (x : JobM α) : RecBuildM α := fun _ ctx log => do
|
||||
match (← x ctx {log}) with
|
||||
| .ok a s => return .ok a s.log
|
||||
| .error e s => return .error e s.log
|
||||
|
||||
instance : MonadLift JobM RecBuildM := ⟨RecBuildM.runJobM⟩
|
||||
|
||||
/-- Run a recursive build. -/
|
||||
@[inline] def RecBuildM.run
|
||||
(stack : CallStack BuildKey) (store : BuildStore) (build : RecBuildM α)
|
||||
: CoreBuildM (α × BuildStore) := fun ctx log => do
|
||||
match (← (build stack ctx log).run store) with
|
||||
| (.ok a log, store) => return .ok (a, store) log
|
||||
| (.error e log, _) => return .error e log
|
||||
|
||||
/-- Run a recursive build in a fresh build store. -/
|
||||
@[inline] def RecBuildM.run' (build : RecBuildM α) : CoreBuildM α := do
|
||||
(·.1) <$> build.run {} {}
|
||||
abbrev RecBuildT (m : Type → Type) :=
|
||||
CallStackT BuildKey <| StateRefT' IO.RealWorld BuildStore <| BuildT m
|
||||
|
||||
/-- Log build cycle and error. -/
|
||||
@[specialize] def buildCycleError [MonadError m] (cycle : Cycle BuildKey) : m α :=
|
||||
error s!"build cycle detected:\n{"\n".intercalate <| cycle.map (s!" {·}")}"
|
||||
|
||||
instance : MonadCycleOf BuildKey RecBuildM where
|
||||
instance [Monad m] [MonadError m] : MonadCycleOf BuildKey (RecBuildT m) where
|
||||
throwCycle := buildCycleError
|
||||
|
||||
/--
|
||||
A recursive build of a Lake build store that may encounter a cycle.
|
||||
|
||||
An internal monad. Not intended for user use.
|
||||
-/
|
||||
abbrev RecBuildM := RecBuildT LogIO
|
||||
|
||||
/-- Run a recursive build. -/
|
||||
@[inline] def RecBuildM.run
|
||||
(stack : CallStack BuildKey) (store : BuildStore) (build : RecBuildM α)
|
||||
: CoreBuildM (α × BuildStore) :=
|
||||
build stack |>.run store
|
||||
|
||||
/-- Run a recursive build in a fresh build store. -/
|
||||
@[inline] def RecBuildM.run' (build : RecBuildM α) : CoreBuildM α := do
|
||||
(·.1) <$> build.run {} {}
|
||||
|
||||
/-- A build function for any element of the Lake build index. -/
|
||||
abbrev IndexBuildFn (m : Type → Type v) :=
|
||||
-- `DFetchFn BuildInfo (BuildData ·.key) m` with less imports
|
||||
(info : BuildInfo) → m (BuildData info.key)
|
||||
|
||||
/-- A transformer to equip a monad with a build function for the Lake index. -/
|
||||
abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
|
||||
abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn RecBuildM) m
|
||||
|
||||
/-- The top-level monad transformer for Lake build functions. -/
|
||||
abbrev FetchT (m : Type → Type) := IndexT <| RecBuildT m
|
||||
|
||||
/-- The top-level monad for Lake build functions. -/
|
||||
abbrev FetchM := IndexT RecBuildM
|
||||
|
||||
/-- Ensures that `JobM` lifts into `FetchM`. -/
|
||||
example : MonadLiftT JobM FetchM := inferInstance
|
||||
|
||||
/-- Ensures that `SpawnM` lifts into `FetchM`. -/
|
||||
example : MonadLiftT SpawnM FetchM := inferInstance
|
||||
abbrev FetchM := FetchT LogIO
|
||||
|
||||
/-- The top-level monad for Lake build functions. **Renamed `FetchM`.** -/
|
||||
@[deprecated FetchM (since := "2024-04-30")] abbrev IndexBuildM := FetchM
|
||||
|
|
@ -86,52 +82,3 @@ example : MonadLiftT SpawnM FetchM := inferInstance
|
|||
fun build => cast (by simp) <| build self
|
||||
|
||||
export BuildInfo (fetch)
|
||||
|
||||
/-- Wraps stray I/O, logs, and errors in `x` into the produced job. -/
|
||||
def ensureJob (x : FetchM (Job α))
|
||||
: FetchM (Job α) := fun fetch stack ctx log store => do
|
||||
let iniPos := log.endPos
|
||||
match (← (withLoggedIO x) fetch stack ctx log store) with
|
||||
| .ok job log =>
|
||||
if iniPos < log.endPos then
|
||||
let (log, jobLog) := log.split iniPos
|
||||
let job := job.mapResult (sync := true) (·.prependLog jobLog)
|
||||
return .ok job log
|
||||
else
|
||||
return .ok job log
|
||||
| .error _ log =>
|
||||
let (log, jobLog) := log.split iniPos
|
||||
return .ok (.error jobLog) log
|
||||
|
||||
/--
|
||||
Registers the job for the top-level build monitor,
|
||||
(e.g., the Lake CLI progress UI), assigning it `caption`.
|
||||
-/
|
||||
def registerJob (caption : String) (job : Job α) (optional := false) : FetchM (Job α) := do
|
||||
let job : Job α := {job with caption, optional}
|
||||
(← getBuildContext).registeredJobs.modify (·.push job)
|
||||
return job.renew
|
||||
|
||||
/--
|
||||
Registers the produced job for the top-level build monitor
|
||||
(e.g., the Lake CLI progress UI), assigning it `caption`.
|
||||
|
||||
Stray I/O, logs, and errors produced by `x` will be wrapped into the job.
|
||||
-/
|
||||
def withRegisterJob
|
||||
(caption : String) (x : FetchM (Job α)) (optional := false)
|
||||
: FetchM (Job α) := do
|
||||
let job ← ensureJob x
|
||||
registerJob caption job optional
|
||||
|
||||
/--
|
||||
Registers the produced job for the top-level build monitor
|
||||
if it is not already (i.e., it has an empty caption).
|
||||
-/
|
||||
@[inline] def maybeRegisterJob
|
||||
(caption : String) (job : Job α)
|
||||
: FetchM (Job α) := do
|
||||
if job.caption.isEmpty then
|
||||
registerJob caption job
|
||||
else
|
||||
return job
|
||||
|
|
|
|||
|
|
@ -1,387 +1,9 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Copyright (c) 2025 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Build.Basic
|
||||
|
||||
open System
|
||||
|
||||
namespace Lake
|
||||
|
||||
def JobAction.verb (failed : Bool) : JobAction → String
|
||||
| .unknown => if failed then "Running" else "Ran"
|
||||
| .replay => if failed then "Replaying" else "Replayed"
|
||||
| .fetch => if failed then "Fetching" else "Fetched"
|
||||
| .build => if failed then "Building" else "Built"
|
||||
|
||||
/--
|
||||
Resets the job state after a checkpoint (e.g., registering the job).
|
||||
Preserves state that downstream jobs want to depend on while resetting
|
||||
job-local state that should not be inherited by downstream jobs.
|
||||
-/
|
||||
@[inline] def JobState.renew (s : JobState) : JobState where
|
||||
trace := s.trace
|
||||
|
||||
def JobState.merge (a b : JobState) : JobState where
|
||||
log := a.log ++ b.log
|
||||
action := a.action.merge b.action
|
||||
trace := mixTrace a.trace b.trace
|
||||
|
||||
@[inline] def JobState.modifyLog (f : Log → Log) (s : JobState) :=
|
||||
{s with log := f s.log}
|
||||
|
||||
@[inline] def JobState.logEntry (e : LogEntry) (s : JobState) :=
|
||||
s.modifyLog (·.push e)
|
||||
|
||||
/-- Add log entries to the beginning of the job's log. -/
|
||||
def JobResult.prependLog (log : Log) (self : JobResult α) : JobResult α :=
|
||||
match self with
|
||||
| .ok a s => .ok a <| s.modifyLog (log ++ ·)
|
||||
| .error e s => .error ⟨log.size + e.val⟩ <| s.modifyLog (log ++ ·)
|
||||
|
||||
/--
|
||||
The monad of asynchronous Lake jobs.
|
||||
|
||||
While this can be lifted into `FetchM`, job action should generally
|
||||
be wrapped into an asynchronous job (e.g., via `Job.async`) instead of being
|
||||
run directly in `FetchM`.
|
||||
-/
|
||||
abbrev JobM := BuildT <| EStateT Log.Pos JobState BaseIO
|
||||
|
||||
instance [Pure m] : MonadLift LakeM (BuildT m) where
|
||||
monadLift x := fun ctx => pure <| x.run ctx.toContext
|
||||
|
||||
instance : MonadStateOf Log JobM where
|
||||
get := (·.log) <$> get
|
||||
set log := modify fun s => {s with log}
|
||||
modifyGet f := modifyGet fun s => let (a, log) := f s.log; (a, {s with log})
|
||||
|
||||
instance : MonadStateOf JobState JobM := inferInstance
|
||||
|
||||
instance : MonadLog JobM := .ofMonadState
|
||||
instance : MonadError JobM := ELog.monadError
|
||||
instance : Alternative JobM := ELog.alternative
|
||||
instance : MonadLift LogIO JobM := ⟨ELogT.takeAndRun⟩
|
||||
|
||||
/-- Record that this job is trying to perform some action. -/
|
||||
@[inline] def updateAction (action : JobAction) : JobM PUnit :=
|
||||
modify fun s => {s with action := s.action.merge action}
|
||||
|
||||
/-- Returns the current job's build trace. -/
|
||||
@[inline] def getTrace : JobM BuildTrace :=
|
||||
(·.trace) <$> get
|
||||
|
||||
/-- Sets the current job's build trace. -/
|
||||
@[inline] def setTrace (trace : BuildTrace) : JobM PUnit :=
|
||||
modify fun s => {s with trace := trace}
|
||||
|
||||
/-- Mix a trace into the current job's build trace. -/
|
||||
@[inline] def addTrace (trace : BuildTrace) : JobM PUnit :=
|
||||
modify fun s => {s with trace := s.trace.mix trace}
|
||||
|
||||
/-- Returns the current job's build trace and removes it from the state. -/
|
||||
@[inline] def takeTrace : JobM BuildTrace :=
|
||||
modifyGet fun s => (s.trace, {s with trace := nilTrace})
|
||||
|
||||
/-- The monad used to spawn asynchronous Lake build jobs. Lifts into `FetchM`. -/
|
||||
abbrev SpawnM := BuildT <| ReaderT BuildTrace <| BaseIO
|
||||
|
||||
@[inline] def JobM.runSpawnM (x : SpawnM α) : JobM α := fun ctx s =>
|
||||
return .ok (← x ctx s.trace) s
|
||||
|
||||
instance : MonadLift SpawnM JobM := ⟨JobM.runSpawnM⟩
|
||||
|
||||
/-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/
|
||||
@[deprecated SpawnM (since := "2024-05-21")] abbrev SchedulerM := SpawnM
|
||||
|
||||
@[inline] private unsafe def Job.toOpaqueImpl (job : Job α) : OpaqueJob :=
|
||||
unsafeCast job
|
||||
|
||||
/-- Forget the value of a job. Implemented as a no-op cast. -/
|
||||
@[implemented_by toOpaqueImpl]
|
||||
def Job.toOpaque (job : Job α) : OpaqueJob :=
|
||||
{job with task := job.task.map (·.map Opaque.mk)}
|
||||
|
||||
instance : CoeOut (Job α) OpaqueJob := ⟨.toOpaque⟩
|
||||
|
||||
namespace Job
|
||||
|
||||
@[inline] def ofTask (task : JobTask α) (caption := "") : Job α :=
|
||||
{task, caption}
|
||||
|
||||
@[inline] protected def error (log : Log := {}) (caption := "") : Job α :=
|
||||
{task := Task.pure (.error 0 {log}), caption}
|
||||
|
||||
@[inline] protected def pure (a : α) (log : Log := {}) (caption := "") : Job α :=
|
||||
{task := Task.pure (.ok a {log}), caption}
|
||||
|
||||
instance : Pure Job := ⟨Job.pure⟩
|
||||
instance [Inhabited α] : Inhabited (Job α) := ⟨pure default⟩
|
||||
|
||||
@[inline] protected def nop (log : Log := {}) (caption := "") : Job Unit :=
|
||||
.pure () log caption
|
||||
|
||||
@[inline] def nil : Job Unit :=
|
||||
.pure ()
|
||||
|
||||
/-- Sets the job's caption. -/
|
||||
@[inline] def setCaption (caption : String) (job : Job α) : Job α :=
|
||||
{job with caption}
|
||||
|
||||
/-- Sets the job's caption if the job's current caption is empty. -/
|
||||
@[inline] def setCaption? (caption : String) (job : Job α) : Job α :=
|
||||
if job.caption.isEmpty then {job with caption} else job
|
||||
|
||||
@[inline] def mapResult
|
||||
(f : JobResult α → JobResult β) (self : Job α)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: Job β := {self with task := self.task.map f prio sync}
|
||||
|
||||
@[inline] def mapOk
|
||||
(f : α → JobState → JobResult β) (self : Job α)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: Job β :=
|
||||
self.mapResult (prio := prio) (sync := sync) fun
|
||||
| .ok a s => f a s
|
||||
| .error e s => .error e s
|
||||
|
||||
@[inline] def bindTask [Monad m]
|
||||
(f : JobTask α → m (JobTask β)) (self : Job α)
|
||||
: m (Job β) := return {self with task := ← f self.task}
|
||||
|
||||
@[inline] protected def map
|
||||
(f : α → β) (self : Job α)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: Job β := self.mapResult (·.map f) prio sync
|
||||
|
||||
instance : Functor Job where map := Job.map
|
||||
|
||||
/--
|
||||
Resets the job's state after a checkpoint (e.g., registering the job).
|
||||
Preserves information that downstream jobs want to depend on while resetting
|
||||
job-local information that should not be inherited by downstream jobs.
|
||||
-/
|
||||
def renew (self : Job α) : Job α :=
|
||||
self.mapResult (sync := true) fun
|
||||
| .ok a s => .ok a s.renew
|
||||
| .error _ s => .error 0 s.renew
|
||||
|
||||
/-- Spawn a job that asynchronously performs `act`. -/
|
||||
@[inline] protected def async
|
||||
(act : JobM α) (prio := Task.Priority.default)
|
||||
: SpawnM (Job α) := fun ctx => .ofTask <$> do
|
||||
BaseIO.asTask (prio := prio) do (withLoggedIO act) ctx {}
|
||||
|
||||
/-- Wait a the job to complete and return the result. -/
|
||||
@[inline] protected def wait (self : Job α) : BaseIO (JobResult α) := do
|
||||
IO.wait self.task
|
||||
|
||||
/--
|
||||
Wait for a job to complete and return the produced value.
|
||||
If an error occurred, return `none` and discarded any logs produced.
|
||||
-/
|
||||
@[inline] protected def wait? (self : Job α) : BaseIO (Option α) := do
|
||||
return (← self.wait).result?
|
||||
|
||||
/--
|
||||
Wait for a job to complete and return the produced value.
|
||||
Logs the job's log and throws if there was an error.
|
||||
-/
|
||||
@[inline] protected def await (self : Job α) : LogIO α := do
|
||||
match (← self.wait) with
|
||||
| .error n {log, ..} => log.replay; throw n
|
||||
| .ok a {log, ..} => log.replay; pure a
|
||||
|
||||
/-- Apply `f` asynchronously to the job's output. -/
|
||||
protected def mapM
|
||||
(self : Job α) (f : α → JobM β)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: SpawnM (Job β) :=
|
||||
fun ctx trace => do
|
||||
self.bindTask fun task => do
|
||||
BaseIO.mapTask (t := task) (prio := prio) (sync := sync) fun
|
||||
| .ok a s =>
|
||||
let trace := mixTrace trace s.trace
|
||||
withLoggedIO (f a) ctx {s with trace}
|
||||
| .error n s => return .error n s
|
||||
|
||||
@[deprecated Job.mapM (since := "2024-12-06")]
|
||||
protected abbrev bindSync
|
||||
(self : Job α) (f : α → JobM β)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: SpawnM (Job β) := self.mapM f prio sync
|
||||
|
||||
/--
|
||||
Apply `f` asynchronously to the job's output
|
||||
and asynchronously await the resulting job.
|
||||
-/
|
||||
def bindM
|
||||
(self : Job α) (f : α → JobM (Job β))
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: SpawnM (Job β) :=
|
||||
fun ctx trace => do
|
||||
self.bindTask fun task => do
|
||||
BaseIO.bindTask task (prio := prio) (sync := sync) fun
|
||||
| .ok a sa => do
|
||||
let trace := mixTrace trace sa.trace
|
||||
match (← withLoggedIO (f a) ctx {sa with trace}) with
|
||||
| .ok job sa =>
|
||||
return job.task.map (prio := prio) (sync := true) fun
|
||||
| .ok b sb => .ok b {sa.merge sb with trace := sb.trace}
|
||||
| .error e sb => .error ⟨sa.log.size + e.val⟩ {sa.merge sb with trace := sb.trace}
|
||||
| .error e sa => return Task.pure (.error e sa)
|
||||
| .error e sa => return Task.pure (.error e sa)
|
||||
|
||||
@[deprecated bindM (since := "2024-12-06")]
|
||||
protected abbrev bindAsync
|
||||
(self : Job α) (f : α → SpawnM (Job β))
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: SpawnM (Job β) := self.bindM (fun a => f a) prio sync
|
||||
|
||||
/--
|
||||
`a.zipWith f b` produces a new job `c` that applies `f` to the
|
||||
results of `a` and `b`. The job `c` errors if either `a` or `b` error.
|
||||
-/
|
||||
@[inline] def zipResultWith
|
||||
(f : JobResult α → JobResult β → JobResult γ) (self : Job α) (other : Job β)
|
||||
(prio := Task.Priority.default) (sync := true)
|
||||
: Job γ := Job.ofTask $
|
||||
self.task.bind (prio := prio) (sync := true) fun rx =>
|
||||
other.task.map (prio := prio) (sync := sync) fun ry =>
|
||||
f rx ry
|
||||
|
||||
/--
|
||||
`a.zipWith f b` produces a new job `c` that applies `f` to the
|
||||
results of `a` and `b`. The job `c` errors if either `a` or `b` error.
|
||||
-/
|
||||
@[inline] def zipWith
|
||||
(f : α → β → γ) (self : Job α) (other : Job β)
|
||||
(prio := Task.Priority.default) (sync := true)
|
||||
: Job γ :=
|
||||
self.zipResultWith (other := other) (prio := prio) (sync := sync) fun
|
||||
| .ok a sa, .ok b sb => .ok (f a b) (sa.merge sb)
|
||||
| ra, rb => .error 0 (ra.state.merge rb.state)
|
||||
|
||||
|
||||
/-- Merges this job with another, discarding its output and trace. -/
|
||||
def add (self : Job α) (other : Job β) : Job α :=
|
||||
self.zipResultWith (other := other) fun
|
||||
| .ok a sa, .ok _ sb => .ok a {sa.merge sb with trace := sa.trace}
|
||||
| ra, rb => .error 0 {ra.state.merge rb.state with trace := ra.state.trace}
|
||||
|
||||
/-- Merges this job with another, discarding both outputs. -/
|
||||
def mix (self : Job α) (other : Job β) : Job Unit :=
|
||||
self.zipWith (fun _ _ => ()) other
|
||||
|
||||
/-- Merge a `List` of jobs into one, discarding their outputs. -/
|
||||
def mixList (jobs : List (Job α)) : Job Unit :=
|
||||
jobs.foldr (·.mix ·) nil
|
||||
|
||||
/-- Merge an `Array` of jobs into one, discarding their outputs. -/
|
||||
def mixArray (jobs : Array (Job α)) : Job Unit :=
|
||||
jobs.foldl (·.mix ·) nil
|
||||
|
||||
/-- Merge a `List` of jobs into one, collecting their outputs into a `List`. -/
|
||||
def collectList (jobs : List (Job α)) : Job (List α) :=
|
||||
jobs.foldr (zipWith List.cons) (pure [])
|
||||
|
||||
/-- Merge an `Array` of jobs into one, collecting their outputs into an `Array`. -/
|
||||
def collectArray (jobs : Array (Job α)) : Job (Array α) :=
|
||||
jobs.foldl (zipWith Array.push) (pure (Array.mkEmpty jobs.size))
|
||||
|
||||
end Job
|
||||
|
||||
/-- A Lake build job. -/
|
||||
abbrev BuildJob α := Job α
|
||||
|
||||
namespace BuildJob
|
||||
|
||||
@[inline, deprecated "Obsolete." (since := "2024-12-06")]
|
||||
def mk (job : Job (α × BuildTrace)) : BuildJob α :=
|
||||
job.mapOk fun (a, trace) s => .ok a {s with trace}
|
||||
|
||||
@[inline, deprecated "Obsolete." (since := "2024-12-06")]
|
||||
def ofJob (job : Job BuildTrace) : BuildJob Unit :=
|
||||
job.mapOk fun trace s => .ok () {s with trace}
|
||||
|
||||
abbrev toJob (self : BuildJob α) : Job α :=
|
||||
self
|
||||
|
||||
@[deprecated Job.nil (since := "2024-12-06")]
|
||||
abbrev nil : BuildJob Unit :=
|
||||
Job.pure ()
|
||||
|
||||
@[deprecated Job.map (since := "2024-12-06")]
|
||||
protected abbrev pure (a : α) : BuildJob α :=
|
||||
Job.pure a
|
||||
|
||||
instance : Pure BuildJob := ⟨Job.pure⟩
|
||||
|
||||
@[deprecated Job.map (since := "2024-12-06")]
|
||||
protected abbrev map (f : α → β) (self : BuildJob α) : BuildJob β :=
|
||||
self.toJob.map f
|
||||
|
||||
instance : Functor BuildJob where
|
||||
map := Job.map
|
||||
|
||||
@[inline, deprecated "Removed without replacement." (since := "2024-12-06")]
|
||||
def mapWithTrace (f : α → BuildTrace → β × BuildTrace) (self : BuildJob α) : BuildJob β :=
|
||||
self.toJob.mapOk fun a s =>
|
||||
let (b, trace) := f a s.trace
|
||||
.ok b {s with trace}
|
||||
|
||||
@[inline, deprecated Job.mapM (since := "2024-12-06")]
|
||||
protected def bindSync
|
||||
(self : BuildJob α) (f : α → BuildTrace → JobM (β × BuildTrace))
|
||||
(prio : Task.Priority := .default) (sync := false)
|
||||
: SpawnM (Job β) :=
|
||||
self.toJob.mapM (prio := prio) (sync := sync) fun a => do
|
||||
let (b, trace) ← f a (← getTrace)
|
||||
setTrace trace
|
||||
return b
|
||||
|
||||
@[inline, deprecated Job.bindM (since := "2024-12-06")]
|
||||
protected def bindAsync
|
||||
(self : BuildJob α) (f : α → BuildTrace → SpawnM (Job β))
|
||||
(prio : Task.Priority := .default) (sync := false)
|
||||
: SpawnM (Job β) :=
|
||||
self.toJob.bindM (prio := prio) (sync := sync) fun a => do
|
||||
f a (← getTrace)
|
||||
|
||||
@[deprecated Job.wait? (since := "2024-12-06")]
|
||||
protected abbrev wait? (self : BuildJob α) : BaseIO (Option α) :=
|
||||
self.toJob.wait?
|
||||
|
||||
@[deprecated Job.add (since := "2024-12-06")]
|
||||
abbrev add (self : BuildJob α) (other : BuildJob β) : BuildJob α :=
|
||||
self.toJob.add other.toJob
|
||||
|
||||
@[deprecated Job.mix (since := "2024-12-06")]
|
||||
abbrev mix (self : BuildJob α) (other : BuildJob β) : BuildJob Unit :=
|
||||
self.toJob.mix other.toJob
|
||||
|
||||
@[deprecated Job.mixList (since := "2024-12-06")]
|
||||
abbrev mixList (jobs : List (BuildJob α)) : Id (BuildJob Unit) :=
|
||||
return Job.mixList jobs
|
||||
|
||||
@[deprecated Job.mixArray (since := "2024-12-06")]
|
||||
abbrev mixArray (jobs : Array (BuildJob α)) : Id (BuildJob Unit) :=
|
||||
return Job.mixArray jobs
|
||||
|
||||
@[deprecated Job.zipWith (since := "2024-12-06")]
|
||||
abbrev zipWith
|
||||
(f : α → β → γ) (self : BuildJob α) (other : BuildJob β)
|
||||
: BuildJob γ :=
|
||||
self.toJob.zipWith f other.toJob
|
||||
|
||||
@[deprecated Job.collectList (since := "2024-12-06")]
|
||||
abbrev collectList (jobs : List (BuildJob α)) : Id (BuildJob (List α)) :=
|
||||
return Job.collectList jobs
|
||||
|
||||
@[deprecated Job.collectArray (since := "2024-12-06")]
|
||||
abbrev collectArray (jobs : Array (BuildJob α)) : Id (BuildJob (Array α)) :=
|
||||
return Job.collectArray jobs
|
||||
|
||||
attribute [deprecated Job (since := "2024-12-06")] BuildJob
|
||||
import Lake.Build.Job.Basic
|
||||
import Lake.Build.Job.Monad
|
||||
import Lake.Build.Job.Register
|
||||
|
|
|
|||
165
src/lake/Lake/Build/Job/Basic.lean
Normal file
165
src/lake/Lake/Build/Job/Basic.lean
Normal file
|
|
@ -0,0 +1,165 @@
|
|||
/-
|
||||
Copyright (c) 2021 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Util.Log
|
||||
import Lake.Util.Task
|
||||
import Lake.Util.Opaque
|
||||
import Lake.Build.Trace
|
||||
|
||||
/-! # 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`.
|
||||
-/
|
||||
|
||||
open System
|
||||
|
||||
namespace Lake
|
||||
|
||||
/-! ## JobAction -/
|
||||
|
||||
/-- Information on what this job did. -/
|
||||
inductive JobAction
|
||||
/-- No information about this job's action is available. -/
|
||||
| unknown
|
||||
/-- Tried to replay a cached build action (set by `buildFileUnlessUpToDate`) -/
|
||||
| replay
|
||||
/-- Tried to fetch a build from a store (can be set by `buildUnlessUpToDate?`) -/
|
||||
| fetch
|
||||
/-- Tried to perform a build action (set by `buildUnlessUpToDate?`) -/
|
||||
| build
|
||||
deriving Inhabited, Repr, DecidableEq, Ord
|
||||
|
||||
instance : LT JobAction := ltOfOrd
|
||||
instance : LE JobAction := leOfOrd
|
||||
instance : Min JobAction := minOfLe
|
||||
instance : Max JobAction := maxOfLe
|
||||
|
||||
def JobAction.merge (a b : JobAction) : JobAction :=
|
||||
max a b
|
||||
|
||||
def JobAction.verb (failed : Bool) : JobAction → String
|
||||
| .unknown => if failed then "Running" else "Ran"
|
||||
| .replay => if failed then "Replaying" else "Replayed"
|
||||
| .fetch => if failed then "Fetching" else "Fetched"
|
||||
| .build => if failed then "Building" else "Built"
|
||||
|
||||
/-! ## JobState -/
|
||||
|
||||
/-- Mutable state of a Lake job. -/
|
||||
structure JobState where
|
||||
/-- The job's log. -/
|
||||
log : Log := {}
|
||||
/-- Tracks whether this job performed any significant build action. -/
|
||||
action : JobAction := .unknown
|
||||
/-- Current trace of a build job. -/
|
||||
trace : BuildTrace := .nil
|
||||
deriving Inhabited
|
||||
|
||||
def JobState.merge (a b : JobState) : JobState where
|
||||
log := a.log ++ b.log
|
||||
action := a.action.merge b.action
|
||||
trace := mixTrace a.trace b.trace
|
||||
|
||||
@[inline] def JobState.modifyLog (f : Log → Log) (s : JobState) : JobState :=
|
||||
{s with log := f s.log}
|
||||
|
||||
@[inline] def JobState.logEntry (e : LogEntry) (s : JobState) :=
|
||||
s.modifyLog (·.push e)
|
||||
|
||||
/-! ## JobTask -/
|
||||
|
||||
/-- The result of a Lake job. -/
|
||||
abbrev JobResult α := EResult Log.Pos JobState α
|
||||
|
||||
/-- Add log entries to the beginning of the job's log. -/
|
||||
def JobResult.prependLog (log : Log) (self : JobResult α) : JobResult α :=
|
||||
match self with
|
||||
| .ok a s => .ok a <| s.modifyLog (log ++ ·)
|
||||
| .error e s => .error ⟨log.size + e.val⟩ <| s.modifyLog (log ++ ·)
|
||||
|
||||
/-- The `Task` of a Lake job. -/
|
||||
abbrev JobTask α := BaseIOTask (JobResult α)
|
||||
|
||||
/-! ## Job -/
|
||||
|
||||
/-- A Lake job. -/
|
||||
structure Job (α : Type u) where
|
||||
/-- The Lean `Task` object for the job. -/
|
||||
task : JobTask α
|
||||
/--
|
||||
A caption for the job in Lake's build monitor.
|
||||
Will be formatted like `✔ [3/5] Ran <caption>`.
|
||||
-/
|
||||
caption : String
|
||||
/-- Whether this job failing should cause the build to fail. -/
|
||||
optional : Bool := false
|
||||
deriving Inhabited
|
||||
|
||||
namespace Job
|
||||
|
||||
@[inline] def ofTask (task : JobTask α) (caption := "") : Job α :=
|
||||
{task, caption}
|
||||
|
||||
@[inline] protected def error (log : Log := {}) (caption := "") : Job α :=
|
||||
{task := Task.pure (.error 0 {log}), caption}
|
||||
|
||||
@[inline] protected def pure (a : α) (log : Log := {}) (caption := "") : Job α :=
|
||||
{task := Task.pure (.ok a {log}), caption}
|
||||
|
||||
instance : Pure Job := ⟨Job.pure⟩
|
||||
|
||||
@[inline] protected def nop (log : Log := {}) (caption := "") : Job Unit :=
|
||||
.pure () log caption
|
||||
|
||||
@[inline] def nil : Job Unit :=
|
||||
.pure ()
|
||||
|
||||
/-- Sets the job's caption. -/
|
||||
@[inline] def setCaption (caption : String) (job : Job α) : Job α :=
|
||||
{job with caption}
|
||||
|
||||
/-- Sets the job's caption if the job's current caption is empty. -/
|
||||
@[inline] def setCaption? (caption : String) (job : Job α) : Job α :=
|
||||
if job.caption.isEmpty then {job with caption} else job
|
||||
|
||||
@[inline] def mapResult
|
||||
(f : JobResult α → JobResult β) (self : Job α)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: Job β := {self with task := self.task.map f prio sync}
|
||||
|
||||
@[inline] def mapOk
|
||||
(f : α → JobState → JobResult β) (self : Job α)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: Job β :=
|
||||
self.mapResult (prio := prio) (sync := sync) fun
|
||||
| .ok a s => f a s
|
||||
| .error e s => .error e s
|
||||
|
||||
@[inline] protected def map
|
||||
(f : α → β) (self : Job α)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: Job β := self.mapResult (·.map f) prio sync
|
||||
|
||||
instance : Functor Job where map := Job.map
|
||||
|
||||
end Job
|
||||
|
||||
/-! ## OpaqueJob -/
|
||||
|
||||
/-- A Lake job with an opaque value in `Type`. -/
|
||||
abbrev OpaqueJob := Job Opaque
|
||||
|
||||
@[inline] private unsafe def Job.toOpaqueImpl (job : Job α) : OpaqueJob :=
|
||||
unsafeCast job
|
||||
|
||||
/-- Forget the value of a job. Implemented as a no-op cast. -/
|
||||
@[implemented_by toOpaqueImpl]
|
||||
def Job.toOpaque (job : Job α) : OpaqueJob :=
|
||||
{job with task := job.task.map (·.map Opaque.mk)}
|
||||
|
||||
instance : CoeOut (Job α) OpaqueJob := ⟨.toOpaque⟩
|
||||
328
src/lake/Lake/Build/Job/Monad.lean
Normal file
328
src/lake/Lake/Build/Job/Monad.lean
Normal file
|
|
@ -0,0 +1,328 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Build.Fetch
|
||||
|
||||
open System
|
||||
|
||||
/-! # Job Monad
|
||||
|
||||
This module contains additional definitions for Lake `Job`.
|
||||
In particular, it defines `JobM`, which uses `BuildContext`, which contains
|
||||
`OpaqueJob`s, hence the module split.
|
||||
-/
|
||||
|
||||
namespace Lake
|
||||
|
||||
/--
|
||||
The monad of asynchronous Lake jobs.
|
||||
|
||||
While this can be lifted into `FetchM`, job action should generally
|
||||
be wrapped into an asynchronous job (e.g., via `Job.async`) instead of being
|
||||
run directly in `FetchM`.
|
||||
-/
|
||||
abbrev JobM := FetchT <| EStateT Log.Pos JobState BaseIO
|
||||
|
||||
instance (priority := high) : MonadStateOf JobState JobM := inferInstance
|
||||
|
||||
instance : MonadStateOf Log JobM where
|
||||
get := (·.log) <$> get
|
||||
set log := modify fun s => {s with log}
|
||||
modifyGet f := modifyGet fun s => let (a, log) := f s.log; (a, {s with log})
|
||||
|
||||
instance : MonadLog JobM := .ofMonadState
|
||||
instance : MonadError JobM := ELog.monadError
|
||||
instance : Alternative JobM := ELog.alternative
|
||||
instance : MonadLift LogIO JobM := ⟨ELogT.takeAndRun⟩
|
||||
|
||||
/-- Record that this job is trying to perform some action. -/
|
||||
@[inline] def updateAction (action : JobAction) : JobM PUnit :=
|
||||
modify fun s => {s with action := s.action.merge action}
|
||||
|
||||
/-- Returns the current job's build trace. -/
|
||||
@[inline] def getTrace : JobM BuildTrace :=
|
||||
(·.trace) <$> get
|
||||
|
||||
/-- Sets the current job's build trace. -/
|
||||
@[inline] def setTrace (trace : BuildTrace) : JobM PUnit :=
|
||||
modify fun s => {s with trace := trace}
|
||||
|
||||
/-- Mix a trace into the current job's build trace. -/
|
||||
@[inline] def addTrace (trace : BuildTrace) : JobM PUnit :=
|
||||
modify fun s => {s with trace := s.trace.mix trace}
|
||||
|
||||
/-- Returns the current job's build trace and removes it from the state. -/
|
||||
@[inline] def takeTrace : JobM BuildTrace :=
|
||||
modifyGet fun s => (s.trace, {s with trace := nilTrace})
|
||||
|
||||
/-- The monad used to spawn asynchronous Lake build jobs. Lifts into `FetchM`. -/
|
||||
abbrev SpawnM := FetchT <| ReaderT BuildTrace <| BaseIO
|
||||
|
||||
@[inline] def JobM.runSpawnM (x : SpawnM α) : JobM α := fun fn stack store ctx s =>
|
||||
return .ok (← x fn stack store ctx s.trace) s
|
||||
|
||||
instance : MonadLift SpawnM JobM := ⟨JobM.runSpawnM⟩
|
||||
|
||||
/-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/
|
||||
@[deprecated SpawnM (since := "2024-05-21")] abbrev SchedulerM := SpawnM
|
||||
|
||||
/--
|
||||
Run a `JobM` action in `FetchM`.
|
||||
|
||||
Generally, this should not be done, and instead a job action
|
||||
should be run asynchronously in a Job (e.g., via `Job.async`).
|
||||
-/
|
||||
@[inline] def FetchM.runJobM (x : JobM α) : FetchM α := fun fetch stack store ctx log => do
|
||||
match (← x fetch stack store ctx {log}) with
|
||||
| .ok a s => return .ok a s.log
|
||||
| .error e s => return .error e s.log
|
||||
|
||||
instance : MonadLift JobM FetchM := ⟨FetchM.runJobM⟩
|
||||
|
||||
/-- Ensures that `JobM` lifts into `FetchM`. -/
|
||||
example : MonadLiftT JobM FetchM := inferInstance
|
||||
|
||||
/-- Ensures that `SpawnM` lifts into `FetchM`. -/
|
||||
example : MonadLiftT SpawnM FetchM := inferInstance
|
||||
|
||||
/-- Run a `FetchM` action in `JobM`. -/
|
||||
@[inline] def JobM.runFetchM (x : FetchM α) : JobM α := fun fetch stack store ctx s => do
|
||||
match (← x fetch stack store ctx s.log) with
|
||||
| .ok a log => return .ok a {s with log}
|
||||
| .error e log => return .error e {s with log}
|
||||
|
||||
instance : MonadLift FetchM JobM := ⟨JobM.runFetchM⟩
|
||||
|
||||
/-- Ensures that `FetchM` lifts into `JobM`. -/
|
||||
example : MonadLiftT FetchM JobM := inferInstance
|
||||
|
||||
/-- Ensures that `FetchM` lifts into `SpawnM`. -/
|
||||
example : MonadLiftT SpawnM FetchM := inferInstance
|
||||
|
||||
namespace Job
|
||||
|
||||
@[inline] def bindTask [Monad m]
|
||||
(f : JobTask α → m (JobTask β)) (self : Job α)
|
||||
: m (Job β) := return {self with task := ← f self.task}
|
||||
|
||||
/-- Spawn a job that asynchronously performs `act`. -/
|
||||
@[inline] protected def async
|
||||
(act : JobM α) (prio := Task.Priority.default)
|
||||
: SpawnM (Job α) := fun fetch stack store ctx => .ofTask <$> do
|
||||
BaseIO.asTask (prio := prio) do (withLoggedIO act) fetch stack store ctx {}
|
||||
|
||||
/-- Wait a the job to complete and return the result. -/
|
||||
@[inline] protected def wait (self : Job α) : BaseIO (JobResult α) := do
|
||||
IO.wait self.task
|
||||
|
||||
/--
|
||||
Wait for a job to complete and return the produced value.
|
||||
If an error occurred, return `none` and discarded any logs produced.
|
||||
-/
|
||||
@[inline] protected def wait? (self : Job α) : BaseIO (Option α) := do
|
||||
return (← self.wait).result?
|
||||
|
||||
/--
|
||||
Wait for a job to complete and return the produced value.
|
||||
Logs the job's log and throws if there was an error.
|
||||
-/
|
||||
@[inline] protected def await (self : Job α) : LogIO α := do
|
||||
match (← self.wait) with
|
||||
| .error n {log, ..} => log.replay; throw n
|
||||
| .ok a {log, ..} => log.replay; pure a
|
||||
|
||||
/-- Apply `f` asynchronously to the job's output. -/
|
||||
protected def mapM
|
||||
(self : Job α) (f : α → JobM β)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: SpawnM (Job β) :=
|
||||
fun fetch stack store ctx trace => do
|
||||
self.bindTask fun task => do
|
||||
BaseIO.mapTask (t := task) (prio := prio) (sync := sync) fun
|
||||
| .ok a s =>
|
||||
let trace := mixTrace trace s.trace
|
||||
withLoggedIO (f a) fetch stack store ctx {s with trace}
|
||||
| .error n s => return .error n s
|
||||
|
||||
@[deprecated Job.mapM (since := "2024-12-06")]
|
||||
protected abbrev bindSync
|
||||
(self : Job α) (f : α → JobM β)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: SpawnM (Job β) := self.mapM f prio sync
|
||||
|
||||
/--
|
||||
Apply `f` asynchronously to the job's output
|
||||
and asynchronously await the resulting job.
|
||||
-/
|
||||
def bindM
|
||||
(self : Job α) (f : α → JobM (Job β))
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: SpawnM (Job β) :=
|
||||
fun fetch stack store ctx trace => do
|
||||
self.bindTask fun task => do
|
||||
BaseIO.bindTask task (prio := prio) (sync := sync) fun
|
||||
| .ok a sa => do
|
||||
let trace := mixTrace trace sa.trace
|
||||
match (← withLoggedIO (f a) fetch stack store ctx {sa with trace}) with
|
||||
| .ok job sa =>
|
||||
return job.task.map (prio := prio) (sync := true) fun
|
||||
| .ok b sb => .ok b {sa.merge sb with trace := sb.trace}
|
||||
| .error e sb => .error ⟨sa.log.size + e.val⟩ {sa.merge sb with trace := sb.trace}
|
||||
| .error e sa => return Task.pure (.error e sa)
|
||||
| .error e sa => return Task.pure (.error e sa)
|
||||
|
||||
@[deprecated bindM (since := "2024-12-06")]
|
||||
protected abbrev bindAsync
|
||||
(self : Job α) (f : α → SpawnM (Job β))
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: SpawnM (Job β) := self.bindM (fun a => f a) prio sync
|
||||
|
||||
/--
|
||||
`a.zipWith f b` produces a new job `c` that applies `f` to the
|
||||
results of `a` and `b`. The job `c` errors if either `a` or `b` error.
|
||||
-/
|
||||
@[inline] def zipResultWith
|
||||
(f : JobResult α → JobResult β → JobResult γ) (self : Job α) (other : Job β)
|
||||
(prio := Task.Priority.default) (sync := true)
|
||||
: Job γ := Job.ofTask $
|
||||
self.task.bind (prio := prio) (sync := true) fun rx =>
|
||||
other.task.map (prio := prio) (sync := sync) fun ry =>
|
||||
f rx ry
|
||||
|
||||
/--
|
||||
`a.zipWith f b` produces a new job `c` that applies `f` to the
|
||||
results of `a` and `b`. The job `c` errors if either `a` or `b` error.
|
||||
-/
|
||||
@[inline] def zipWith
|
||||
(f : α → β → γ) (self : Job α) (other : Job β)
|
||||
(prio := Task.Priority.default) (sync := true)
|
||||
: Job γ :=
|
||||
self.zipResultWith (other := other) (prio := prio) (sync := sync) fun
|
||||
| .ok a sa, .ok b sb => .ok (f a b) (sa.merge sb)
|
||||
| ra, rb => .error 0 (ra.state.merge rb.state)
|
||||
|
||||
/-- Merges this job with another, discarding its output and trace. -/
|
||||
def add (self : Job α) (other : Job β) : Job α :=
|
||||
self.zipResultWith (other := other) fun
|
||||
| .ok a sa, .ok _ sb => .ok a {sa.merge sb with trace := sa.trace}
|
||||
| ra, rb => .error 0 {ra.state.merge rb.state with trace := ra.state.trace}
|
||||
|
||||
/-- Merges this job with another, discarding both outputs. -/
|
||||
def mix (self : Job α) (other : Job β) : Job Unit :=
|
||||
self.zipWith (fun _ _ => ()) other
|
||||
|
||||
/-- Merge a `List` of jobs into one, discarding their outputs. -/
|
||||
def mixList (jobs : List (Job α)) : Job Unit :=
|
||||
jobs.foldr (·.mix ·) nil
|
||||
|
||||
/-- Merge an `Array` of jobs into one, discarding their outputs. -/
|
||||
def mixArray (jobs : Array (Job α)) : Job Unit :=
|
||||
jobs.foldl (·.mix ·) nil
|
||||
|
||||
/-- Merge a `List` of jobs into one, collecting their outputs into a `List`. -/
|
||||
def collectList (jobs : List (Job α)) : Job (List α) :=
|
||||
jobs.foldr (zipWith List.cons) (pure [])
|
||||
|
||||
/-- Merge an `Array` of jobs into one, collecting their outputs into an `Array`. -/
|
||||
def collectArray (jobs : Array (Job α)) : Job (Array α) :=
|
||||
jobs.foldl (zipWith Array.push) (pure (Array.mkEmpty jobs.size))
|
||||
|
||||
end Job
|
||||
|
||||
/-! ## BuildJob (deprecated) -/
|
||||
|
||||
/-- A Lake build job. -/
|
||||
abbrev BuildJob α := Job α
|
||||
|
||||
namespace BuildJob
|
||||
|
||||
@[inline, deprecated "Obsolete." (since := "2024-12-06")]
|
||||
def mk (job : Job (α × BuildTrace)) : BuildJob α :=
|
||||
job.mapOk fun (a, trace) s => .ok a {s with trace}
|
||||
|
||||
@[inline, deprecated "Obsolete." (since := "2024-12-06")]
|
||||
def ofJob (job : Job BuildTrace) : BuildJob Unit :=
|
||||
job.mapOk fun trace s => .ok () {s with trace}
|
||||
|
||||
abbrev toJob (self : BuildJob α) : Job α :=
|
||||
self
|
||||
|
||||
@[deprecated Job.nil (since := "2024-12-06")]
|
||||
abbrev nil : BuildJob Unit :=
|
||||
Job.pure ()
|
||||
|
||||
@[deprecated Job.map (since := "2024-12-06")]
|
||||
protected abbrev pure (a : α) : BuildJob α :=
|
||||
Job.pure a
|
||||
|
||||
instance : Pure BuildJob := ⟨Job.pure⟩
|
||||
|
||||
@[deprecated Job.map (since := "2024-12-06")]
|
||||
protected abbrev map (f : α → β) (self : BuildJob α) : BuildJob β :=
|
||||
self.toJob.map f
|
||||
|
||||
instance : Functor BuildJob where
|
||||
map := Job.map
|
||||
|
||||
@[inline, deprecated "Removed without replacement." (since := "2024-12-06")]
|
||||
def mapWithTrace (f : α → BuildTrace → β × BuildTrace) (self : BuildJob α) : BuildJob β :=
|
||||
self.toJob.mapOk fun a s =>
|
||||
let (b, trace) := f a s.trace
|
||||
.ok b {s with trace}
|
||||
|
||||
@[inline, deprecated Job.mapM (since := "2024-12-06")]
|
||||
protected def bindSync
|
||||
(self : BuildJob α) (f : α → BuildTrace → JobM (β × BuildTrace))
|
||||
(prio : Task.Priority := .default) (sync := false)
|
||||
: SpawnM (Job β) :=
|
||||
self.toJob.mapM (prio := prio) (sync := sync) fun a => do
|
||||
let (b, trace) ← f a (← getTrace)
|
||||
setTrace trace
|
||||
return b
|
||||
|
||||
@[inline, deprecated Job.bindM (since := "2024-12-06")]
|
||||
protected def bindAsync
|
||||
(self : BuildJob α) (f : α → BuildTrace → SpawnM (Job β))
|
||||
(prio : Task.Priority := .default) (sync := false)
|
||||
: SpawnM (Job β) :=
|
||||
self.toJob.bindM (prio := prio) (sync := sync) fun a => do
|
||||
f a (← getTrace)
|
||||
|
||||
@[deprecated Job.wait? (since := "2024-12-06")]
|
||||
protected abbrev wait? (self : BuildJob α) : BaseIO (Option α) :=
|
||||
self.toJob.wait?
|
||||
|
||||
@[deprecated Job.add (since := "2024-12-06")]
|
||||
abbrev add (self : BuildJob α) (other : BuildJob β) : BuildJob α :=
|
||||
self.toJob.add other.toJob
|
||||
|
||||
@[deprecated Job.mix (since := "2024-12-06")]
|
||||
abbrev mix (self : BuildJob α) (other : BuildJob β) : BuildJob Unit :=
|
||||
self.toJob.mix other.toJob
|
||||
|
||||
@[deprecated Job.mixList (since := "2024-12-06")]
|
||||
abbrev mixList (jobs : List (BuildJob α)) : Id (BuildJob Unit) :=
|
||||
return Job.mixList jobs
|
||||
|
||||
@[deprecated Job.mixArray (since := "2024-12-06")]
|
||||
abbrev mixArray (jobs : Array (BuildJob α)) : Id (BuildJob Unit) :=
|
||||
return Job.mixArray jobs
|
||||
|
||||
@[deprecated Job.zipWith (since := "2024-12-06")]
|
||||
abbrev zipWith
|
||||
(f : α → β → γ) (self : BuildJob α) (other : BuildJob β)
|
||||
: BuildJob γ :=
|
||||
self.toJob.zipWith f other.toJob
|
||||
|
||||
@[deprecated Job.collectList (since := "2024-12-06")]
|
||||
abbrev collectList (jobs : List (BuildJob α)) : Id (BuildJob (List α)) :=
|
||||
return Job.collectList jobs
|
||||
|
||||
@[deprecated Job.collectArray (since := "2024-12-06")]
|
||||
abbrev collectArray (jobs : Array (BuildJob α)) : Id (BuildJob (Array α)) :=
|
||||
return Job.collectArray jobs
|
||||
|
||||
attribute [deprecated Job (since := "2024-12-06")] BuildJob
|
||||
78
src/lake/Lake/Build/Job/Register.lean
Normal file
78
src/lake/Lake/Build/Job/Register.lean
Normal file
|
|
@ -0,0 +1,78 @@
|
|||
/-
|
||||
Copyright (c) 2024 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Build.Fetch
|
||||
|
||||
/-! # Job Registration -/
|
||||
|
||||
namespace Lake
|
||||
|
||||
/--
|
||||
Resets the job state after a checkpoint (e.g., registering the job).
|
||||
Preserves state that downstream jobs want to depend on while resetting
|
||||
job-local state that should not be inherited by downstream jobs.
|
||||
-/
|
||||
@[inline] def JobState.renew (s : JobState) : JobState where
|
||||
trace := s.trace
|
||||
|
||||
/--
|
||||
Resets the job's state after a checkpoint (e.g., registering the job).
|
||||
Preserves information that downstream jobs want to depend on while resetting
|
||||
job-local information that should not be inherited by downstream jobs.
|
||||
-/
|
||||
def Job.renew (self : Job α) : Job α :=
|
||||
self.mapResult (sync := true) fun
|
||||
| .ok a s => .ok a s.renew
|
||||
| .error _ s => .error 0 s.renew
|
||||
|
||||
/--
|
||||
Registers the job for the top-level build monitor,
|
||||
(e.g., the Lake CLI progress UI), assigning it `caption`.
|
||||
-/
|
||||
def registerJob (caption : String) (job : Job α) (optional := false) : FetchM (Job α) := do
|
||||
let job : Job α := {job with caption, optional}
|
||||
(← getBuildContext).registeredJobs.modify (·.push job)
|
||||
return job.renew
|
||||
|
||||
/-- Wraps stray I/O, logs, and errors in `x` into the produced job. -/
|
||||
def ensureJob (x : FetchM (Job α))
|
||||
: FetchM (Job α) := fun fetch stack store ctx log => do
|
||||
let iniPos := log.endPos
|
||||
match (← (withLoggedIO x) fetch stack store ctx log) with
|
||||
| .ok job log =>
|
||||
if iniPos < log.endPos then
|
||||
let (log, jobLog) := log.split iniPos
|
||||
let job := job.mapResult (sync := true) (·.prependLog jobLog)
|
||||
return .ok job log
|
||||
else
|
||||
return .ok job log
|
||||
| .error _ log =>
|
||||
let (log, jobLog) := log.split iniPos
|
||||
return .ok (.error jobLog) log
|
||||
|
||||
/--
|
||||
Registers the produced job for the top-level build monitor
|
||||
(e.g., the Lake CLI progress UI), assigning it `caption`.
|
||||
|
||||
Stray I/O, logs, and errors produced by `x` will be wrapped into the job.
|
||||
-/
|
||||
def withRegisterJob
|
||||
(caption : String) (x : FetchM (Job α)) (optional := false)
|
||||
: FetchM (Job α) := do
|
||||
let job ← ensureJob x
|
||||
registerJob caption job optional
|
||||
|
||||
/--
|
||||
Registers the produced job for the top-level build monitor
|
||||
if it is not already (i.e., it has an empty caption).
|
||||
-/
|
||||
@[inline] def maybeRegisterJob
|
||||
(caption : String) (job : Job α)
|
||||
: FetchM (Job α) := do
|
||||
if job.caption.isEmpty then
|
||||
registerJob caption job
|
||||
else
|
||||
return job
|
||||
|
|
@ -47,12 +47,12 @@ we equip the monad `m` with a fetch function of its own.
|
|||
-/
|
||||
|
||||
/-- A transformer that equips a monad with a `DFetchFn`. -/
|
||||
abbrev DFetchT (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
|
||||
abbrev DFetchFnT (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
|
||||
EquipT (DFetchFn α β m) m
|
||||
|
||||
/-- A `DFetchT` that is not dependently typed. -/
|
||||
abbrev FetchT (α : Type u) (β : Type v) (m : Type v → Type w) :=
|
||||
DFetchT α (fun _ => β) m
|
||||
/-- A `DFetchFnT` that is not dependently typed. -/
|
||||
abbrev FetchFnT (α : Type u) (β : Type v) (m : Type v → Type w) :=
|
||||
DFetchFnT α (fun _ => β) m
|
||||
|
||||
/-!
|
||||
We can then use the such a monad as the basis for a fetch function itself.
|
||||
|
|
@ -64,11 +64,11 @@ fetch values. It is thus usually implemented recursively via some variation
|
|||
of the `recFetch` function below, hence the "rec" in both names.
|
||||
-/
|
||||
abbrev DRecFetchFn (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
|
||||
DFetchFn α β (DFetchT α β m)
|
||||
DFetchFn α β (DFetchFnT α β m)
|
||||
|
||||
/-- A `DRecFetchFn` that is not dependently typed. -/
|
||||
abbrev RecFetchFn (α : Type u) (β : Type v) (m : Type v → Type w) :=
|
||||
α → FetchT α β m β
|
||||
α → FetchFnT α β m β
|
||||
|
||||
/-- A `DFetchFn` that provides its base `DRecFetchFn` with itself. -/
|
||||
@[specialize] partial def recFetch
|
||||
|
|
|
|||
|
|
@ -5,6 +5,7 @@ Authors: Mac Malone
|
|||
-/
|
||||
prelude
|
||||
import Lake.Config.Monad
|
||||
import Lake.Build.Job
|
||||
import Lake.CLI.Error
|
||||
|
||||
namespace Lake
|
||||
|
|
|
|||
|
|
@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Build.Job
|
||||
import Lake.Build.Data
|
||||
import Lake.Build.Job.Basic
|
||||
|
||||
namespace Lake
|
||||
open Lean System
|
||||
|
|
|
|||
|
|
@ -267,6 +267,7 @@ end MonadLogT
|
|||
/- A Lake log. An `Array` of log entries. -/
|
||||
structure Log where
|
||||
entries : Array LogEntry
|
||||
deriving Inhabited
|
||||
|
||||
instance : ToJson Log := ⟨(toJson ·.entries)⟩
|
||||
instance : FromJson Log := ⟨(Log.mk <$> fromJson? ·)⟩
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue