Lean.Server.Rpc.Basic

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

class Lean.Server.MonadRpcSession (m : Type → Type) :

Type

rpcStoreRef : Lean.Name → NonScalar → m Lean.Lsp.RpcRef
rpcGetRef : Lean.Lsp.RpcRef → m (Option (Lean.Name × NonScalar))
rpcReleaseRef : Lean.Lsp.RpcRef → m Bool

Monads with an RPC session in their state.

Instances

source

instance Lean.Server.instMonadRpcSession {m : Type → Type} {n : Type → Type} [inst : MonadLift m n] [inst : Lean.Server.MonadRpcSession m] :

Lean.Server.MonadRpcSession n

Equations

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

source

class Lean.Server.RpcEncoding (α : Type) (β : outParam Type) :

Type 1

rpcEncode : {m : Type → Type} → [inst : Monad m] → [inst : Lean.Server.MonadRpcSession m] → α → m β
rpcDecode : {m : Type → Type} → [inst : Monad m] → [inst : Lean.Server.MonadRpcSession m] → β → ExceptT String m α

RpcEncoding α β means that α may participate in RPC calls with its on-the-wire LSP encoding being β. This is useful when α contains fields which must be marshalled in a special way. In particular, we encode WithRpcRef fields as opaque references rather than send their content.

Structures with From/ToJson use JSON as their RpcEncoding. Structures containing non-JSON-serializable fields can be auto-encoded in two ways:

deriving RpcEncoding acts like From/ToJson but marshalls any WithRpcRef fields as Lsp.RpcRefs.
deriving RpcEncoding with { withRef := true } generates an encoding for WithRpcRef TheType.

Instances

source

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

Lean.Server.RpcEncoding α α

Equations

Lean.Server.instRpcEncoding = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] => pure, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] => pure }