This file provides a thin ServerTask wrapper over the Task API. All calls to the Task API in the language server should go through this API.

The reason for this API is that the elaborator consuming threads from the thread pool should never hinder language server operations. Specifically, we want to ensure the following:

• All new tasks spawned in the language server must be dedicated so that they cannot be starved by the elaborator.
  • Dedicated tasks are costly, so avoid spawning new tasks for operations that are so cheap that they can just be done on the current thread instead.
• When mapping or binding a task:
  • If the function being mapped is sufficiently cheap that it can run on the current thread, map it with sync := true. This runs the function on the current thread if the task has already finished, or it reuses the thread of the task if the task has not finished. This ensures that the function to be executed cannot be starved by the elaborator.
  • If the function being mapped is not cheap / costly, map it with prio := .dedicated. This spawns a new thread and thus cannot be starved by the elaborator. Finally, if the function being mapped is costly, but is already being executed in a dedicated task, it is fine to pretend that it is a cheap function instead.

In request handlers, the distinction of whether an operation is "cheap" or "costly" should be decided by the following:

• If the operation is sufficiently fast that it could run on the main task of the language server, blocking all other communication for a brief moment, then it can be considered cheap.
• If the operation is being executed in a dedicated task that isn't the main task of the server, it can also be considered cheap.
• Otherwise, it is to be considered costly.

structure Lean.Server.ServerTask (α : Type u) : Type u

• task : Task α

Instances For

• Lean.Server.instCoeTaskServerTask
• Lean.Server.instInhabitedServerTask

instance Lean.Server.instInhabitedServerTask {a✝ : Type u_1} [Inhabited a✝] : Inhabited (ServerTask a✝)

Equations

• Lean.Server.instInhabitedServerTask = { default := { task := default } }

instance Lean.Server.instCoeTaskServerTask {α : Type u_1} : Coe (Task α) (ServerTask α)

Equations

• Lean.Server.instCoeTaskServerTask = { coe := Lean.Server.ServerTask.mk }

def Lean.Server.ServerTask.pure {α : Type u_1} (x : α) : ServerTask α

Equations

• Lean.Server.ServerTask.pure x = { task := { get := x } }

def Lean.Server.ServerTask.get {α : Type u_1} (t : ServerTask α) : α

Equations

• t.get = t.task.get

def Lean.Server.ServerTask.mapCheap {α : Type u_1} {β : Type u_2} (f : α → β) (t : ServerTask α) : ServerTask β

Equations

• Lean.Server.ServerTask.mapCheap f t = { task := Task.map f t.task Task.Priority.default true }

def Lean.Server.ServerTask.mapCostly {α : Type u_1} {β : Type u_2} (f : α → β) (t : ServerTask α) : ServerTask β

Equations

• Lean.Server.ServerTask.mapCostly f t = { task := Task.map f t.task Task.Priority.dedicated }

def Lean.Server.ServerTask.bindCheap {α : Type u_1} {β : Type u_2} (t : ServerTask α) (f : α → ServerTask β) : ServerTask β

Equations

• t.bindCheap f = { task := t.task.bind (fun (x : α) => (f x).task) Task.Priority.default true }

def Lean.Server.ServerTask.bindCostly {α : Type u_1} {β : Type u_2} (t : ServerTask α) (f : α → ServerTask β) : ServerTask β

Equations

• t.bindCostly f = { task := t.task.bind (fun (x : α) => (f x).task) Task.Priority.dedicated }

def Lean.Server.ServerTask.BaseIO.asTask {α : Type} (act : BaseIO α) : BaseIO (ServerTask α)

Equations

• Lean.Server.ServerTask.BaseIO.asTask act = do let a ← act.asTask Task.Priority.dedicated pure { task := a }

def Lean.Server.ServerTask.BaseIO.mapTaskCheap {α : Type u_1} {β : Type} (f : α → BaseIO β) (t : ServerTask α) : BaseIO (ServerTask β)

Equations

• Lean.Server.ServerTask.BaseIO.mapTaskCheap f t = do let a ← BaseIO.mapTask f t.task Task.Priority.default true pure { task := a }

def Lean.Server.ServerTask.BaseIO.mapTaskCostly {α : Type u_1} {β : Type} (f : α → BaseIO β) (t : ServerTask α) : BaseIO (ServerTask β)

Equations

• Lean.Server.ServerTask.BaseIO.mapTaskCostly f t = do let a ← BaseIO.mapTask f t.task Task.Priority.dedicated pure { task := a }

def Lean.Server.ServerTask.BaseIO.bindTaskCheap {α : Type u_1} {β : Type} (t : ServerTask α) (f : α → BaseIO (ServerTask β)) : BaseIO (ServerTask β)

Equations

• Lean.Server.ServerTask.BaseIO.bindTaskCheap t f = do let a ← BaseIO.bindTask t.task (fun (x : α) => Lean.Server.ServerTask.task <$> f x) Task.Priority.default true pure { task := a }

def Lean.Server.ServerTask.BaseIO.bindTaskCostly {α : Type u_1} {β : Type} (t : ServerTask α) (f : α → BaseIO (ServerTask β)) : BaseIO (ServerTask β)

