sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

feat: update RPC wire format (#12905)

Browse Source 
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.
This commit is contained in:
Wojciech Nawrocki
2026-03-13 19:46:16 -04:00
committed by GitHub
parent de2b177423
commit 47b3be0524
18 changed files with 425 additions and 250 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
src/Lean/Data/Lsp/Capabilities.lean
View File

@@ -69,6 +69,11 @@ structure LeanClientCapabilities where
If `none` or `false`, silent diagnostics will not be served to the client.
-/
silentDiagnosticSupport? : Option Bool := none
/--
The latest RPC wire format supported by the client.
Defaults to `v0` when `none`.
-/
rpcWireFormat? : Option RpcWireFormat := none
deriving ToJson, FromJson
structure ClientCapabilities where
@@ -86,6 +91,13 @@ def ClientCapabilities.silentDiagnosticSupport (c : ClientCapabilities) : Bool :
| return false
return silentDiagnosticSupport
def ClientCapabilities.rpcWireFormat (c : ClientCapabilities) : RpcWireFormat := Id.run do
let some lean := c.lean?
| return .v0
let some v := lean.rpcWireFormat?
| return .v0
return v
structure LeanServerCapabilities where
moduleHierarchyProvider? : Option ModuleHierarchyOptions
rpcProvider? : Option RpcOptions

23
src/Lean/Data/Lsp/Extra.lean
View File

@@ -132,6 +132,11 @@ structure HighlightMatchesOptions where
structure RpcOptions where
highlightMatchesProvider? : Option HighlightMatchesOptions := none
/--
The latest RPC wire format supported by the server.
Defaults to `v0` when `none`.
-/
rpcWireFormat? : Option RpcWireFormat := none
deriving FromJson, ToJson
structure LeanModule where
@@ -208,11 +213,18 @@ structure RpcConnected where
/-- `$/lean/rpc/call` client->server request.
A request to execute a procedure bound for RPC. If an incorrect session ID is present, the server
errors with `RpcNeedsReconnect`.
A request to execute a procedure bound for RPC.
If an incorrect session ID is present, the server errors with `RpcNeedsReconnect`.
Extending TDPP is weird. But in Lean, symbols exist in the context of a position within a source
file. So we need this to refer to code in the environment at that position. -/
Extends `TextDocumentPositionParams` because in Lean,
symbols exist in the context of a position within a source file
(e.g., `foo` is defined below but not above `def foo`).
We use the position to resolve the set of defined constants,
registered RPC methods, etc.
Both the request and the response may contain `RpcEncodable` data.
It is serialized following the `RpcWireFormat`.
-/
structure RpcCallParams extends TextDocumentPositionParams where
sessionId : UInt64
/-- Procedure to invoke. Must be fully qualified. -/
@@ -227,7 +239,8 @@ A notification to release remote references. Should be sent by the client when i
structure RpcReleaseParams where
uri : DocumentUri
sessionId : UInt64
refs : Array RpcRef
/-- Array of RPC references to release. -/
refs : Array Json
deriving FromJson, ToJson
/-- `$/lean/rpc/keepAlive` client->server notification.

19
src/Lean/Server/FileWorker.lean
View File

@@ -654,15 +654,17 @@ section NotificationHandling
def handleRpcRelease (p : Lsp.RpcReleaseParams) : WorkerM Unit := do
-- NOTE(WN): when the worker restarts e.g. due to changed imports, we may receive `rpc/release`
-- for the previous RPC session. This is fine, just ignore.
let ctx ← read
if let some seshRef := (← get).rpcSessions.get? p.sessionId then
let monoMsNow ← IO.monoMsNow
let discardRefs : StateM RpcObjectStore Unit := do
for ref in p.refs do
discard do rpcReleaseRef ref
seshRef.modify fun st =>
let st := st.keptAlive monoMsNow
let ((), objects) := discardRefs.run st.objects
{ st with objects }
let wireFormat ← seshRef.modifyGet fun st =>
(st.objects.wireFormat, st.keptAlive monoMsNow)
for ref in p.refs do
let .ok p := ref.getObjVal? wireFormat.refFieldName >>= fromJson?
| ctx.hLog.putStrLn s!"malformed RPC ref (wire format {toJson wireFormat}): {ref.compress}"
seshRef.modify fun st =>
let (_, objects) := rpcReleaseRef ⟨p⟩ |>.run st.objects
{ st with objects }
def handleRpcKeepAlive (p : Lsp.RpcKeepAliveParams) : WorkerM Unit := do
match (← get).rpcSessions.get? p.sessionId with
@@ -676,7 +678,8 @@ end NotificationHandling
section RequestHandling
def handleRpcConnect (_ : RpcConnectParams) : WorkerM RpcConnected := do
let (newId, newSesh) ← RpcSession.new
let wireFormat := (← read).initParams.capabilities.rpcWireFormat
let (newId, newSesh) ← RpcSession.new wireFormat
let newSeshRef ← IO.mkRef newSesh
modify fun st => { st with rpcSessions := st.rpcSessions.insert newId newSeshRef }
return { sessionId := newId }

4
src/Lean/Server/FileWorker/Utils.lean
View File

@@ -83,12 +83,12 @@ namespace RpcSession
def keepAliveTimeMs : Nat :=
30000
def new : IO (UInt64 × RpcSession) := do
def new (wireFormat : Lsp.RpcWireFormat) : IO (UInt64 × RpcSession) := do
/- We generate a random ID to ensure that session IDs do not repeat across re-initializations
and worker restarts. Otherwise, the client may attempt to use outdated references. -/
let newId ← ByteArray.toUInt64LE! <$> IO.getRandomBytes 8
let newSesh := {
objects := {}
objects := { wireFormat }
expireTime := (← IO.monoMsNow) + keepAliveTimeMs
}
return (newId, newSesh)

91
src/Lean/Server/Rpc/Basic.lean
View File

@@ -24,28 +24,55 @@ first connect to the session using `$/lean/rpc/connect`. -/
namespace Lean.Lsp
/--
An object which RPC clients can refer to without marshalling.
The address of an object in an `RpcObjectStore` that clients can refer to.
Its JSON encoding depends on the RPC wire format.
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.
The language server may serve the same `RpcRef` multiple times.
It 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.
-/
structure RpcRef where
/- NOTE(WN): It is important for this to be a single-field structure
in order to deserialize as an `Object` on the JS side. -/
p : USize
deriving Inhabited, BEq, Hashable, FromJson, ToJson
deriving Inhabited, BEq, Hashable
instance : ToString RpcRef where
toString r := toString r.p
/-- The *RPC wire format* specifies how user data is encoded in RPC requests. -/
inductive RpcWireFormat where
/-- Version `0` uses JSON.
Serialized RPC data is stored directly in `RpcCallParams.params` and in `JsonRpc.Response.result`
(as opposed to being wrapped in additional metadata).
General types (except RPC references) are (de)serialized via `ToJson/FromJson`.
RPC references are serialized as `{"p": n}`. -/
| v0
/-- Version `1` is like `0`,
except that RPC references are serialized as `{"__rpcref": n}`. -/
| v1
deriving FromJson, ToJson
@[inline]
def RpcWireFormat.refFieldName : RpcWireFormat → String
| .v0 => "p"
| .v1 => "__rpcref"
end Lean.Lsp
namespace Lean.Server
/--
Marks values to be encoded as opaque references in RPC packets.
`WithRpcRef α` marks values that RPC clients should see as opaque references.
This includes heavy objects such as `Lean.Environment`s
and non-serializable objects such as closures.
In the Lean server, `WithRpcRef α` is a structure containing a value of type `α`
and an associated `id`.
In an RPC client (e.g. the infoview), it is an opaque reference.
Thus, `WithRpcRef α` is cheap to transmit, but its data may only be accessed server-side.
In practice, this is used by client code 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.
See also the docstring for `RpcEncodable`.
@@ -90,6 +117,8 @@ structure RpcObjectStore : Type where
Value to use for the next fresh `RpcRef`, monotonically increasing.
-/
nextRef : USize := 0
/-- The RPC wire format to follow. -/
wireFormat : Lsp.RpcWireFormat := .v1
def rpcStoreRef [TypeName α] (obj : WithRpcRef α) : StateM RpcObjectStore Lsp.RpcRef := do
let st ← get
@@ -137,29 +166,27 @@ def rpcReleaseRef (r : Lsp.RpcRef) : StateM RpcObjectStore Bool := do
return true
/--
`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).
`RpcEncodable α` means `α` can be used as an argument or return value
in Remote Procedure Call (RPC) methods.
Any type with `FromJson` and `ToJson` instances is `RpcEncodable`.
The following types are `RpcEncodable` by default:
- Any type with both `FromJson` and `ToJson` instances.
- Any type all of whose components
(meaning the fields of a `structure`, or the arguments to `inductive` constructors)
are `RpcEncodable`.
Use `deriving RpcEncodable` to construct an instance in this case.
- Certain common containers, if containing `RpcEncodable` data (see instances below).
- Any `WithRpcRef α` where `[TypeName α]`.
Furthermore, types that do not have these instances may still be `RpcEncodable`.
Use `deriving RpcEncodable` to automatically derive instances for such types.
Some names are reserved for internal use and must not appear
as the name of a field or constructor argument in any `RpcEncodable` type,
or as an object key in any nested JSON.
The following are currently reserved:
- `__rpcref`
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.
It is also possible (but discouraged for non-experts)
to implement custom `RpcEncodable` instances.
These must respect the `RpcObjectStore.wireFormat`.
-/
-- TODO(WN): for Lean.js, compile `WithRpcRef` to "opaque reference" on the client
class RpcEncodable (α : Type) where
@@ -200,7 +227,13 @@ instance [TypeName α] : RpcEncodable (WithRpcRef α) :=
{ rpcEncode, rpcDecode }
where
-- separate definitions to prevent inlining
rpcEncode r := toJson <$> rpcStoreRef r
rpcDecode j := do rpcGetRef α (← fromJson? j)
rpcEncode r := do
let ref ← rpcStoreRef r
let fieldName := (← get).wireFormat.refFieldName
return Json.mkObj [(fieldName, toJson ref.p)]
rpcDecode j := do
let fieldName := (← read).wireFormat.refFieldName
let p ← j.getObjValAs? USize fieldName
rpcGetRef α ⟨p⟩
end Lean.Server

6
src/Lean/Server/Rpc/Deriving.lean
View File

@@ -30,6 +30,9 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
let mut encInits := #[]
let mut decInits := #[]
for fieldName in fields do
if fieldName == `__rpcref then
throwError "'__rpcref' is reserved and cannot be used as a field name. \
See the `RpcEncodable` docstring."
let fid := mkIdent fieldName
fieldIds := fieldIds.push fid
if isOptField fieldName then
@@ -72,6 +75,9 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
-- create the constructor
let fieldStxs ← argVars.mapM fun arg => do
let name := (← getFVarLocalDecl arg).userName
if name == `__rpcref then
throwError "'__rpcref' is reserved and cannot be used as an argument name. \
See the `RpcEncodable` docstring."
`(bracketedBinderF| ($(mkIdent name) : Json))
let pktCtor ← `(Parser.Command.ctor|
| $ctorId:ident $[$fieldStxs]* : RpcEncodablePacket)

7
src/Lean/Server/Test/Runner.lean
View File

@@ -46,6 +46,12 @@ def normalizedRef (ref : RpcRef) : NormalizeM RpcRef := do
})
return ⟨ptr⟩
-- Test-only instances using the most recent version of the RPC wire format.
instance : ToJson RpcRef where
toJson r := Json.mkObj [("__rpcref", toJson r.p)]
instance : FromJson RpcRef where
fromJson? j := return ⟨← j.getObjValAs? USize "__rpcref"⟩
structure SubexprInfo where
info : RpcRef
subexprPos : String
@@ -713,6 +719,7 @@ partial def main (args : List String) : IO Unit := do
}
lean? := some {
silentDiagnosticSupport? := some true
rpcWireFormat? := some .v1
}
}
Ipc.writeRequest ⟨0, "initialize", { initializationOptions?, capabilities : InitializeParams }⟩

1
src/Lean/Server/Watchdog.lean
View File

@@ -1602,6 +1602,7 @@ def mkLeanServerCapabilities : ServerCapabilities := {
moduleHierarchyProvider? := some {}
rpcProvider? := some {
highlightMatchesProvider? := some {}
rpcWireFormat? := some .v1
}
}
}

17
tests/elab/derivingRpcEncoding.lean
View File

@@ -93,3 +93,20 @@ structure UnusedStruct (α : Type)
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

12
tests/elab/derivingRpcEncoding.lean.out.expected
View File

@@ -1,14 +1,14 @@
ok: {"p": "0"}
ok: {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}
ok: {"bar": {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}}
ok: {"__rpcref": "0"}
ok: {"fooRef": {"__rpcref": "0"}, "fooJson": {"s": ""}}
ok: {"bar": {"fooRef": {"__rpcref": "0"}, "fooJson": {"s": ""}}}
ok: {"arr": []}
ok: {"a": 0}
ok: {"b": 42, "a": 3}
ok: {"baz":
{"arr":
[{"fooRef": {"p": "0"}, "fooJson": {"s": ""}},
{"fooRef": {"p": "1"}, "fooJson": {"s": ""}}]}}
ok: {"a": [{"baz": {"arr": []}}, {"p": "0"}]}
[{"fooRef": {"__rpcref": "0"}, "fooJson": {"s": ""}},
{"fooRef": {"__rpcref": "1"}, "fooJson": {"s": ""}}]}}
ok: {"a": [{"baz": {"arr": []}}, {"__rpcref": "0"}]}
ok: {"b": {"n": 42, "m": 0, "a": {"baz": {"arr": []}}}}
ok: {"a": [{"baz": {"arr": []}}, [{"a": [{"baz": {"arr": []}}, []]}]]}
ok: {"a": 42}

172
tests/server_interactive/Diff.lean.out.expected
View File

@@ -3,284 +3,314 @@
{"goals":
[{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "1"}},
[{"subexprPos": "/", "info": {"__rpcref": "1"}},
{"append":
[{"tag":
[{"subexprPos": "/0", "info": {"p": "2"}},
[{"subexprPos": "/0", "info": {"__rpcref": "2"}},
{"append":
[{"tag":
[{"subexprPos": "/0/0/1", "info": {"p": "3"}}, {"text": "x"}]},
[{"subexprPos": "/0/0/1", "info": {"__rpcref": "3"}},
{"text": "x"}]},
{"text": " = "},
{"tag":
[{"subexprPos": "/0/1", "info": {"p": "4"}}, {"text": "x"}]}]}]},
[{"subexprPos": "/0/1", "info": {"__rpcref": "4"}},
{"text": "x"}]}]}]},
{"text": " → "},
{"tag":
[{"subexprPos": "/1", "info": {"p": "5"}}, {"text": "True"}]}]}]},
[{"subexprPos": "/1", "info": {"__rpcref": "5"}},
{"text": "True"}]}]}]},
"mvarId": "[anonymous]",
"isInserted": false,
"hyps":
[{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "Nat"}]},
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "Nat"}]},
"names": ["x"],
"isInserted": true,
"fvarIds": []}],
"goalPrefix": "⊢ ",
"ctx": {"p": "6"}}]}
"ctx": {"__rpcref": "6"}}]}
{"textDocument": {"uri": "file:///Diff.lean"},
"position": {"line": 4, "character": 2}}
{"goals":
[{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "1"}},
[{"subexprPos": "/", "info": {"__rpcref": "1"}},
{"append":
[{"tag":
[{"subexprPos": "/0", "info": {"p": "2"}, "diffStatus": "willDelete"},
[{"subexprPos": "/0",
"info": {"__rpcref": "2"},
"diffStatus": "willDelete"},
{"append":
[{"tag":
[{"subexprPos": "/0/0/1", "info": {"p": "3"}}, {"text": "x"}]},
[{"subexprPos": "/0/0/1", "info": {"__rpcref": "3"}},
{"text": "x"}]},
{"text": " = "},
{"tag":
[{"subexprPos": "/0/1", "info": {"p": "4"}}, {"text": "x"}]}]}]},
[{"subexprPos": "/0/1", "info": {"__rpcref": "4"}},
{"text": "x"}]}]}]},
{"text": " → "},
{"tag":
[{"subexprPos": "/1", "info": {"p": "5"}}, {"text": "True"}]}]}]},
[{"subexprPos": "/1", "info": {"__rpcref": "5"}},
{"text": "True"}]}]}]},
"mvarId": "[anonymous]",
"isInserted": false,
"hyps":
[{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "Nat"}]},
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "Nat"}]},
"names": ["x"],
"fvarIds": []}],
"goalPrefix": "⊢ ",
"ctx": {"p": "6"}}]}
"ctx": {"__rpcref": "6"}}]}
{"textDocument": {"uri": "file:///Diff.lean"},
"position": {"line": 9, "character": 2}}
{"goals":
[{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "0"}},
[{"subexprPos": "/", "info": {"__rpcref": "0"}},
{"append":
[{"text": "∀ ("},
{"tag": [{"subexprPos": "/", "info": {"p": "1"}}, {"text": "x"}]},
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "1"}}, {"text": "x"}]},
{"text": " : "},
{"tag":
[{"subexprPos": "/0", "info": {"p": "2"}, "diffStatus": "willDelete"},
[{"subexprPos": "/0",
"info": {"__rpcref": "2"},
"diffStatus": "willDelete"},
{"text": "Nat"}]},
{"text": "), "},
{"tag":
[{"subexprPos": "/1", "info": {"p": "3"}},
[{"subexprPos": "/1", "info": {"__rpcref": "3"}},
{"append":
[{"tag":
[{"subexprPos": "/1/0",
"info": {"p": "4"},
"info": {"__rpcref": "4"},
"diffStatus": "willDelete"},
{"append":
[{"tag":
[{"subexprPos": "/1/0/0/1", "info": {"p": "5"}},
[{"subexprPos": "/1/0/0/1", "info": {"__rpcref": "5"}},
{"text": "x"}]},
{"text": " = "},
{"tag":
[{"subexprPos": "/1/0/1", "info": {"p": "6"}},
[{"subexprPos": "/1/0/1", "info": {"__rpcref": "6"}},
{"text": "x"}]}]}]},
{"text": " → "},
{"tag":
[{"subexprPos": "/1/1", "info": {"p": "7"}},
[{"subexprPos": "/1/1", "info": {"__rpcref": "7"}},
{"text": "True"}]}]}]}]}]},
"mvarId": "[anonymous]",
"isInserted": false,
"hyps": [],
"goalPrefix": "⊢ ",
"ctx": {"p": "8"}}]}
"ctx": {"__rpcref": "8"}}]}
{"textDocument": {"uri": "file:///Diff.lean"},
"position": {"line": 15, "character": 5}}
{"goals":
[{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "11"}}, {"text": "True"}]},
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "11"}}, {"text": "True"}]},
"mvarId": "[anonymous]",
"isInserted": false,
"hyps":
[{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "Sort u_1"}]},
{"tag":
[{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "Sort u_1"}]},
"names": ["α"],
"isType": true,
"fvarIds": []},
{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "1"}}, {"text": "Nat"}]},
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "1"}}, {"text": "Nat"}]},
"names": ["x", "y"],
"fvarIds": []},
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "2"}},
[{"subexprPos": "/", "info": {"__rpcref": "2"}},
{"append":
[{"text": "∀ ("},
{"tag": [{"subexprPos": "/", "info": {"p": "3"}}, {"text": "a"}]},
{"tag":
[{"subexprPos": "/", "info": {"__rpcref": "3"}}, {"text": "a"}]},
{"text": " : "},
{"tag": [{"subexprPos": "/0", "info": {"p": "4"}}, {"text": "α"}]},
{"tag":
[{"subexprPos": "/0", "info": {"__rpcref": "4"}}, {"text": "α"}]},
{"text": "), "},
{"tag":
[{"subexprPos": "/1", "info": {"p": "5"}},
[{"subexprPos": "/1", "info": {"__rpcref": "5"}},
{"append":
[{"tag":
[{"subexprPos": "/1/0/1", "info": {"p": "6"}}, {"text": "x"}]},
[{"subexprPos": "/1/0/1", "info": {"__rpcref": "6"}},
{"text": "x"}]},
{"text": " = "},
{"tag":
[{"subexprPos": "/1/1",
"info": {"p": "7"},
"info": {"__rpcref": "7"},
"diffStatus": "willChange"},
{"text": "y"}]}]}]}]}]},
"names": ["f"],
"fvarIds": []},
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "8"}},
[{"subexprPos": "/", "info": {"__rpcref": "8"}},
{"append":
[{"tag": [{"subexprPos": "/0/1", "info": {"p": "9"}}, {"text": "y"}]},
[{"tag":
[{"subexprPos": "/0/1", "info": {"__rpcref": "9"}}, {"text": "y"}]},
{"text": " = "},
{"tag":
[{"subexprPos": "/1", "info": {"p": "10"}}, {"text": "x"}]}]}]},
[{"subexprPos": "/1", "info": {"__rpcref": "10"}},
{"text": "x"}]}]}]},
"names": ["h"],
"fvarIds": []}],
"goalPrefix": "⊢ ",
"ctx": {"p": "12"}}]}
"ctx": {"__rpcref": "12"}}]}
{"textDocument": {"uri": "file:///Diff.lean"},
"position": {"line": 20, "character": 9}}
{"goals":
[{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "11"}}, {"text": "True"}]},
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "11"}}, {"text": "True"}]},
"mvarId": "[anonymous]",
"isInserted": false,
"hyps":
[{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "Sort u_1"}]},
{"tag":
[{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "Sort u_1"}]},
"names": ["α"],
"isType": true,
"fvarIds": []},
{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "1"}}, {"text": "Nat"}]},
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "1"}}, {"text": "Nat"}]},
"names": ["x", "y"],
"fvarIds": []},
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "2"}},
[{"subexprPos": "/", "info": {"__rpcref": "2"}},
{"append":
[{"text": "∀ ("},
{"tag": [{"subexprPos": "/", "info": {"p": "3"}}, {"text": "a"}]},
{"tag":
[{"subexprPos": "/", "info": {"__rpcref": "3"}}, {"text": "a"}]},
{"text": " : "},
{"tag": [{"subexprPos": "/0", "info": {"p": "4"}}, {"text": "α"}]},
{"tag":
[{"subexprPos": "/0", "info": {"__rpcref": "4"}}, {"text": "α"}]},
{"text": "), "},
{"tag":
[{"subexprPos": "/1", "info": {"p": "5"}},
[{"subexprPos": "/1", "info": {"__rpcref": "5"}},
{"append":
[{"tag":
[{"subexprPos": "/1/0/1", "info": {"p": "6"}}, {"text": "x"}]},
[{"subexprPos": "/1/0/1", "info": {"__rpcref": "6"}},
{"text": "x"}]},
{"text": " = "},
{"tag":
[{"subexprPos": "/1/1",
"info": {"p": "7"},
"info": {"__rpcref": "7"},
"diffStatus": "wasChanged"},
{"text": "x"}]}]}]}]}]},
"names": ["f"],
"fvarIds": []},
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "8"}},
[{"subexprPos": "/", "info": {"__rpcref": "8"}},
{"append":
[{"tag": [{"subexprPos": "/0/1", "info": {"p": "9"}}, {"text": "y"}]},
[{"tag":
[{"subexprPos": "/0/1", "info": {"__rpcref": "9"}}, {"text": "y"}]},
{"text": " = "},
{"tag":
[{"subexprPos": "/1", "info": {"p": "10"}}, {"text": "x"}]}]}]},
[{"subexprPos": "/1", "info": {"__rpcref": "10"}},
{"text": "x"}]}]}]},
"names": ["h"],
"fvarIds": []}],
"goalPrefix": "⊢ ",
"ctx": {"p": "12"}}]}
"ctx": {"__rpcref": "12"}}]}
{"textDocument": {"uri": "file:///Diff.lean"},
"position": {"line": 25, "character": 2}}
{"goals":
[{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "0"}, "diffStatus": "willChange"},
[{"subexprPos": "/", "info": {"__rpcref": "0"}, "diffStatus": "willChange"},
{"append":
[{"tag": [{"subexprPos": "/0/1", "info": {"p": "1"}}, {"text": "True"}]},
[{"tag":
[{"subexprPos": "/0/1", "info": {"__rpcref": "1"}}, {"text": "True"}]},
{"text": " ∧ "},
{"tag":
[{"subexprPos": "/1", "info": {"p": "2"}}, {"text": "True"}]}]}]},
[{"subexprPos": "/1", "info": {"__rpcref": "2"}},
{"text": "True"}]}]}]},
"mvarId": "[anonymous]",
"isInserted": false,
"hyps": [],
"goalPrefix": "⊢ ",
"ctx": {"p": "3"}}]}
"ctx": {"__rpcref": "3"}}]}
{"textDocument": {"uri": "file:///Diff.lean"},
"position": {"line": 27, "character": 2}}
{"goals":
[{"userName": "left",
"type": {"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "True"}]},
"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "True"}]},
"mvarId": "[anonymous]",
"isRemoved": true,
"hyps": [],
"goalPrefix": "⊢ ",
"ctx": {"p": "1"}},
"ctx": {"__rpcref": "1"}},
{"userName": "right",
"type": {"tag": [{"subexprPos": "/", "info": {"p": "2"}}, {"text": "True"}]},
"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "2"}}, {"text": "True"}]},
"mvarId": "[anonymous]",
"hyps": [],
"goalPrefix": "⊢ ",
"ctx": {"p": "3"}}]}
"ctx": {"__rpcref": "3"}}]}
{"textDocument": {"uri": "file:///Diff.lean"},
"position": {"line": 29, "character": 2}}
{"goals":
[{"userName": "right",
"type": {"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "True"}]},
"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "True"}]},
"mvarId": "[anonymous]",
"isRemoved": true,
"hyps": [],
"goalPrefix": "⊢ ",
"ctx": {"p": "1"}}]}
"ctx": {"__rpcref": "1"}}]}
{"textDocument": {"uri": "file:///Diff.lean"},
"position": {"line": 33, "character": 6}}
{"goals":
[{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "4"}},
[{"subexprPos": "/", "info": {"__rpcref": "4"}},
{"append":
[{"tag":
[{"subexprPos": "/0/1", "info": {"p": "5"}},
[{"subexprPos": "/0/1", "info": {"__rpcref": "5"}},
{"append":
[{"tag":
[{"subexprPos": "/0/1/0/1",
"info": {"p": "6"},
"info": {"__rpcref": "6"},
"diffStatus": "willChange"},
{"text": "x"}]},
{"text": " + "},
{"tag":
[{"subexprPos": "/0/1/1",
"info": {"p": "7"},
"info": {"__rpcref": "7"},
"diffStatus": "willChange"},
{"text": "z"}]}]}]},
{"text": " = "},
{"tag":
[{"subexprPos": "/1", "info": {"p": "8"}},
[{"subexprPos": "/1", "info": {"__rpcref": "8"}},
{"append":
[{"tag":
[{"subexprPos": "/1/0/1", "info": {"p": "9"}}, {"text": "z"}]},
[{"subexprPos": "/1/0/1", "info": {"__rpcref": "9"}},
{"text": "z"}]},
{"text": " + "},
{"tag":
[{"subexprPos": "/1/1", "info": {"p": "10"}},
[{"subexprPos": "/1/1", "info": {"__rpcref": "10"}},
{"text": "y"}]}]}]}]}]},
"mvarId": "[anonymous]",
"isInserted": false,
"hyps":
[{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "Nat"}]},
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "Nat"}]},
"names": ["x", "y", "z"],
"fvarIds": []},
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "1"}},
[{"subexprPos": "/", "info": {"__rpcref": "1"}},
{"append":
[{"tag": [{"subexprPos": "/0/1", "info": {"p": "2"}}, {"text": "y"}]},
[{"tag":
[{"subexprPos": "/0/1", "info": {"__rpcref": "2"}}, {"text": "y"}]},
{"text": " = "},
{"tag": [{"subexprPos": "/1", "info": {"p": "3"}}, {"text": "x"}]}]}]},
{"tag":
[{"subexprPos": "/1", "info": {"__rpcref": "3"}}, {"text": "x"}]}]}]},
"names": ["h"],
"fvarIds": []}],
"goalPrefix": "⊢ ",
"ctx": {"p": "11"}}]}
"ctx": {"__rpcref": "11"}}]}

6
tests/server_interactive/highlightMatches.lean.out.expected
View File

@@ -22,7 +22,7 @@
"indent": 0,
"collapsed": true,
"cls": "Meta.debug",
"children": {"lazy": {"p": "0"}}}},
"children": {"lazy": {"__rpcref": "0"}}}},
{"text": ""}]}}
{"tag":
[{"trace":
@@ -103,7 +103,7 @@
"indent": 2,
"collapsed": true,
"cls": "Meta.debug",
"children": {"lazy": {"p": "1"}}}},
"children": {"lazy": {"__rpcref": "1"}}}},
{"text": ""}]},
{"tag":
[{"trace":
@@ -115,7 +115,7 @@
"indent": 2,
"collapsed": true,
"cls": "Meta.debug",
"children": {"lazy": {"p": "2"}}}},
"children": {"lazy": {"__rpcref": "2"}}}},
{"text": ""}]},
{"tag":
[{"trace":

5
tests/server_interactive/incrementalTactic.lean.out.expected
View File

@@ -62,11 +62,12 @@ s
{"textDocument": {"uri": "file:///incrementalTactic.lean"},
"position": {"line": 5, "character": 2}}
{"goals":
[{"type": {"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "True"}]},
[{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "True"}]},
"mvarId": "[anonymous]",
"hyps": [],
"goalPrefix": "⊢ ",
"ctx": {"p": "1"}}]}
"ctx": {"__rpcref": "1"}}]}
{"version": 1,
"uri": "file:///incrementalTactic.lean",
"diagnostics":

6
tests/server_interactive/interactiveDiagnostics.lean.out.expected
View File

@@ -40,7 +40,8 @@
[{"tag": [{"expr": {"text": "declaration uses `"}}, {"text": ""}]},
{"tag":
[{"expr":
{"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "sorry"}]}},
{"tag":
[{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "sorry"}]}},
{"text": ""}]},
{"tag": [{"expr": {"text": "`"}}, {"text": ""}]}]},
"fullRange":
@@ -85,7 +86,8 @@
[{"expr":
{"append":
[{"text": "Nat : "},
{"tag": [{"subexprPos": "/1", "info": {"p": "0"}}, {"text": "Type"}]}]}},
{"tag":
[{"subexprPos": "/1", "info": {"__rpcref": "0"}}, {"text": "Type"}]}]}},
{"text": ""}]},
"fullRange":
{"start": {"line": 6, "character": 0}, "end": {"line": 6, "character": 6}}}]

