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

source
structure Lean.Lsp.RpcRef :
Type

An object which RPC clients can refer to without marshalling.

The language server may serve the same `RpcRef` multiple times and 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

Instances For

source
def Lean.Lsp.instInhabitedRpcRef.default :
RpcRef
Equations

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

Instances For

source
instance Lean.Lsp.instInhabitedRpcRef :
Inhabited RpcRef
Equations

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

source
instance Lean.Lsp.instBEqRpcRef :
BEq RpcRef
Equations

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

source
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

Instances For

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

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

Instances For

source
instance Lean.Lsp.instHashableRpcRef :
Hashable RpcRef
Equations

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

source
def Lean.Lsp.instFromJsonRpcRef.fromJson :
Json → Except String RpcRef
Equations

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

Instances For

source
instance Lean.Lsp.instFromJsonRpcRef :
FromJson RpcRef
Equations

- Lean.Lsp.instFromJsonRpcRef = { fromJson? := Lean.Lsp.instFromJsonRpcRef.fromJson }

source
def Lean.Lsp.instToJsonRpcRef.toJson :
RpcRef → Json
Equations

- Lean.Lsp.instToJsonRpcRef.toJson x✝ = Lean.Json.mkObj [[("p", Lean.toJson x✝.p)]].flatten

Instances For

source
instance Lean.Lsp.instToJsonRpcRef :
ToJson RpcRef
Equations

- Lean.Lsp.instToJsonRpcRef = { toJson := Lean.Lsp.instToJsonRpcRef.toJson }

source
instance Lean.Lsp.instToStringRpcRef :
ToString RpcRef
Equations

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

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

Marks values to be encoded as opaque references in RPC packets. Two `WithRpcRef`s with the same `id` will yield the same client-side reference.

See also the docstring for `RpcEncodable`.

- mk' :: (

- val : α
- id : USize

- )

Instances For

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

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

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

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

Instances For

source
opaque Lean.Server.freshWithRpcRefId :
IO.Ref USize
source
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 }

Instances For

source
structure Lean.Server.ReferencedObject :
Type

- obj : Dynamic
- id : USize
- rc : Nat

Instances For

source
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 `RpcRef`s for the same object. Reusing `RpcRef`s is helpful because it enables clients to reuse their UI state.

- nextRef : USize

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

source
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 a structure containing a value of type `α` and an associated `id`. 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. Two `WithRpcRef`s with the same `id` will yield the same client-side reference.

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

Instances

source
instance Lean.Server.instNonemptyRpcEncodable {α : Type} :
Nonempty (RpcEncodable α)
source
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) }

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

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

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

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

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

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

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

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

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

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

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

- Lean.Server.instRpcEncodableWithRpcRefOfTypeName.rpcEncode r = Lean.toJson <$> Lean.Server.rpcStoreRef r

Instances For

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

- Lean.Server.instRpcEncodableWithRpcRefOfTypeName.rpcDecode j = do let __do_lift ← liftM (Lean.fromJson? j) Lean.Server.rpcGetRef α __do_lift

Instances For