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

• p : USize

An object which RPC clients can refer to without marshalling.

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

Equations

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

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

Equations

• Lean.Lsp.instHashableRpcRef = { hash := Lean.Lsp.hashRpcRef✝ }

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

Equations

• Lean.Lsp.instFromJsonRpcRef = { fromJson? := Lean.Lsp.fromJsonRpcRef✝ }

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

Equations

• Lean.Lsp.instToStringRpcRef = { toString := fun r => toString r.p }

structure Lean.Server.RpcObjectStore : Type

• 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.

  aliveRefs : Lean.PersistentHashMap Lean.Lsp.RpcRef Dynamic

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

  nextRef : USize

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

Equations

• Lean.Server.rpcStoreRef any = do let st ← get set { aliveRefs := Lean.PersistentHashMap.insert st.aliveRefs { p := st.nextRef } any, nextRef := st.nextRef + 1 } pure { p := st.nextRef }

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 (Lean.PersistentHashMap.find? __do_lift.aliveRefs r)

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

Equations

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

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

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

RpcEncodable α means that α can be serialized in the RPC system of the Lean server. This is required when α contains fields which should be serialized as an RPC reference instead of being sent in full. The type wrapper WithRpcRef is used for these fields which should be sent as a reference.

• Any type with FromJson and ToJson instance is automatically RpcEncodable.
• If a type has an Dynamic instance, then WithRpcRef can be used for its references.
• deriving RpcEncodable acts like FromJson/ToJson but marshalls any WithRpcRef fields as Lsp.RpcRefs.

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

Equations

• @Lean.Server.instNonemptyRpcEncodable = @Lean.Server.instNonemptyRpcEncodable.proof_1

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

Equations

• Lean.Server.instRpcEncodable = { rpcEncode := fun a => pure (Lean.toJson a), rpcDecode := fun j => ofExcept (Lean.fromJson? j) }

instance Lean.Server.instRpcEncodableOption {α : Type} [inst : 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} [inst : Lean.Server.RpcEncodable α] : Lean.Server.RpcEncodable (Array α)

Equations

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

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

Equations

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

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

• val : α

Marks fields to encode as opaque references in LSP packets.

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

Equations

• Lean.Server.instInhabitedWithRpcRef = { default := { val := default } }

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

Equations

• Lean.Server.instRpcEncodableWithRpcRef = { rpcEncode := Lean.Server.instRpcEncodableWithRpcRef.rpcEncode, rpcDecode := Lean.Server.instRpcEncodableWithRpcRef.rpcDecode }

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

Equations

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

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

Equations

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