26
tests/server_interactive/interactiveGoalGoToLoc.lean.out.expected
View File

@@ -2,29 +2,33 @@
"position": {"line": 14, "character": 2}}
{"goals":
[{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "4"}}, {"text": "MyTrue"}]},
{"tag":
[{"subexprPos": "/", "info": {"__rpcref": "4"}}, {"text": "MyTrue"}]},
"mvarId": "[anonymous]",
"isRemoved": true,
"hyps":
[{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "MyNat"}]},
{"tag":
[{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "MyNat"}]},
"names": ["x"],
"fvarIds": []},
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "1"}},
[{"subexprPos": "/", "info": {"__rpcref": "1"}},
{"append":
[{"text": "MyEq "},
{"tag": [{"subexprPos": "/0/1", "info": {"p": "2"}}, {"text": "x"}]},
{"tag":
[{"subexprPos": "/0/1", "info": {"__rpcref": "2"}}, {"text": "x"}]},
{"text": " "},
{"tag": [{"subexprPos": "/1", "info": {"p": "3"}}, {"text": "x"}]}]}]},
{"tag":
[{"subexprPos": "/1", "info": {"__rpcref": "3"}}, {"text": "x"}]}]}]},
"names": ["h"],
"fvarIds": []}],
"goalPrefix": "⊢ ",
"ctx": {"p": "5"}}]}
"ctx": {"__rpcref": "5"}}]}
GoToLoc responses for type of x:
GoToLoc response for MyNat:
{"kind": "definition", "info": {"p": "0"}}
{"kind": "definition", "info": {"__rpcref": "0"}}
[{"targetUri": "file:///interactiveGoalGoToLoc.lean",
"targetSelectionRange":
{"start": {"line": 1, "character": 10}, "end": {"line": 1, "character": 15}},
@@ -32,21 +36,21 @@ GoToLoc response for MyNat:
{"start": {"line": 0, "character": 0}, "end": {"line": 3, "character": 24}}}]
GoToLoc responses for type of h:
GoToLoc response for MyEq x x:
{"kind": "definition", "info": {"p": "1"}}
{"kind": "definition", "info": {"__rpcref": "1"}}
[{"targetUri": "file:///interactiveGoalGoToLoc.lean",
"targetSelectionRange":
{"start": {"line": 9, "character": 10}, "end": {"line": 9, "character": 14}},
"targetRange":
{"start": {"line": 8, "character": 0}, "end": {"line": 10, "character": 27}}}]
GoToLoc response for x:
{"kind": "definition", "info": {"p": "2"}}
{"kind": "definition", "info": {"__rpcref": "2"}}
[]
GoToLoc response for x:
{"kind": "definition", "info": {"p": "3"}}
{"kind": "definition", "info": {"__rpcref": "3"}}
[]
GoToLoc responses for type of goal:
GoToLoc response for MyTrue:
{"kind": "definition", "info": {"p": "4"}}
{"kind": "definition", "info": {"__rpcref": "4"}}
[{"targetUri": "file:///interactiveGoalGoToLoc.lean",
"targetSelectionRange":
{"start": {"line": 6, "character": 10}, "end": {"line": 6, "character": 16}},

51
tests/server_interactive/interactiveGoalPopups.lean.out.expected
View File

@@ -2,60 +2,71 @@
"position": {"line": 14, "character": 2}}
{"goals":
[{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "4"}}, {"text": "MyTrue"}]},
{"tag":
[{"subexprPos": "/", "info": {"__rpcref": "4"}}, {"text": "MyTrue"}]},
"mvarId": "[anonymous]",
"isRemoved": true,
"hyps":
[{"type":
{"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "MyNat"}]},
{"tag":
[{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "MyNat"}]},
"names": ["x"],
"fvarIds": []},
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "1"}},
[{"subexprPos": "/", "info": {"__rpcref": "1"}},
{"append":
[{"text": "MyEq "},
{"tag": [{"subexprPos": "/0/1", "info": {"p": "2"}}, {"text": "x"}]},
{"tag":
[{"subexprPos": "/0/1", "info": {"__rpcref": "2"}}, {"text": "x"}]},
{"text": " "},
{"tag": [{"subexprPos": "/1", "info": {"p": "3"}}, {"text": "x"}]}]}]},
{"tag":
[{"subexprPos": "/1", "info": {"__rpcref": "3"}}, {"text": "x"}]}]}]},
"names": ["h"],
"fvarIds": []}],
"goalPrefix": "⊢ ",
"ctx": {"p": "5"}}]}
"ctx": {"__rpcref": "5"}}]}
Popups for type of x:
Popup for MyNat:
{"p": "0"}
{"type": {"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "Type"}]},
{"__rpcref": "0"}
{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "Type"}]},
"exprExplicit": {"text": "MyNat"},
"doc": "MyNat doc "}
Popups for type of h:
Popup for MyEq x x:
{"p": "1"}
{"type": {"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "Prop"}]},
{"__rpcref": "1"}
{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "Prop"}]},
"exprExplicit":
{"append":
[{"text": "@"},
{"tag": [{"subexprPos": "/0/0/0", "info": {"p": "1"}}, {"text": "MyEq"}]},
{"tag":
[{"subexprPos": "/0/0/0", "info": {"__rpcref": "1"}}, {"text": "MyEq"}]},
{"text": " "},
{"tag": [{"subexprPos": "/0/0/1", "info": {"p": "2"}}, {"text": "MyNat"}]},
{"tag":
[{"subexprPos": "/0/0/1", "info": {"__rpcref": "2"}}, {"text": "MyNat"}]},
{"text": " "},
{"tag": [{"subexprPos": "/0/1", "info": {"p": "3"}}, {"text": "x"}]},
{"tag": [{"subexprPos": "/0/1", "info": {"__rpcref": "3"}}, {"text": "x"}]},
{"text": " "},
{"tag": [{"subexprPos": "/1", "info": {"p": "4"}}, {"text": "x"}]}]},
{"tag": [{"subexprPos": "/1", "info": {"__rpcref": "4"}}, {"text": "x"}]}]},
"doc": null}
Popup for x:
{"p": "2"}
{"type": {"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "MyNat"}]},
{"__rpcref": "2"}
{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "MyNat"}]},
"exprExplicit": {"text": "x"},
"doc": null}
Popup for x:
{"p": "3"}
{"type": {"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "MyNat"}]},
{"__rpcref": "3"}
{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "MyNat"}]},
"exprExplicit": {"text": "x"},
"doc": null}
Popups for type of goal:
Popup for MyTrue:
{"p": "4"}
{"type": {"tag": [{"subexprPos": "/", "info": {"p": "0"}}, {"text": "Prop"}]},
{"__rpcref": "4"}
{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "Prop"}]},
"exprExplicit": {"text": "MyTrue"},
"doc": "MyTrue doc "}

