47b3be0524
This PR adjusts the JSON encoding of RPC references from `{"p": "n"}` to
`{"__rpcref": "n"}`. Existing clients will continue to work unchanged,
but should eventually move to the new format by advertising the
`rpcWireFormat` client capability.
- This came up in leanprover/vscode-lean4#712.
- The new encoding is far less likely to clash with real-world names,
and is now documented as a "reserved internal name".
- At 8 bytes vs. 1 byte, it incurs a ~5% size increase on the JSON size
of interactive terms, e.g. from 868KiB to 903KiB on the
leanprover/vscode-lean4#500 test.
- Make `deriving RpcEncodable` throw an error when it encounters the
reserved name. We cannot easily guard against clashes in user-provided
JSON, however, so we just assume it does not clash.
- Add a notion of *RPC wire format* with corresponding `rpcWireFormat`
client and server capabilities. The format before this PR is now called
`v0`, whereas here we implement `v1`. Existing clients should eventually
implement compatibility with `v1` (because doing so fixes the above
bug), but will continue to work in the meantime. The format may be
revised again in the future (but we don't expect to revise it so often
that semver would be useful).
- Document everything.
## Alternative designs (abandoned for now)
- Option 1. Add a method `$/lean/rpc/metadata` which, given the name of
an RPC method `foo`, returns metadata containing a description of where
the RPC refs in any return value of `foo` would be (essentially a
description of the structure of the return type).
- Option 2. Wrap every response to `$/lean/rpc/call` in such metadata.
This would be a different change to the wire format.
- To implement this in an extensible way, we extend `RpcEncodable` by a
`refPaths` field. But how does `refPaths` describe where the refs are?
- Option A. Emit the code of a JS method that extracts the refs. This is
maybe simplest, but it would leave non-JS clients (e.g. `lean.nvim`)
behind.
- Option B. Give the description in some query language. The query
language must be able to describe paths into arbitrary inductive types.
- The most popular option,
[JSONPath](https://www.rfc-editor.org/rfc/rfc9535), seemingly cannot
describe non-uniform paths (e.g. both the `a`s in `{a: 1, {b: {a:
2}}}`).
- [JMESPath](https://jmespath.org/) can describe non-uniform paths, and
has 'fully compliant' implementations in many languages, but doesn't
seem to handle recursive paths.
- The most expressive option is [jq](https://github.com/jqlang/jq), but
the most popular way to run it is via an Emscripten WASM blob in
[jq-web](https://github.com/fiatjaf/jq-web) which seems heavy. There is
[jqjs](https://github.com/mwh/jqjs) as well; I'm not sure how
production-ready that is.
112 lines
2.8 KiB
Text
112 lines
2.8 KiB
Text
import Lean.Server.Rpc.Basic
|
||
|
||
open Lean Server
|
||
|
||
abbrev M := StateM RpcObjectStore
|
||
|
||
def M.run (x : ExceptT String M α) : Except String α :=
|
||
x.run' {}
|
||
|
||
def test (α : Type) [RpcEncodable α] (a : α) := M.run do
|
||
let json ← rpcEncode a
|
||
let _a : α ← ofExcept (rpcDecode json (← get))
|
||
return json
|
||
|
||
structure FooRef where
|
||
a : Array Nat
|
||
deriving Inhabited, TypeName
|
||
|
||
#eval do return test (WithRpcRef FooRef) (← WithRpcRef.mk default)
|
||
|
||
structure FooJson where
|
||
s : String
|
||
deriving FromJson, ToJson, Inhabited
|
||
|
||
structure Bar where
|
||
fooRef : WithRpcRef FooRef
|
||
fooJson : FooJson
|
||
deriving RpcEncodable, Inhabited
|
||
|
||
def Bar.mkDefault : BaseIO Bar := do return {
|
||
fooRef := ← WithRpcRef.mk default
|
||
fooJson := default
|
||
}
|
||
|
||
#eval do return test Bar (← Bar.mkDefault)
|
||
|
||
structure BarTrans where
|
||
bar : Bar
|
||
deriving RpcEncodable, Inhabited
|
||
|
||
#eval do return test BarTrans { bar := ← Bar.mkDefault }
|
||
|
||
structure Baz where
|
||
arr : Array String -- non-constant field
|
||
deriving RpcEncodable, Inhabited
|
||
|
||
#eval test Baz default
|
||
|
||
structure FooGeneric (α : Type) where
|
||
a : α
|
||
b? : Option α
|
||
deriving RpcEncodable, Inhabited
|
||
|
||
#eval test (FooGeneric Nat) default
|
||
#eval test (FooGeneric Nat) { a := 3, b? := some 42 }
|
||
|
||
inductive BazInductive
|
||
| baz (arr : Array Bar)
|
||
deriving RpcEncodable, Inhabited
|
||
|
||
#eval do return test BazInductive ⟨#[← Bar.mkDefault, ← Bar.mkDefault]⟩
|
||
|
||
inductive FooInductive (α : Type) where
|
||
| a : α → WithRpcRef FooRef → FooInductive α
|
||
| b : (n : Nat) → (a : α) → (m : Nat) → FooInductive α
|
||
deriving RpcEncodable, Inhabited
|
||
|
||
#eval do return test (FooInductive BazInductive) (.a default (← WithRpcRef.mk default))
|
||
#eval do return test (FooInductive BazInductive) (.b 42 default default)
|
||
|
||
inductive FooNested (α : Type) where
|
||
| a : α → Array (FooNested α) → FooNested α
|
||
deriving RpcEncodable, Inhabited
|
||
|
||
#eval test (FooNested BazInductive) (.a default #[default])
|
||
|
||
inductive FooParam (n : Nat) where
|
||
| a : Nat → FooParam n
|
||
deriving RpcEncodable, Inhabited
|
||
|
||
#eval test (FooParam 10) (.a 42)
|
||
|
||
inductive Unused (α : Type) | a
|
||
deriving RpcEncodable, Inhabited
|
||
|
||
structure NoRpcEncodable
|
||
#eval test (Unused NoRpcEncodable) default
|
||
|
||
structure UnusedStruct (α : Type)
|
||
deriving RpcEncodable, Inhabited
|
||
|
||
#eval test (UnusedStruct NoRpcEncodable) default
|
||
|
||
deriving instance Repr, RpcEncodable for Empty
|
||
#eval rpcDecode (α := Empty) .null {}
|
||
|
||
/--
|
||
error: '__rpcref' is reserved and cannot be used as a field name. See the `RpcEncodable` docstring.
|
||
-/
|
||
#guard_msgs in
|
||
structure ReservedFieldName where
|
||
__rpcref : Nat
|
||
deriving RpcEncodable
|
||
|
||
/--
|
||
error: '__rpcref' is reserved and cannot be used as an argument name. See the `RpcEncodable` docstring.
|
||
-/
|
||
#guard_msgs in
|
||
inductive ReservedCtorArgName where
|
||
| mk : ReservedCtorArgName
|
||
| mk2 (__rpcref : Nat) : Nat → ReservedCtorArgName
|
||
deriving RpcEncodable
|