diff --git a/Lake/Build/Job.lean b/Lake/Build/Job.lean index 11c75be7c2..5b3ba7f27a 100644 --- a/Lake/Build/Job.lean +++ b/Lake/Build/Job.lean @@ -31,8 +31,8 @@ namespace Job await self @[inline] protected def bindSync -(self : Job α) (f : α → JobM β) : SchedulerM (Job β) := - bindSync self f +(self : Job α) (f : α → JobM β) (prio := Task.Priority.default) : SchedulerM (Job β) := + bindSync prio self f @[inline] protected def bindAsync (self : Job α) (f : α → SchedulerM (Job β)) : SchedulerM (Job β) := @@ -69,8 +69,9 @@ instance : Functor BuildJob where map := BuildJob.map @[inline] protected def bindSync -(self : BuildJob α) (f : α → BuildTrace → JobM β) : SchedulerM (Job β) := - self.toJob.bindSync fun (a, t) => f a t +(self : BuildJob α) (f : α → BuildTrace → JobM β) +(prio : Task.Priority := .default) : SchedulerM (Job β) := + self.toJob.bindSync (prio := prio) fun (a, t) => f a t @[inline] protected def bindAsync (self : BuildJob α) (f : α → BuildTrace → SchedulerM (Job β)) : SchedulerM (Job β) := diff --git a/Lake/Util/Async.lean b/Lake/Util/Async.lean index 1740a632de..f52ddb143e 100644 --- a/Lake/Util/Async.lean +++ b/Lake/Util/Async.lean @@ -101,7 +101,7 @@ instance [Await k m] : Await (OptionT k) (OptionT m) where class BindSync (m : Type u → Type v) (n : outParam $ Type u' → Type w) (k : outParam $ Type u → Type u') where /-- Perform a synchronous action after another (a)synchronous task completes successfully. -/ - bindSync {α β : Type u} : k α → (α → m β) → n (k β) + bindSync {α β : Type u} : Task.Priority → k α → (α → m β) → n (k β) export BindSync (bindSync) @@ -143,29 +143,29 @@ extends SeqAsync n k, SeqLeftAsync n k, SeqRightAsync n k, SeqWithAsync n k wher /-! ## Standard Instances -/ -instance : BindSync Id Id Task := ⟨flip Task.map⟩ -instance : BindSync BaseIO BaseIO BaseIOTask := ⟨flip BaseIO.mapTask⟩ +instance : BindSync Id Id Task := ⟨fun _ => flip Task.map⟩ +instance : BindSync BaseIO BaseIO BaseIOTask := ⟨fun _ => flip BaseIO.mapTask⟩ instance : BindSync (EIO ε) BaseIO (ETask ε) where - bindSync ka f := ka.run |> BaseIO.mapTask fun + bindSync prio ka f := ka.run |> BaseIO.mapTask (prio := prio) fun | Except.ok a => f a |>.toBaseIO | Except.error e => pure <| Except.error e instance : BindSync OptionIO BaseIO OptionIOTask where - bindSync ka f := ka.run |> BaseIO.mapTask fun + bindSync prio ka f := ka.run |> BaseIO.mapTask (prio := prio) fun | some a => f a |>.toBaseIO | none => pure none instance [BindSync m n k] : BindSync (ReaderT ρ m) (ReaderT ρ n) k where - bindSync ka f := fun r => bindSync ka fun a => f a r + bindSync prio ka f := fun r => bindSync prio ka fun a => f a r instance [BindSync m n k] [Pure m] : BindSync (ExceptT ε m) n (ExceptT ε k) where - bindSync ka f := cast (by delta ExceptT; rfl) <| bindSync (n := n) ka.run fun + bindSync prio ka f := cast (by delta ExceptT; rfl) <| bindSync prio (n := n) ka.run fun | Except.ok a => f a |>.run | Except.error e => pure <| Except.error e instance [BindSync m n k] [Pure m] : BindSync (OptionT m) n (OptionT k) where - bindSync ka f := cast (by delta OptionT; rfl) <| bindSync ka.run fun + bindSync prio ka f := cast (by delta OptionT; rfl) <| bindSync prio ka.run fun | some a => f a |>.run | none => pure none