215
tests/server_interactive/interactiveTermGoals.lean.out.expected
View File

@@ -2,263 +2,298 @@
"position": {"line": 2, "character": 14}}
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "1"}},
[{"subexprPos": "/", "info": {"__rpcref": "1"}},
{"append":
[{"tag": [{"subexprPos": "/0/1", "info": {"p": "2"}}, {"text": "0"}]},
[{"tag":
[{"subexprPos": "/0/1", "info": {"__rpcref": "2"}}, {"text": "0"}]},
{"text": " < "},
{"tag": [{"subexprPos": "/1", "info": {"p": "3"}}, {"text": "2"}]}]}]},
"term": {"p": "0"},
{"tag":
[{"subexprPos": "/1", "info": {"__rpcref": "3"}}, {"text": "2"}]}]}]},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 2, "character": 2}, "end": {"line": 2, "character": 51}},
"hyps": [],
"ctx": {"p": "4"}}
"ctx": {"__rpcref": "4"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 2, "character": 15}}
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "1"}},
[{"subexprPos": "/", "info": {"__rpcref": "1"}},
{"append":
[{"tag": [{"subexprPos": "/0/1", "info": {"p": "2"}}, {"text": "0"}]},
[{"tag":
[{"subexprPos": "/0/1", "info": {"__rpcref": "2"}}, {"text": "0"}]},
{"text": " < "},
{"tag": [{"subexprPos": "/1", "info": {"p": "3"}}, {"text": "1"}]}]}]},
"term": {"p": "0"},
{"tag":
[{"subexprPos": "/1", "info": {"__rpcref": "3"}}, {"text": "1"}]}]}]},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 2, "character": 15}, "end": {"line": 2, "character": 30}},
"hyps": [],
"ctx": {"p": "4"}}
"ctx": {"__rpcref": "4"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 2, "character": 16}}
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "1"}},
[{"subexprPos": "/", "info": {"__rpcref": "1"}},
{"append":
[{"tag": [{"subexprPos": "/0/1", "info": {"p": "2"}}, {"text": "0"}]},
[{"tag":
[{"subexprPos": "/0/1", "info": {"__rpcref": "2"}}, {"text": "0"}]},
{"text": " < "},
{"tag": [{"subexprPos": "/1", "info": {"p": "3"}}, {"text": "1"}]}]}]},
"term": {"p": "0"},
{"tag":
[{"subexprPos": "/1", "info": {"__rpcref": "3"}}, {"text": "1"}]}]}]},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 2, "character": 15}, "end": {"line": 2, "character": 30}},
"hyps": [],
"ctx": {"p": "4"}}
"ctx": {"__rpcref": "4"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 2, "character": 31}}
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "1"}},
[{"subexprPos": "/", "info": {"__rpcref": "1"}},
{"append":
[{"tag": [{"subexprPos": "/0/1", "info": {"p": "2"}}, {"text": "1"}]},
[{"tag":
[{"subexprPos": "/0/1", "info": {"__rpcref": "2"}}, {"text": "1"}]},
{"text": " < "},
{"tag": [{"subexprPos": "/1", "info": {"p": "3"}}, {"text": "2"}]}]}]},
"term": {"p": "0"},
{"tag":
[{"subexprPos": "/1", "info": {"__rpcref": "3"}}, {"text": "2"}]}]}]},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 2, "character": 31}, "end": {"line": 2, "character": 51}},
"hyps": [],
"ctx": {"p": "4"}}
"ctx": {"__rpcref": "4"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 2, "character": 48}}
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "1"}},
[{"subexprPos": "/", "info": {"__rpcref": "1"}},
{"append":
[{"tag": [{"subexprPos": "/0/1", "info": {"p": "2"}}, {"text": "1"}]},
[{"tag":
[{"subexprPos": "/0/1", "info": {"__rpcref": "2"}}, {"text": "1"}]},
{"text": " < "},
{"tag": [{"subexprPos": "/1", "info": {"p": "3"}}, {"text": "2"}]}]}]},
"term": {"p": "0"},
{"tag":
[{"subexprPos": "/1", "info": {"__rpcref": "3"}}, {"text": "2"}]}]}]},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 2, "character": 32}, "end": {"line": 2, "character": 50}},
"hyps": [],
"ctx": {"p": "4"}}
"ctx": {"__rpcref": "4"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 11, "character": 10}}
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "2"}},
[{"subexprPos": "/", "info": {"__rpcref": "2"}},
{"append":
[{"text": "Option "},
{"tag": [{"subexprPos": "/1", "info": {"p": "3"}}, {"text": "Unit"}]}]}]},
"term": {"p": "0"},
{"tag":
[{"subexprPos": "/1", "info": {"__rpcref": "3"}}, {"text": "Unit"}]}]}]},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 11, "character": 2}, "end": {"line": 11, "character": 19}},
"hyps":
[{"type": {"tag": [{"subexprPos": "/", "info": {"p": "1"}}, {"text": "Int"}]},
[{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "1"}}, {"text": "Int"}]},
"names": ["y"],
"fvarIds": []}],
"ctx": {"p": "4"}}
"ctx": {"__rpcref": "4"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 16, "character": 17}}
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "2"}},
[{"subexprPos": "/", "info": {"__rpcref": "2"}},
{"append":
[{"tag":
[{"subexprPos": "/0/1", "info": {"p": "3"}},
[{"subexprPos": "/0/1", "info": {"__rpcref": "3"}},
{"append":
[{"tag":
[{"subexprPos": "/0/1/0/0", "info": {"p": "4"}}, {"text": "?m"}]},
[{"subexprPos": "/0/1/0/0", "info": {"__rpcref": "4"}},
{"text": "?m"}]},
{"text": " "},
{"tag":
[{"subexprPos": "/0/1/0/1", "info": {"p": "5"}}, {"text": "m"}]},
[{"subexprPos": "/0/1/0/1", "info": {"__rpcref": "5"}},
{"text": "m"}]},
{"text": " "},
{"tag":
[{"subexprPos": "/0/1/1", "info": {"p": "6"}}, {"text": "n"}]}]}]},
[{"subexprPos": "/0/1/1", "info": {"__rpcref": "6"}},
{"text": "n"}]}]}]},
{"text": " < "},
{"tag": [{"subexprPos": "/1", "info": {"p": "7"}}, {"text": "n"}]}]}]},
"term": {"p": "0"},
{"tag":
[{"subexprPos": "/1", "info": {"__rpcref": "7"}}, {"text": "n"}]}]}]},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 16, "character": 17}, "end": {"line": 16, "character": 18}},
"hyps":
[{"type": {"tag": [{"subexprPos": "/", "info": {"p": "1"}}, {"text": "Nat"}]},
[{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "1"}}, {"text": "Nat"}]},
"names": ["m", "n"],
"fvarIds": []}],
"ctx": {"p": "8"}}
"ctx": {"__rpcref": "8"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 16, "character": 18}}
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "2"}},
[{"subexprPos": "/", "info": {"__rpcref": "2"}},
{"append":
[{"tag":
[{"subexprPos": "/0/1", "info": {"p": "3"}},
[{"subexprPos": "/0/1", "info": {"__rpcref": "3"}},
{"append":
[{"tag":
[{"subexprPos": "/0/1/0/0", "info": {"p": "4"}}, {"text": "?m"}]},
[{"subexprPos": "/0/1/0/0", "info": {"__rpcref": "4"}},
{"text": "?m"}]},
{"text": " "},
{"tag":
[{"subexprPos": "/0/1/0/1", "info": {"p": "5"}}, {"text": "m"}]},
[{"subexprPos": "/0/1/0/1", "info": {"__rpcref": "5"}},
{"text": "m"}]},
{"text": " "},
{"tag":
[{"subexprPos": "/0/1/1", "info": {"p": "6"}}, {"text": "n"}]}]}]},
[{"subexprPos": "/0/1/1", "info": {"__rpcref": "6"}},
{"text": "n"}]}]}]},
{"text": " < "},
{"tag": [{"subexprPos": "/1", "info": {"p": "7"}}, {"text": "n"}]}]}]},
"term": {"p": "0"},
{"tag":
[{"subexprPos": "/1", "info": {"__rpcref": "7"}}, {"text": "n"}]}]}]},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 16, "character": 17}, "end": {"line": 16, "character": 18}},
"hyps":
[{"type": {"tag": [{"subexprPos": "/", "info": {"p": "1"}}, {"text": "Nat"}]},
[{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "1"}}, {"text": "Nat"}]},
"names": ["m", "n"],
"fvarIds": []}],
"ctx": {"p": "8"}}
"ctx": {"__rpcref": "8"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 20, "character": 18}}
{"type": {"tag": [{"subexprPos": "/", "info": {"p": "1"}}, {"text": "True"}]},
"term": {"p": "0"},
{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "1"}}, {"text": "True"}]},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 20, "character": 18}, "end": {"line": 20, "character": 23}},
"hyps": [],
"ctx": {"p": "2"}}
"ctx": {"__rpcref": "2"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 24, "character": 2}}
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "1"}},
[{"subexprPos": "/", "info": {"__rpcref": "1"}},
{"append":
[{"text": "∀ ("},
{"tag": [{"subexprPos": "/", "info": {"p": "2"}}, {"text": "n"}]},
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "2"}}, {"text": "n"}]},
{"text": " : "},
{"tag": [{"subexprPos": "/0", "info": {"p": "3"}}, {"text": "Nat"}]},
{"tag":
[{"subexprPos": "/0", "info": {"__rpcref": "3"}}, {"text": "Nat"}]},
{"text": "), "},
{"tag":
[{"subexprPos": "/1", "info": {"p": "4"}},
[{"subexprPos": "/1", "info": {"__rpcref": "4"}},
{"append":
[{"tag": [{"subexprPos": "/1/0/1", "info": {"p": "5"}}, {"text": "n"}]},
[{"tag":
[{"subexprPos": "/1/0/1", "info": {"__rpcref": "5"}}, {"text": "n"}]},
{"text": " < "},
{"tag":
[{"subexprPos": "/1/1", "info": {"p": "6"}},
[{"subexprPos": "/1/1", "info": {"__rpcref": "6"}},
{"append":
[{"tag":
[{"subexprPos": "/1/1/0/1", "info": {"p": "7"}}, {"text": "n"}]},
[{"subexprPos": "/1/1/0/1", "info": {"__rpcref": "7"}},
{"text": "n"}]},
{"text": " + "},
{"tag":
[{"subexprPos": "/1/1/1", "info": {"p": "8"}},
[{"subexprPos": "/1/1/1", "info": {"__rpcref": "8"}},
{"text": "42"}]}]}]}]}]}]}]},
"term": {"p": "0"},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 24, "character": 2}, "end": {"line": 24, "character": 74}},
"hyps": [],
"ctx": {"p": "9"}}
"ctx": {"__rpcref": "9"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 24, "character": 6}}
{"type": {"tag": [{"subexprPos": "/", "info": {"p": "1"}}, {"text": "Nat"}]},
"term": {"p": "0"},
{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "1"}}, {"text": "Nat"}]},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 24, "character": 6}, "end": {"line": 24, "character": 7}},
"hyps": [],
"ctx": {"p": "2"}}
"ctx": {"__rpcref": "2"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 30, "character": 6}}
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "2"}},
[{"subexprPos": "/", "info": {"__rpcref": "2"}},
{"append":
[{"text": "∀ ("},
{"tag": [{"subexprPos": "/", "info": {"p": "3"}}, {"text": "n "}]},
{"tag": [{"subexprPos": "/", "info": {"p": "4"}}, {"text": "m"}]},
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "3"}}, {"text": "n "}]},
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "4"}}, {"text": "m"}]},
{"text": " : "},
{"tag": [{"subexprPos": "/1/0", "info": {"p": "5"}}, {"text": "Nat"}]},
{"tag":
[{"subexprPos": "/1/0", "info": {"__rpcref": "5"}}, {"text": "Nat"}]},
{"text": "), "},
{"tag":
[{"subexprPos": "/1/1", "info": {"p": "6"}},
[{"subexprPos": "/1/1", "info": {"__rpcref": "6"}},
{"append":
[{"tag":
[{"subexprPos": "/1/1/0/1", "info": {"p": "7"}},
[{"subexprPos": "/1/1/0/1", "info": {"__rpcref": "7"}},
{"append":
[{"tag":
[{"subexprPos": "/1/1/0/1/0/1", "info": {"p": "8"}},
[{"subexprPos": "/1/1/0/1/0/1", "info": {"__rpcref": "8"}},
{"text": "n"}]},
{"text": " + "},
{"tag":
[{"subexprPos": "/1/1/0/1/1", "info": {"p": "9"}},
[{"subexprPos": "/1/1/0/1/1", "info": {"__rpcref": "9"}},
{"text": "m"}]}]}]},
{"text": " = "},
{"tag":
[{"subexprPos": "/1/1/1", "info": {"p": "10"}},
[{"subexprPos": "/1/1/1", "info": {"__rpcref": "10"}},
{"append":
[{"tag":
[{"subexprPos": "/1/1/1/0/1", "info": {"p": "11"}},
[{"subexprPos": "/1/1/1/0/1", "info": {"__rpcref": "11"}},
{"text": "m"}]},
{"text": " + "},
{"tag":
[{"subexprPos": "/1/1/1/1", "info": {"p": "12"}},
[{"subexprPos": "/1/1/1/1", "info": {"__rpcref": "12"}},
{"text": "n"}]}]}]}]}]}]}]},
"term": {"p": "0"},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 30, "character": 6}, "end": {"line": 30, "character": 18}},
"hyps":
[{"type": {"tag": [{"subexprPos": "/", "info": {"p": "1"}}, {"text": "Nat"}]},
[{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "1"}}, {"text": "Nat"}]},
"names": ["n"],
"fvarIds": []}],
"ctx": {"p": "13"}}
"ctx": {"__rpcref": "13"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 32, "character": 8}}
{"type":
{"tag":
[{"subexprPos": "/", "info": {"p": "2"}},
[{"subexprPos": "/", "info": {"__rpcref": "2"}},
{"append":
[{"tag": [{"subexprPos": "/0/1", "info": {"p": "3"}}, {"text": "n"}]},
[{"tag":
[{"subexprPos": "/0/1", "info": {"__rpcref": "3"}}, {"text": "n"}]},
{"text": " < "},
{"tag":
[{"subexprPos": "/1", "info": {"p": "4"}},
[{"subexprPos": "/1", "info": {"__rpcref": "4"}},
{"append":
[{"tag": [{"subexprPos": "/1/0/1", "info": {"p": "5"}}, {"text": "n"}]},
[{"tag":
[{"subexprPos": "/1/0/1", "info": {"__rpcref": "5"}}, {"text": "n"}]},
{"text": " + "},
{"tag":
[{"subexprPos": "/1/1", "info": {"p": "6"}}, {"text": "1"}]}]}]}]}]},
"term": {"p": "0"},
[{"subexprPos": "/1/1", "info": {"__rpcref": "6"}},
{"text": "1"}]}]}]}]}]},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 32, "character": 8}, "end": {"line": 32, "character": 26}},
"hyps":
[{"type": {"tag": [{"subexprPos": "/", "info": {"p": "1"}}, {"text": "Nat"}]},
[{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "1"}}, {"text": "Nat"}]},
"names": ["n"],
"fvarIds": []}],
"ctx": {"p": "7"}}
"ctx": {"__rpcref": "7"}}
{"textDocument": {"uri": "file:///interactiveTermGoals.lean"},
"position": {"line": 35, "character": 14}}
{"type": {"tag": [{"subexprPos": "/", "info": {"p": "2"}}, {"text": "Nat"}]},
"term": {"p": "0"},
{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "2"}}, {"text": "Nat"}]},
"term": {"__rpcref": "0"},
"range":
{"start": {"line": 35, "character": 14}, "end": {"line": 35, "character": 15}},
"hyps":
[{"type": {"tag": [{"subexprPos": "/", "info": {"p": "1"}}, {"text": "Nat"}]},
[{"type":
{"tag": [{"subexprPos": "/", "info": {"__rpcref": "1"}}, {"text": "Nat"}]},
"names": ["n"],
"fvarIds": []}],
"ctx": {"p": "3"}}
"ctx": {"__rpcref": "3"}}

2
tests/server_interactive/userWidget.lean
View File

@@ -1,4 +1,4 @@
import Lean
import Lean.Widget.Commands
open Lean
@[widget_module]