Allows LSP clients to make Remote Procedure Calls to the server.

The single use case for these is to allow the infoview UI to refer to and manipulate heavy-weight objects residing on the server. It would be inefficient to serialize these into JSON and send over. For example, the client can format an Expr without transporting the whole Environment.

All RPC requests are relative to an open file and an RPC session for that file. The client must first connect to the session using $/lean/rpc/connect.

structure Lean.Lsp.RpcRef : Type

An object which RPC clients can refer to without marshalling.

• p : USize

instance Lean.Lsp.instBEqRpcRef : BEq Lean.Lsp.RpcRef

Equations

• Lean.Lsp.instBEqRpcRef = { beq := Lean.Lsp.beqRpcRef✝ }

instance Lean.Lsp.instHashableRpcRef : Hashable Lean.Lsp.RpcRef

instance Lean.Lsp.instFromJsonRpcRef : Lean.FromJson Lean.Lsp.RpcRef

instance Lean.Lsp.instToJsonRpcRef : Lean.ToJson Lean.Lsp.RpcRef

Equations

• Lean.Lsp.instToJsonRpcRef = { toJson := Lean.Lsp.toJsonRpcRef✝ }

instance Lean.Lsp.instToStringRpcRef : ToString Lean.Lsp.RpcRef

structure Lean.Server.RpcObjectStore : Type

• aliveRefs : Lean.PersistentHashMap Lean.Lsp.RpcRef Dynamic

  Objects that are being kept alive for the RPC client, together with their type names, mapped to by their RPC reference.

  Note that we may currently have multiple references to the same object. It is only disposed of once all of those are gone. This simplifies the client a bit as it can drop every reference received separately.

• nextRef : USize

  Value to use for the next RpcRef. It is monotonically increasing to avoid any possible bugs resulting from its reuse.

def Lean.Server.rpcStoreRef (any : Dynamic) : StateM Lean.Server.RpcObjectStore Lean.Lsp.RpcRef

def Lean.Server.rpcGetRef (r : Lean.Lsp.RpcRef) : ReaderT Lean.Server.RpcObjectStore Id (Option Dynamic)

Equations

• Lean.Server.rpcGetRef r = do let __do_lift ← read pure (__do_lift.aliveRefs.find? r)

def Lean.Server.rpcReleaseRef (r : Lean.Lsp.RpcRef) : StateM Lean.Server.RpcObjectStore Bool

class Lean.Server.RpcEncodable (α : Type) : Type

RpcEncodable α means that α can be deserialized from and serialized into JSON for the purpose of receiving arguments to and sending return values from Remote Procedure Calls (RPCs).

Any type with FromJson and ToJson instances is RpcEncodable.

Furthermore, types that do not have these instances may still be RpcEncodable. Use deriving RpcEncodable to automatically derive instances for such types.

This occurs when α contains data that should not or cannot be serialized: for instance, heavy objects such as Lean.Environment, or closures. For such data, we use the WithRpcRef marker. Note that for WithRpcRef α to be RpcEncodable, α must have a TypeName instance

On the server side, WithRpcRef α is just a structure containing a value of type α. On the client side, it is an opaque reference of (structural) type Lsp.RpcRef. Thus, WithRpcRef α is cheap to transmit over the network but may only be accessed on the server side. In practice, it is used by the client to pass data between various RPC methods provided by the server.

• rpcEncode : α → StateM Lean.Server.RpcObjectStore Lean.Json
• rpcDecode : Lean.Json → ExceptT String (ReaderT Lean.Server.RpcObjectStore Id) α

theorem Lean.Server.instNonemptyRpcEncodable {α : Type} : Nonempty (Lean.Server.RpcEncodable α)

instance Lean.Server.instRpcEncodableOfFromJsonOfToJson {α : Type} [Lean.FromJson α] [Lean.ToJson α] : Lean.Server.RpcEncodable α

instance Lean.Server.instRpcEncodableOption {α : Type} [Lean.Server.RpcEncodable α] : Lean.Server.RpcEncodable (Option α)

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Server.instRpcEncodableArray {α : Type} [Lean.Server.RpcEncodable α] : Lean.Server.RpcEncodable (Array α)

instance Lean.Server.instRpcEncodableProd {α β : Type} [Lean.Server.RpcEncodable α] [Lean.Server.RpcEncodable β] : Lean.Server.RpcEncodable (α × β)

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Server.instRpcEncodableStateMRpcObjectStore {α : Type} [Lean.Server.RpcEncodable α] : Lean.Server.RpcEncodable (StateM Lean.Server.RpcObjectStore α)

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

Marks values to be encoded as opaque references in RPC packets.

See the docstring for RpcEncodable.

• val : α

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

instance Lean.Server.instRpcEncodableWithRpcRefOfTypeName {α : Type} [TypeName α] : Lean.Server.RpcEncodable (Lean.Server.WithRpcRef α)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.instRpcEncodableWithRpcRefOfTypeName.rpcEncode {α : Type} [TypeName α] (r : Lean.Server.WithRpcRef α) : StateM Lean.Server.RpcObjectStore Lean.Json

Equations

• Lean.Server.instRpcEncodableWithRpcRefOfTypeName.rpcEncode r = Lean.toJson <$> Lean.Server.rpcStoreRef (Dynamic.mk r.val)

def Lean.Server.instRpcEncodableWithRpcRefOfTypeName.rpcDecode {α : Type} [TypeName α] (j : Lean.Json) : ExceptT String (ReaderT Lean.Server.RpcObjectStore Id) (Lean.Server.WithRpcRef α)