fix: lengthen RPC reference field name (#719)

Client part of leanprover/lean4#12905. Fixes #712.

Author: Vtec234

lean4-infoview-api/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview-api",
-    "version": "0.11.0",
+    "version": "0.12.0",
     "description": "Types and API for @leanprover/infoview.",
     "repository": {
         "type": "git",
@@ -9,7 +9,7 @@
     "scripts": {
         "watch": "tsc --watch",
         "watchTest": "tsc --watch",
-        "build": "tsc",
+        "build": "tsc --sourceMap false",
         "build:dev": "tsc"
     },
     "main": "dist/index",

lean4-infoview-api/src/infoviewApi.ts

@@ -11,13 +11,16 @@ export type ModuleHierarchyOptions = {}
 
 export type HighlightMatchesOptions = {}
 
+export type RpcWireFormat = 'v0' | 'v1'
+
 export interface RpcOptions {
-    highlightMatchesProvider?: HighlightMatchesOptions | undefined
+    highlightMatchesProvider?: HighlightMatchesOptions
+    rpcWireFormat?: RpcWireFormat
 }
 
 export interface LeanServerCapabilities {
-    moduleHierarchyProvider?: ModuleHierarchyOptions | undefined
-    rpcProvider?: RpcOptions | undefined
+    moduleHierarchyProvider?: ModuleHierarchyOptions
+    rpcProvider?: RpcOptions
 }
 
 export type ExpectedTypeVisibility = 'Expanded by default' | 'Collapsed by default' | 'Hidden'

lean4-infoview-api/src/lspTypes.ts

@@ -69,17 +69,19 @@ declare const tag: unique symbol
  * which we need to be able to reference but which would be too large to
  * send over directly.
  */
-export type RpcPtr<T> = { readonly [tag]: T; p: string }
+export type RpcPtr<T> = { readonly [tag]: T; __rpcref: string } | { readonly [tag]: T; p: string }
 
 // eslint-disable-next-line @typescript-eslint/no-namespace
 export namespace RpcPtr {
     export function copy<T>(p: RpcPtr<T>): RpcPtr<T> {
-        return { p: p.p } as RpcPtr<T>
+        if ('p' in p) return { p: p.p } as RpcPtr<T>
+        else return { __rpcref: p.__rpcref } as RpcPtr<T>
     }
 
     /** Turns a reference into a unique string. Useful for React `key`s. */
     export function toKey(p: RpcPtr<any>): string {
-        return p.p
+        if ('p' in p) return p.p
+        else return p.__rpcref
     }
 }
 

lean4-infoview-api/src/rpcSessions.ts

@@ -1,5 +1,10 @@
-import type { DocumentUri, Position, TextDocumentPositionParams } from 'vscode-languageserver-protocol'
-import { ClientRequestOptions } from './infoviewApi'
+import type {
+    DocumentUri,
+    Position,
+    ServerCapabilities,
+    TextDocumentPositionParams,
+} from 'vscode-languageserver-protocol'
+import { ClientRequestOptions, LeanServerCapabilities } from './infoviewApi'
 import { RpcCallParams, RpcErrorCode, RpcPtr, RpcReleaseParams } from './lspTypes'
 
 /**
@@ -83,6 +88,7 @@ class RpcSessionForFile {
     constructor(
         public uri: DocumentUri,
         public sessions: RpcSessions,
+        private serverCapabilities: ServerCapabilities<LeanServerCapabilities>,
     ) {
         this.sessionId = (async () => {
             try {
@@ -133,23 +139,34 @@ class RpcSessionForFile {
      * for future garbage collection.
      *
      * The function implements a form of "conservative garbage collection"
-     * where it treats any subobject `{'p': v}` as a potential RPC reference.
-     * Therefore `p` should not be used as a field name on the Lean side
+     * where it treats any subobject `{'__rpcref': v}` as a potential RPC reference.
+     * Therefore `__rpcref` should not be used as a field name on the Lean side
      * to prevent false positives.
      *
-     * It is unclear if the false positives will become a big issue.
      * Earlier versions of the extension
      * had manually written registration functions for every type,
      * but those are a lot of boilerplate.
      * If we change back to that approach,
      * we should generate them automatically.
+     * It would also be possible to move to a new RPC wire format
+     * that specifies which values are references using metadata.
      */
     registerRefs(o: any) {
         if (o instanceof Object) {
-            if (Object.keys(o as {}).length === 1 && 'p' in o && typeof o.p !== 'object') {
-                this.finalizers.register(o as {}, RpcPtr.copy(o as RpcPtr<any>))
+            let isRef = false
+            if (this.serverCapabilities.experimental?.rpcProvider?.rpcWireFormat === 'v1') {
+                if (Object.keys(o as {}).length === 1 && '__rpcref' in o && typeof o.__rpcref === 'string') {
+                    this.finalizers.register(o as {}, RpcPtr.copy(o as RpcPtr<any>))
+                    isRef = true
+                }
             } else {
-                for (const v of Object.values(o as {})) this.registerRefs(v)
+                if (Object.keys(o as {}).length === 1 && 'p' in o && typeof o.p === 'string') {
+                    this.finalizers.register(o as {}, RpcPtr.copy(o as RpcPtr<any>))
+                    isRef = true
+                }
+            }
+            if (!isRef) {
+                for (const v of Object.values(o)) this.registerRefs(v)
             }
         } else if (o instanceof Array) {
             for (const e of o) this.registerRefs(e)
@@ -240,9 +257,12 @@ export class RpcSessions {
 
     constructor(public iface: RpcServerIface) {}
 
-    private connectCore(uri: DocumentUri): RpcSessionForFile {
+    private connectCore(
+        uri: DocumentUri,
+        serverCapabilities: ServerCapabilities<LeanServerCapabilities>,
+    ): RpcSessionForFile {
         if (this.sessions.has(uri)) return this.sessions.get(uri) as RpcSessionForFile
-        const sess = new RpcSessionForFile(uri, this)
+        const sess = new RpcSessionForFile(uri, this, serverCapabilities)
         this.sessions.set(uri, sess)
         return sess
     }
@@ -254,8 +274,11 @@ export class RpcSessions {
      * A new session is only created if a fatal error occurs (the worker crashes)
      * or the session is closed manually (the file is closed).
      */
-    connect(pos: TextDocumentPositionParams): RpcSessionAtPos {
-        return this.connectCore(pos.textDocument.uri).at(pos.position)
+    connect(
+        pos: TextDocumentPositionParams,
+        serverCapabilities: ServerCapabilities<LeanServerCapabilities>,
+    ): RpcSessionAtPos {
+        return this.connectCore(pos.textDocument.uri, serverCapabilities).at(pos.position)
     }
 
     /** Closes the session for the given URI. */

lean4-infoview/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview",
-    "version": "0.11.1",
+    "version": "0.12.0",
     "description": "An interactive display for the Lean 4 theorem prover.",
     "repository": {
         "type": "git",
@@ -57,7 +57,7 @@
         "typescript": "^5.4.5"
     },
     "dependencies": {
-        "@leanprover/infoview-api": "~0.11.0",
+        "@leanprover/infoview-api": "~0.12.0",
         "@vscode/codicons": "^0.0.40",
         "@vscode-elements/react-elements": "^0.5.0",
         "es-module-lexer": "^1.5.4",

lean4-infoview/src/infoview/main.tsx

@@ -57,9 +57,8 @@ function Main() {
         [],
     )
 
-    const serverVersion = useEventResult(
-        ec.events.serverRestarted,
-        result => new ServerVersion(result.serverInfo?.version ?? ''),
+    const serverVersion = useEventResult(ec.events.serverRestarted, result =>
+        ServerVersion.ofString(result.serverInfo?.version ?? ''),
     )
     const capabilities = useEventResult(ec.events.serverRestarted, result => result.capabilities)
     const serverStoppedResult = useEventResult(ec.events.serverStopped)

lean4-infoview/src/infoview/rpcSessions.tsx

@@ -5,7 +5,7 @@ import type {
     DocumentUri,
     TextDocumentPositionParams,
 } from 'vscode-languageserver-protocol'
-import { EditorContext, EnvPosContext } from './contexts'
+import { CapabilityContext, EditorContext, EnvPosContext } from './contexts'
 import { DocumentPosition, useClientNotificationEffect, useEvent } from './util'
 
 const RpcSessionsContext = React.createContext<RpcSessions | undefined>(undefined)
@@ -46,20 +46,20 @@ export function WithRpcSessions({ children }: { children: React.ReactNode }) {
     return <RpcSessionsContext.Provider value={sessions}>{children}</RpcSessionsContext.Provider>
 }
 
-const noCtxRpcSession: RpcSessionAtPos = {
-    call: async () => {
-        throw new Error('no RPC context set')
-    },
-}
-
-const noPosRpcSession: RpcSessionAtPos = {
-    call: async () => {
-        throw new Error('no position context set')
-    },
+function errorRpcSession(err: string): RpcSessionAtPos {
+    return {
+        call: async () => {
+            throw new Error(err)
+        },
+    }
 }
 
 export function useRpcSessionAtTdpp(pos: TextDocumentPositionParams): RpcSessionAtPos {
-    return React.useContext(RpcSessionsContext)?.connect(pos) || noCtxRpcSession
+    const rsc = React.useContext(RpcSessionsContext)
+    const cap = React.useContext(CapabilityContext)
+    if (!rsc) return errorRpcSession('no RPC context set')
+    if (!cap) return errorRpcSession('no capability context set')
+    return rsc.connect(pos, cap)
 }
 
 export function useRpcSessionAtPos(pos: DocumentPosition): RpcSessionAtPos {
@@ -73,7 +73,7 @@ export function useRpcSessionAtPos(pos: DocumentPosition): RpcSessionAtPos {
  * A future major release of @leanprover/infoview could remove this context
  * after it has been deprecated for a sufficiently long time.
  */
-export const RpcContext = React.createContext<RpcSessionAtPos>(noCtxRpcSession)
+export const RpcContext = React.createContext<RpcSessionAtPos>(errorRpcSession('no RPC context set'))
 
 /**
  * Retrieve an RPC session at {@link EnvPosContext},
@@ -82,8 +82,13 @@ export const RpcContext = React.createContext<RpcSessionAtPos>(noCtxRpcSession)
  */
 export function useRpcSession(): RpcSessionAtPos {
     const pos = React.useContext(EnvPosContext)
+    // Cannot deduplicate with `useRpcSessionAtTdpp`
+    // because we'd only call it when `pos !== undefined`
+    // but hooks must be called unconditionally.
     const rsc = React.useContext(RpcSessionsContext)
-    if (!pos) return noPosRpcSession
-    if (!rsc) return noCtxRpcSession
-    return rsc.connect(DocumentPosition.toTdpp(pos))
+    const cap = React.useContext(CapabilityContext)
+    if (!pos) return errorRpcSession('no position context set')
+    if (!rsc) return errorRpcSession('no RPC context set')
+    if (!cap) return errorRpcSession('no capability context set')
+    return rsc.connect(DocumentPosition.toTdpp(pos), cap)
 }

lean4-infoview/src/infoview/serverVersion.ts

@@ -4,22 +4,37 @@
  */
 
 export class ServerVersion {
-    major: number
-    minor: number
-    patch: number
+    constructor(
+        public major: number,
+        public minor: number,
+        public patch: number,
+    ) {}
 
-    constructor(version: string) {
+    static ofString(version: string): ServerVersion {
         const vs = version.split('.')
         if (vs.length === 2) {
-            this.major = parseInt(vs[0])
-            this.minor = parseInt(vs[1])
-            this.patch = 0
+            return new ServerVersion(parseInt(vs[0]), parseInt(vs[1]), 0)
         } else if (vs.length === 3) {
-            this.major = parseInt(vs[0])
-            this.minor = parseInt(vs[1])
-            this.patch = parseInt(vs[2])
+            return new ServerVersion(parseInt(vs[0]), parseInt(vs[1]), parseInt(vs[2]))
         } else {
             throw new Error(`cannot parse Lean server version '${version}'`)
         }
     }
+
+    /** Is `this` version equal to `other`? */
+    eq(other: ServerVersion): boolean {
+        return this.major === other.major && this.minor === other.minor && this.patch === other.patch
+    }
+
+    /** Is `this` version strictly below `other`? */
+    lt(other: ServerVersion): boolean {
+        if (this.major !== other.major) return this.major < other.major
+        if (this.minor !== other.minor) return this.minor < other.minor
+        return this.patch < other.patch
+    }
+
+    /** Is `this` version either strictly below or equal to `other`? */
+    le(other: ServerVersion): boolean {
+        return this.lt(other) || this.eq(other)
+    }
 }