Implementation of JSON-RPC 2.0 (https://www.jsonrpc.org/specification) for use in the LSP server.

inductive Lean.JsonRpc.RequestID : Type

In JSON-RPC, each request from the client editor to the language server comes with a request id so that the corresponding response can be identified or cancelled.

• str: String → Lean.JsonRpc.RequestID
• num: Lean.JsonNumber → Lean.JsonRpc.RequestID
• null: Lean.JsonRpc.RequestID

instance Lean.JsonRpc.instInhabitedRequestID : Inhabited Lean.JsonRpc.RequestID

Equations

• Lean.JsonRpc.instInhabitedRequestID = { default := Lean.JsonRpc.RequestID.str default }

instance Lean.JsonRpc.instBEqRequestID : BEq Lean.JsonRpc.RequestID

Equations

• Lean.JsonRpc.instBEqRequestID = { beq := Lean.JsonRpc.beqRequestID✝ }

instance Lean.JsonRpc.instOrdRequestID : Ord Lean.JsonRpc.RequestID

Equations

• Lean.JsonRpc.instOrdRequestID = { compare := Lean.JsonRpc.ordRequestID✝ }

instance Lean.JsonRpc.instOfNatRequestID {n : Nat} : OfNat Lean.JsonRpc.RequestID n

Equations

• Lean.JsonRpc.instOfNatRequestID = { ofNat := Lean.JsonRpc.RequestID.num (Lean.JsonNumber.fromNat n) }

instance Lean.JsonRpc.instToStringRequestID : ToString Lean.JsonRpc.RequestID

Equations

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

inductive Lean.JsonRpc.ErrorCode : Type

Error codes defined by JSON-RPC and LSP.

• parseError: Lean.JsonRpc.ErrorCode

  Invalid JSON was received by the server. An error occurred on the server while parsing the JSON text.

• invalidRequest: Lean.JsonRpc.ErrorCode

  The JSON sent is not a valid Request object.

• methodNotFound: Lean.JsonRpc.ErrorCode

  The method does not exist / is not available.

• invalidParams: Lean.JsonRpc.ErrorCode

  Invalid method parameter(s).

• internalError: Lean.JsonRpc.ErrorCode

  Internal JSON-RPC error.

• serverNotInitialized: Lean.JsonRpc.ErrorCode

  Error code indicating that a server received a notification or request before the server has received the initialize request.

• unknownErrorCode: Lean.JsonRpc.ErrorCode
• contentModified: Lean.JsonRpc.ErrorCode

  The server detected that the content of a document got modified outside normal conditions. A server should NOT send this error code if it detects a content change in it unprocessed messages. The result even computed on an older state might still be useful for the client.

  If a client decides that a result is not of any use anymore the client should cancel the request.

• requestCancelled: Lean.JsonRpc.ErrorCode

  The client has canceled a request and a server as detected the cancel.

• rpcNeedsReconnect: Lean.JsonRpc.ErrorCode
• workerExited: Lean.JsonRpc.ErrorCode
• workerCrashed: Lean.JsonRpc.ErrorCode

instance Lean.JsonRpc.instInhabitedErrorCode : Inhabited Lean.JsonRpc.ErrorCode

Equations

• Lean.JsonRpc.instInhabitedErrorCode = { default := Lean.JsonRpc.ErrorCode.parseError }

instance Lean.JsonRpc.instBEqErrorCode : BEq Lean.JsonRpc.ErrorCode

Equations

• Lean.JsonRpc.instBEqErrorCode = { beq := Lean.JsonRpc.beqErrorCode✝ }

instance Lean.JsonRpc.instFromJsonErrorCode : Lean.FromJson Lean.JsonRpc.ErrorCode

Equations

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

instance Lean.JsonRpc.instToJsonErrorCode : Lean.ToJson Lean.JsonRpc.ErrorCode

Equations

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

inductive Lean.JsonRpc.Message : Type

A JSON-RPC message.

Uses separate constructors for notifications and errors because client and server behavior is expected to be wildly different for both.

• request: Lean.JsonRpc.RequestID → String → Option Lean.Json.Structured → Lean.JsonRpc.Message

  A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request.

• notification: String → Option Lean.Json.Structured → Lean.JsonRpc.Message

  A notification message. A processed notification message must not send a response back. They work like events.

• response: Lean.JsonRpc.RequestID → Lean.Json → Lean.JsonRpc.Message

  A Response Message sent as a result of a request.

• responseError: Lean.JsonRpc.RequestID → Lean.JsonRpc.ErrorCode → String → Option Lean.Json → Lean.JsonRpc.Message

  A non-successful response.

def Lean.JsonRpc.Batch : Type

Equations

• Lean.JsonRpc.Batch = Array Lean.JsonRpc.Message

structure Lean.JsonRpc.Request (α : Type u) : Type u

Generic version of Message.request.

A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request.

• LSP
• JSON-RPC

• id : Lean.JsonRpc.RequestID
• method : String
• param : α

instance Lean.JsonRpc.instInhabitedRequest : {a : Type u_1} → [inst : Inhabited a] → Inhabited (Lean.JsonRpc.Request a)

Equations

• Lean.JsonRpc.instInhabitedRequest = { default := { id := default, method := default, param := default } }

instance Lean.JsonRpc.instBEqRequest : {α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.Request α)

Equations

• Lean.JsonRpc.instBEqRequest = { beq := Lean.JsonRpc.beqRequest✝ }

instance Lean.JsonRpc.instCoeOutRequestMessage {α : Type u_1} [Lean.ToJson α] : CoeOut (Lean.JsonRpc.Request α) Lean.JsonRpc.Message

Equations

• Lean.JsonRpc.instCoeOutRequestMessage = { coe := fun (r : Lean.JsonRpc.Request α) => Lean.JsonRpc.Message.request r.id r.method (Except.toOption (Lean.Json.toStructured? r.param)) }

structure Lean.JsonRpc.Notification (α : Type u) : Type u

Generic version of Message.notification.

A notification message. A processed notification message must not send a response back. They work like events.

• JSON-RPC
• LSP.

• method : String
• param : α

instance Lean.JsonRpc.instInhabitedNotification : {a : Type u_1} → [inst : Inhabited a] → Inhabited (Lean.JsonRpc.Notification a)

Equations

• Lean.JsonRpc.instInhabitedNotification = { default := { method := default, param := default } }

instance Lean.JsonRpc.instBEqNotification : {α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.Notification α)

Equations

• Lean.JsonRpc.instBEqNotification = { beq := Lean.JsonRpc.beqNotification✝ }

instance Lean.JsonRpc.instCoeOutNotificationMessage {α : Type u_1} [Lean.ToJson α] : CoeOut (Lean.JsonRpc.Notification α) Lean.JsonRpc.Message

Equations

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

structure Lean.JsonRpc.Response (α : Type u) : Type u

Generic version of Message.response.

A Response Message sent as a result of a request. If a request doesn’t provide a result value the receiver of a request still needs to return a response message to conform to the JSON-RPC specification. The result property of the ResponseMessage should be set to null in this case to signal a successful request.

References:

• JSON-RPC
• LSP

• id : Lean.JsonRpc.RequestID
• result : α

instance Lean.JsonRpc.instInhabitedResponse : {a : Type u_1} → [inst : Inhabited a] → Inhabited (Lean.JsonRpc.Response a)

Equations

• Lean.JsonRpc.instInhabitedResponse = { default := { id := default, result := default } }

instance Lean.JsonRpc.instBEqResponse : {α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.Response α)

Equations

• Lean.JsonRpc.instBEqResponse = { beq := Lean.JsonRpc.beqResponse✝ }

instance Lean.JsonRpc.instCoeOutResponseMessage {α : Type u_1} [Lean.ToJson α] : CoeOut (Lean.JsonRpc.Response α) Lean.JsonRpc.Message

Equations

• Lean.JsonRpc.instCoeOutResponseMessage = { coe := fun (r : Lean.JsonRpc.Response α) => Lean.JsonRpc.Message.response r.id (Lean.toJson r.result) }

structure Lean.JsonRpc.ResponseError (α : Type u) : Type u

Generic version of Message.responseError.

References:

• JSON-RPC
• LSP.

• id : Lean.JsonRpc.RequestID
• code : Lean.JsonRpc.ErrorCode
• message : String

  A string providing a short description of the error.

• data? : Option α

  A primitive or structured value that contains additional information about the error. Can be omitted.

instance Lean.JsonRpc.instInhabitedResponseError : {a : Type u_1} → Inhabited (Lean.JsonRpc.ResponseError a)

Equations

• Lean.JsonRpc.instInhabitedResponseError = { default := { id := default, code := default, message := default, data? := default } }

instance Lean.JsonRpc.instBEqResponseError : {α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.ResponseError α)

Equations

• Lean.JsonRpc.instBEqResponseError = { beq := Lean.JsonRpc.beqResponseError✝ }

instance Lean.JsonRpc.instCoeOutResponseErrorMessage {α : Type u_1} [Lean.ToJson α] : CoeOut (Lean.JsonRpc.ResponseError α) Lean.JsonRpc.Message

Equations

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

instance Lean.JsonRpc.instCoeStringRequestID : Coe String Lean.JsonRpc.RequestID

Equations

• Lean.JsonRpc.instCoeStringRequestID = { coe := Lean.JsonRpc.RequestID.str }

instance Lean.JsonRpc.instCoeJsonNumberRequestID : Coe Lean.JsonNumber Lean.JsonRpc.RequestID

Equations

• Lean.JsonRpc.instCoeJsonNumberRequestID = { coe := Lean.JsonRpc.RequestID.num }

instance Lean.JsonRpc.instLTRequestID : LT Lean.JsonRpc.RequestID

Equations

• Lean.JsonRpc.instLTRequestID = Lean.JsonRpc.RequestID.ltProp

instance Lean.JsonRpc.instDecidableLtRequestIDInstLTRequestID (a : Lean.JsonRpc.RequestID) (b : Lean.JsonRpc.RequestID) : Decidable (a < b)

Equations

• Lean.JsonRpc.instDecidableLtRequestIDInstLTRequestID a b = inferInstanceAs (Decidable (Lean.JsonRpc.RequestID.lt a b = true))

instance Lean.JsonRpc.instFromJsonRequestID : Lean.FromJson Lean.JsonRpc.RequestID

Equations

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

instance Lean.JsonRpc.instToJsonRequestID : Lean.ToJson Lean.JsonRpc.RequestID

Equations

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

instance Lean.JsonRpc.instToJsonMessage : Lean.ToJson Lean.JsonRpc.Message

Equations

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

instance Lean.JsonRpc.instFromJsonMessage : Lean.FromJson Lean.JsonRpc.Message

Equations

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

instance Lean.JsonRpc.instFromJsonNotification {α : Type} [Lean.FromJson α] : Lean.FromJson (Lean.JsonRpc.Notification α)

Equations

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

def IO.FS.Stream.readMessage (h : IO.FS.Stream) (nBytes : Nat) : IO Lean.JsonRpc.Message

Equations

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

def IO.FS.Stream.readRequestAs (h : IO.FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [Lean.FromJson α] : IO (Lean.JsonRpc.Request α)

Equations

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

def IO.FS.Stream.readNotificationAs (h : IO.FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [Lean.FromJson α] : IO (Lean.JsonRpc.Notification α)

Equations

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

def IO.FS.Stream.readResponseAs (h : IO.FS.Stream) (nBytes : Nat) (expectedID : Lean.JsonRpc.RequestID) (α : Type) [Lean.FromJson α] : IO (Lean.JsonRpc.Response α)

Equations

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

def IO.FS.Stream.writeMessage (h : IO.FS.Stream) (m : Lean.JsonRpc.Message) : IO Unit

Equations

• IO.FS.Stream.writeMessage h m = IO.FS.Stream.writeJson h (Lean.toJson m)

def IO.FS.Stream.writeRequest {α : Type u_1} [Lean.ToJson α] (h : IO.FS.Stream) (r : Lean.JsonRpc.Request α) : IO Unit

Equations

• IO.FS.Stream.writeRequest h r = IO.FS.Stream.writeMessage h (Lean.JsonRpc.Message.request r.id r.method (Except.toOption (Lean.Json.toStructured? r.param)))

def IO.FS.Stream.writeNotification {α : Type u_1} [Lean.ToJson α] (h : IO.FS.Stream) (n : Lean.JsonRpc.Notification α) : IO Unit

Equations

• IO.FS.Stream.writeNotification h n = IO.FS.Stream.writeMessage h (Lean.JsonRpc.Message.notification n.method (Except.toOption (Lean.Json.toStructured? n.param)))

def IO.FS.Stream.writeResponse {α : Type u_1} [Lean.ToJson α] (h : IO.FS.Stream) (r : Lean.JsonRpc.Response α) : IO Unit

Equations

• IO.FS.Stream.writeResponse h r = IO.FS.Stream.writeMessage h (Lean.JsonRpc.Message.response r.id (Lean.toJson r.result))

def IO.FS.Stream.writeResponseError (h : IO.FS.Stream) (e : Lean.JsonRpc.ResponseError Unit) : IO Unit

Equations

• IO.FS.Stream.writeResponseError h e = IO.FS.Stream.writeMessage h (Lean.JsonRpc.Message.responseError e.id e.code e.message none)

def IO.FS.Stream.writeResponseErrorWithData {α : Type u_1} [Lean.ToJson α] (h : IO.FS.Stream) (e : Lean.JsonRpc.ResponseError α) : IO Unit

Equations

• IO.FS.Stream.writeResponseErrorWithData h e = IO.FS.Stream.writeMessage h (Lean.JsonRpc.Message.responseError e.id e.code e.message (Option.map Lean.toJson e.data?))