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 α

@[implicit_reducible]

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

def Lean.Server.instInhabitedServerTask.default {a✝ : Type u_1} [Inhabited a✝] : ServerTask a✝

@[implicit_reducible]

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

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

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

def Lean.Server.ServerTask.wait {α : Type} (t : ServerTask α) : BaseIO α

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

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

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

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

def Lean.Server.ServerTask.join {α : Type u_1} (ts : Array (ServerTask α)) : ServerTask (Array α)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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