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

The address of an object in an RpcObjectStore that clients can refer to. Its JSON encoding depends on the RPC wire format.

The language server may serve the same RpcRef multiple times. It maintains a reference count to track how many times it has served the reference. If clients want to release the object associated with an RpcRef, they must release the reference as many times as they have received it from the server.

• p : USize

@[implicit_reducible]

instance Lean.Lsp.instInhabitedRpcRef : Inhabited RpcRef

Equations

• Lean.Lsp.instInhabitedRpcRef = { default := Lean.Lsp.instInhabitedRpcRef.default }

def Lean.Lsp.instInhabitedRpcRef.default : RpcRef

Equations

• Lean.Lsp.instInhabitedRpcRef.default = { p := default }

@[implicit_reducible]

instance Lean.Lsp.instBEqRpcRef : BEq RpcRef

Equations

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

def Lean.Lsp.instBEqRpcRef.beq : RpcRef → RpcRef → Bool

Equations

• Lean.Lsp.instBEqRpcRef.beq { p := a } { p := b } = (a == b)
• Lean.Lsp.instBEqRpcRef.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Lean.Lsp.instHashableRpcRef : Hashable RpcRef

Equations

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

def Lean.Lsp.instHashableRpcRef.hash : RpcRef → UInt64

Equations

• Lean.Lsp.instHashableRpcRef.hash { p := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance Lean.Lsp.instToStringRpcRef : ToString RpcRef

Equations

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

inductive Lean.Lsp.RpcWireFormat : Type

The RPC wire format specifies how user data is encoded in RPC requests.

• v0 : RpcWireFormat

  Version 0 uses JSON. Serialized RPC data is stored directly in RpcCallParams.params and in JsonRpc.Response.result (as opposed to being wrapped in additional metadata). General types (except RPC references) are (de)serialized via ToJson/FromJson. RPC references are serialized as {"p": n}.

• v1 : RpcWireFormat

  Version 1 is like 0, except that RPC references are serialized as {"__rpcref": n}.

def Lean.Lsp.instFromJsonRpcWireFormat.fromJson : Json → Except String RpcWireFormat

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonRpcWireFormat : FromJson RpcWireFormat

Equations

• Lean.Lsp.instFromJsonRpcWireFormat = { fromJson? := Lean.Lsp.instFromJsonRpcWireFormat.fromJson }

def Lean.Lsp.instToJsonRpcWireFormat.toJson : RpcWireFormat → Json

Equations

• Lean.Lsp.instToJsonRpcWireFormat.toJson Lean.Lsp.RpcWireFormat.v0 = Lean.toJson "v0"
• Lean.Lsp.instToJsonRpcWireFormat.toJson Lean.Lsp.RpcWireFormat.v1 = Lean.toJson "v1"

@[implicit_reducible]

instance Lean.Lsp.instToJsonRpcWireFormat : ToJson RpcWireFormat

Equations

• Lean.Lsp.instToJsonRpcWireFormat = { toJson := Lean.Lsp.instToJsonRpcWireFormat.toJson }

@[inline]

def Lean.Lsp.RpcWireFormat.refFieldName : RpcWireFormat → String

Equations

• Lean.Lsp.RpcWireFormat.v0.refFieldName = "p"
• Lean.Lsp.RpcWireFormat.v1.refFieldName = "__rpcref"

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

WithRpcRef α marks values that RPC clients should see as opaque references. This includes heavy objects such as Lean.Environments and non-serializable objects such as closures.

In the Lean server, WithRpcRef α is a structure containing a value of type α and an associated id. In an RPC client (e.g. the infoview), it is an opaque reference. Thus, WithRpcRef α is cheap to transmit, but its data may only be accessed server-side. In practice, this is used by client code to pass data between various RPC methods provided by the server.

Two WithRpcRefs with the same id will yield the same client-side reference.

See also the docstring for RpcEncodable.

• mk' :: (
• val : α
• id : USize
• )

def Lean.Server.instInhabitedWithRpcRef.default {a✝ : Type u_1} [Inhabited a✝] : WithRpcRef a✝

Equations

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

@[implicit_reducible]

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

Equations

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

opaque Lean.Server.freshWithRpcRefId : IO.Ref USize

def Lean.Server.WithRpcRef.mk {α : Type} (val : α) : BaseIO (WithRpcRef α)

Creates an WithRpcRef instance with a unique id. As long as the client holds at least one reference to this WithRpcRef, serving it again will yield the same client-side reference. Thus, when used as React deps, client-side references can help preserve UI state across RPC requests.

Equations

• Lean.Server.WithRpcRef.mk val = do let id ← ST.Ref.modifyGet Lean.Server.freshWithRpcRefId fun (id : USize) => (id, id + 1) pure { val := val, id := id }

structure Lean.Server.ReferencedObject : Type

• obj : Dynamic
• id : USize
• rc : Nat

structure Lean.Server.RpcObjectStore : Type

• aliveRefs : PersistentHashMap Lsp.RpcRef ReferencedObject

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

• refsById : PersistentHashMap USize Lsp.RpcRef

  Unique RpcRef for the ID of an object that is being referenced through RPC. We store this mapping so that we can reuse RpcRefs for the same object. Reusing RpcRefs is helpful because it enables clients to reuse their UI state.

• nextRef : USize

  Value to use for the next fresh RpcRef, monotonically increasing.

• wireFormat : Lsp.RpcWireFormat

  The RPC wire format to follow.

def Lean.Server.rpcStoreRef {α : Type u_1} [TypeName α] (obj : WithRpcRef α) : StateM RpcObjectStore Lsp.RpcRef

Equations

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

def Lean.Server.rpcGetRef (α : Type) [TypeName α] (r : Lsp.RpcRef) : ReaderT RpcObjectStore (ExceptT String Id) (WithRpcRef α)

Equations

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

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

Equations

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

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

RpcEncodable α means α can be used as an argument or return value in Remote Procedure Call (RPC) methods.

The following types are RpcEncodable by default:

• Any type with both FromJson and ToJson instances.
• Any type all of whose components (meaning the fields of a structure, or the arguments to inductive constructors) are RpcEncodable. Use deriving RpcEncodable to construct an instance in this case.
• Certain common containers, if containing RpcEncodable data (see instances below).
• Any WithRpcRef α where [TypeName α].

Some names are reserved for internal use and must not appear as the name of a field or constructor argument in any RpcEncodable type, or as an object key in any nested JSON. The following are currently reserved:

• __rpcref

It is also possible (but discouraged for non-experts) to implement custom RpcEncodable instances. These must respect the RpcObjectStore.wireFormat.

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

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

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

Equations

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