Documentation

Lean.Server.ServerTask

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:

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

structure Lean.Server.ServerTask (α : Type u) :
Instances For
    Equations
      Equations
        def Lean.Server.ServerTask.pure {α : Type u_1} (x : α) :
        Equations
          Instances For
            def Lean.Server.ServerTask.get {α : Type u_1} (t : ServerTask α) :
            α
            Equations
              Instances For
                def Lean.Server.ServerTask.mapCheap {α : Type u_1} {β : Type u_2} (f : αβ) (t : ServerTask α) :
                Equations
                  Instances For
                    def Lean.Server.ServerTask.mapCostly {α : Type u_1} {β : Type u_2} (f : αβ) (t : ServerTask α) :
                    Equations
                      Instances For
                        def Lean.Server.ServerTask.bindCheap {α : Type u_1} {β : Type u_2} (t : ServerTask α) (f : αServerTask β) :
                        Equations
                          Instances For
                            def Lean.Server.ServerTask.bindCostly {α : Type u_1} {β : Type u_2} (t : ServerTask α) (f : αServerTask β) :
                            Equations
                              Instances For
                                Equations
                                  Instances For
                                    Equations
                                      Instances For
                                        def Lean.Server.ServerTask.BaseIO.mapTaskCheap {α : Type u_1} {β : Type} (f : αBaseIO β) (t : ServerTask α) :
                                        Equations
                                          Instances For
                                            def Lean.Server.ServerTask.BaseIO.mapTaskCostly {α : Type u_1} {β : Type} (f : αBaseIO β) (t : ServerTask α) :
                                            Equations
                                              Instances For
                                                def Lean.Server.ServerTask.BaseIO.bindTaskCheap {α : Type u_1} {β : Type} (t : ServerTask α) (f : αBaseIO (ServerTask β)) :
                                                Equations
                                                  Instances For
                                                    Equations
                                                      Instances For
                                                        def Lean.Server.ServerTask.EIO.asTask {ε α : Type} (act : EIO ε α) :
                                                        Equations
                                                          Instances For
                                                            def Lean.Server.ServerTask.EIO.mapTaskCheap {α : Type u_1} {ε β : Type} (f : αEIO ε β) (t : ServerTask α) :
                                                            Equations
                                                              Instances For
                                                                def Lean.Server.ServerTask.EIO.mapTaskCostly {α : Type u_1} {ε β : Type} (f : αEIO ε β) (t : ServerTask α) :
                                                                Equations
                                                                  Instances For
                                                                    def Lean.Server.ServerTask.EIO.bindTaskCheap {α : Type u_1} {ε β : Type} (t : ServerTask α) (f : αEIO ε (ServerTask (Except ε β))) :
                                                                    Equations
                                                                      Instances For
                                                                        def Lean.Server.ServerTask.EIO.bindTaskCostly {α : Type u_1} {ε β : Type} (t : ServerTask α) (f : αEIO ε (ServerTask (Except ε β))) :
                                                                        Equations
                                                                          Instances For
                                                                            Equations
                                                                              Instances For
                                                                                def Lean.Server.ServerTask.IO.mapTaskCheap {α : Type u_1} {β : Type} (f : αIO β) (t : ServerTask α) :
                                                                                Equations
                                                                                  Instances For
                                                                                    def Lean.Server.ServerTask.IO.mapTaskCostly {α : Type u_1} {β : Type} (f : αIO β) (t : ServerTask α) :
                                                                                    Equations
                                                                                      Instances For
                                                                                        Equations
                                                                                          Instances For
                                                                                            Equations
                                                                                              Instances For
                                                                                                Equations
                                                                                                  Instances For
                                                                                                    def Lean.Server.ServerTask.waitAny {α : Type} (tasks : List (ServerTask α)) (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) :
                                                                                                    Equations
                                                                                                      Instances For
                                                                                                        Equations
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                              Instances For