fix: lengthen RPC reference field name

[Vtec234]

Attempt to address #712 the easy way: just make the magic identifier longer. The name __rpcref is more "internal-looking" than p. Of course a user could still type it in, we are just hoping they wouldn't. At 8 bytes vs. 1 byte, this incurs a ~5% size increase on the JSON size of interactive terms, e.g. from 868KiB to 903KiB on the #500 test. Server change is here.

The implementation is not as simple as I would've hoped, mostly due to having to gate which name we use behind a check of the Lean server version; so the alternative, "really fix it" design may be worth considering.

Alternative design

• Add a method $/lean/rpc/metadata which, given the name of an RPC method foo, returns a structure containing a description of where the RPC refs in any response to foo would be.
• To implement $/lean/rpc/metadata 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 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, seemingly cannot describe non-uniform paths (e.g. both the as in {a: 1, {b: {a: 2}}}).
    • The most expressive option is jq, but the most popular way to run it is via an Emscripten WASM blob in jq-web which seems heavy. There is jqjs as well; I'm not sure how production-ready that is.
    • JMESPath seems to provide all that is needed, and has 'fully compliant' implementations in many languages, but has unintuitive behavior with 'falsy' values.