Equations

• Lean.Server.ServerTask.BaseIO.bindTaskCostly t f = do let a ← BaseIO.bindTask t.task (fun (x : α) => Lean.Server.ServerTask.task <$> f x) Task.Priority.dedicated pure { task := a }

def Lean.Server.ServerTask.EIO.asTask {ε α : Type} (act : EIO ε α) : BaseIO (ServerTask (Except ε α))

Equations

• Lean.Server.ServerTask.EIO.asTask act = do let a ← act.asTask Task.Priority.dedicated pure { task := a }

def Lean.Server.ServerTask.EIO.mapTaskCheap {α : Type u_1} {ε β : Type} (f : α → EIO ε β) (t : ServerTask α) : BaseIO (ServerTask (Except ε β))

Equations

• Lean.Server.ServerTask.EIO.mapTaskCheap f t = do let a ← EIO.mapTask f t.task Task.Priority.default true pure { task := a }

def Lean.Server.ServerTask.EIO.mapTaskCostly {α : Type u_1} {ε β : Type} (f : α → EIO ε β) (t : ServerTask α) : BaseIO (ServerTask (Except ε β))

Equations

• Lean.Server.ServerTask.EIO.mapTaskCostly f t = do let a ← EIO.mapTask f t.task Task.Priority.dedicated pure { task := a }

def Lean.Server.ServerTask.EIO.bindTaskCheap {α : Type u_1} {ε β : Type} (t : ServerTask α) (f : α → EIO ε (ServerTask (Except ε β))) : BaseIO (ServerTask (Except ε β))

Equations

• Lean.Server.ServerTask.EIO.bindTaskCheap t f = do let a ← EIO.bindTask t.task (fun (x : α) => Lean.Server.ServerTask.task <$> f x) Task.Priority.default true pure { task := a }

def Lean.Server.ServerTask.EIO.bindTaskCostly {α : Type u_1} {ε β : Type} (t : ServerTask α) (f : α → EIO ε (ServerTask (Except ε β))) : BaseIO (ServerTask (Except ε β))

Equations

• Lean.Server.ServerTask.EIO.bindTaskCostly t f = do let a ← EIO.bindTask t.task (fun (x : α) => Lean.Server.ServerTask.task <$> f x) Task.Priority.dedicated pure { task := a }

def Lean.Server.ServerTask.IO.asTask {α : Type} (act : IO α) : BaseIO (ServerTask (Except IO.Error α))

Equations

• Lean.Server.ServerTask.IO.asTask act = do let a ← act.asTask Task.Priority.dedicated pure { task := a }

def Lean.Server.ServerTask.IO.mapTaskCheap {α : Type u_1} {β : Type} (f : α → IO β) (t : ServerTask α) : BaseIO (ServerTask (Except IO.Error β))

Equations

• Lean.Server.ServerTask.IO.mapTaskCheap f t = do let a ← IO.mapTask f t.task Task.Priority.default true pure { task := a }

def Lean.Server.ServerTask.IO.mapTaskCostly {α : Type u_1} {β : Type} (f : α → IO β) (t : ServerTask α) : BaseIO (ServerTask (Except IO.Error β))

Equations

• Lean.Server.ServerTask.IO.mapTaskCostly f t = do let a ← IO.mapTask f t.task Task.Priority.dedicated pure { task := a }

def Lean.Server.ServerTask.IO.bindTaskCheap {α : Type u_1} {β : Type} (t : ServerTask α) (f : α → IO (ServerTask (Except IO.Error β))) : BaseIO (ServerTask (Except IO.Error β))

Equations

• Lean.Server.ServerTask.IO.bindTaskCheap t f = do let a ← IO.bindTask t.task (fun (x : α) => Lean.Server.ServerTask.task <$> f x) Task.Priority.default true pure { task := a }

def Lean.Server.ServerTask.IO.bindTaskCostly {α : Type u_1} {β : Type} (t : ServerTask α) (f : α → IO (ServerTask (Except IO.Error β))) : BaseIO (ServerTask (Except IO.Error β))

Equations

• Lean.Server.ServerTask.IO.bindTaskCostly t f = do let a ← IO.bindTask t.task (fun (x : α) => Lean.Server.ServerTask.task <$> f x) Task.Priority.dedicated pure { task := a }

def Lean.Server.ServerTask.hasFinished {α : Type u_1} (t : ServerTask α) : BaseIO Bool

Equations

• t.hasFinished = IO.hasFinished t.task

def Lean.Server.ServerTask.waitAny {α : Type} (tasks : List (ServerTask α)) (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) : BaseIO α

Equations

• Lean.Server.ServerTask.waitAny tasks h = IO.waitAny (List.map (fun (x : Lean.Server.ServerTask α) => x.task) tasks) ⋯

def Lean.Server.ServerTask.cancel {α : Type u_1} (t : ServerTask α) : BaseIO Unit

Equations

• t.cancel = IO.cancel t.task

def Task.asServerTask {α : Type u_1} (t : Task α) : Lean.Server.ServerTask α

Equations

• t.asServerTask = { task := t }