From a0528650f10a3a2d8fc77b0389dfa870561d8ad9 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Tue, 3 Mar 2026 15:43:02 -0500
Subject: [PATCH 1/8] fix: stricter typeof check

---
 lean4-infoview-api/src/rpcSessions.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean4-infoview-api/src/rpcSessions.ts b/lean4-infoview-api/src/rpcSessions.ts
index 1fdbb342..bc97c6e6 100644
--- a/lean4-infoview-api/src/rpcSessions.ts
+++ b/lean4-infoview-api/src/rpcSessions.ts
@@ -146,7 +146,7 @@ class RpcSessionForFile {
      */
     registerRefs(o: any) {
         if (o instanceof Object) {
-            if (Object.keys(o as {}).length === 1 && 'p' in o && typeof o.p !== 'object') {
+            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>))
             } else {
                 for (const v of Object.values(o as {})) this.registerRefs(v)

From 0131bd29cdcb3fb88c1733e35b98062c4034d70a Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Tue, 3 Mar 2026 19:05:52 -0500
Subject: [PATCH 2/8] chore: pass server version around

---
 lean4-infoview-api/src/index.ts               |  1 +
 lean4-infoview-api/src/rpcSessions.ts         | 10 +++--
 .../src}/serverVersion.ts                     |  0
 lean4-infoview/src/index.tsx                  |  1 -
 lean4-infoview/src/infoview/contexts.ts       |  2 +-
 lean4-infoview/src/infoview/main.tsx          |  2 +-
 lean4-infoview/src/infoview/rpcSessions.tsx   | 37 +++++++++++--------
 7 files changed, 30 insertions(+), 23 deletions(-)
 rename {lean4-infoview/src/infoview => lean4-infoview-api/src}/serverVersion.ts (100%)

diff --git a/lean4-infoview-api/src/index.ts b/lean4-infoview-api/src/index.ts
index 12fb8b39..80ed82b4 100644
--- a/lean4-infoview-api/src/index.ts
+++ b/lean4-infoview-api/src/index.ts
@@ -2,4 +2,5 @@ export * from './infoviewApi'
 export * from './lspTypes'
 export * from './rpcApi'
 export * from './rpcSessions'
+export * from './serverVersion'
 export * from './util'
diff --git a/lean4-infoview-api/src/rpcSessions.ts b/lean4-infoview-api/src/rpcSessions.ts
index bc97c6e6..12920ac4 100644
--- a/lean4-infoview-api/src/rpcSessions.ts
+++ b/lean4-infoview-api/src/rpcSessions.ts
@@ -1,6 +1,7 @@
 import type { DocumentUri, Position, TextDocumentPositionParams } from 'vscode-languageserver-protocol'
 import { ClientRequestOptions } from './infoviewApi'
 import { RpcCallParams, RpcErrorCode, RpcPtr, RpcReleaseParams } from './lspTypes'
+import { ServerVersion } from './serverVersion'
 
 /**
  * Abstraction of the functionality needed
@@ -83,6 +84,7 @@ class RpcSessionForFile {
     constructor(
         public uri: DocumentUri,
         public sessions: RpcSessions,
+        private serverVersion: ServerVersion,
     ) {
         this.sessionId = (async () => {
             try {
@@ -240,9 +242,9 @@ export class RpcSessions {
 
     constructor(public iface: RpcServerIface) {}
 
-    private connectCore(uri: DocumentUri): RpcSessionForFile {
+    private connectCore(uri: DocumentUri, serverVersion: ServerVersion): 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, serverVersion)
         this.sessions.set(uri, sess)
         return sess
     }
@@ -254,8 +256,8 @@ 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, serverVersion: ServerVersion): RpcSessionAtPos {
+        return this.connectCore(pos.textDocument.uri, serverVersion).at(pos.position)
     }
 
     /** Closes the session for the given URI. */
diff --git a/lean4-infoview/src/infoview/serverVersion.ts b/lean4-infoview-api/src/serverVersion.ts
similarity index 100%
rename from lean4-infoview/src/infoview/serverVersion.ts
rename to lean4-infoview-api/src/serverVersion.ts
diff --git a/lean4-infoview/src/index.tsx b/lean4-infoview/src/index.tsx
index b0311b11..5c7d1ca9 100644
--- a/lean4-infoview/src/index.tsx
+++ b/lean4-infoview/src/index.tsx
@@ -10,7 +10,6 @@ export { GoalLocation, GoalsLocation, LocationsContext } from './infoview/goalLo
 export { InteractiveCode, InteractiveCodeProps, Markdown } from './infoview/interactiveCode'
 export { renderInfoview } from './infoview/main'
 export { RpcContext, useRpcSession } from './infoview/rpcSessions'
-export { ServerVersion } from './infoview/serverVersion'
 export { DynamicComponent, DynamicComponentProps, importWidgetModule, PanelWidgetProps } from './infoview/userWidget'
 export {
     DocumentPosition,
diff --git a/lean4-infoview/src/infoview/contexts.ts b/lean4-infoview/src/infoview/contexts.ts
index 7a30e757..0efffc9a 100644
--- a/lean4-infoview/src/infoview/contexts.ts
+++ b/lean4-infoview/src/infoview/contexts.ts
@@ -7,10 +7,10 @@ import {
     LeanDiagnostic,
     LeanFileProgressProcessingInfo,
     LeanServerCapabilities,
+    ServerVersion,
 } from '@leanprover/infoview-api'
 
 import { EditorConnection } from './editorConnection'
-import { ServerVersion } from './serverVersion'
 import { DocumentPosition } from './util'
 
 // Type-unsafe initializers for contexts which we immediately set up at the top-level.
diff --git a/lean4-infoview/src/infoview/main.tsx b/lean4-infoview/src/infoview/main.tsx
index b7cc2c7b..72e69c50 100644
--- a/lean4-infoview/src/infoview/main.tsx
+++ b/lean4-infoview/src/infoview/main.tsx
@@ -15,6 +15,7 @@ import {
     InfoviewApi,
     LeanFileProgressParams,
     LeanFileProgressProcessingInfo,
+    ServerVersion,
 } from '@leanprover/infoview-api'
 
 import { CapabilityContext, ConfigContext, EditorContext, ProgressContext, VersionContext } from './contexts'
@@ -23,7 +24,6 @@ import { EventEmitter } from './event'
 import { Infos } from './infos'
 import { AllMessages, WithLspDiagnosticsContext } from './messages'
 import { WithRpcSessions } from './rpcSessions'
-import { ServerVersion } from './serverVersion'
 import { useClientNotificationEffect, useEventResult, useServerNotificationState } from './util'
 
 function Main() {
diff --git a/lean4-infoview/src/infoview/rpcSessions.tsx b/lean4-infoview/src/infoview/rpcSessions.tsx
index 798aaeab..86342c32 100644
--- a/lean4-infoview/src/infoview/rpcSessions.tsx
+++ b/lean4-infoview/src/infoview/rpcSessions.tsx
@@ -5,7 +5,7 @@ import type {
     DocumentUri,
     TextDocumentPositionParams,
 } from 'vscode-languageserver-protocol'
-import { EditorContext, EnvPosContext } from './contexts'
+import { EditorContext, EnvPosContext, VersionContext } 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 ver = React.useContext(VersionContext)
+    if (!rsc) return errorRpcSession('no RPC context set')
+    if (!ver) return errorRpcSession('no server version context set')
+    return rsc.connect(pos, ver)
 }
 
 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 ver = React.useContext(VersionContext)
+    if (!pos) return errorRpcSession('no position context set')
+    if (!rsc) return errorRpcSession('no RPC context set')
+    if (!ver) return errorRpcSession('no server version context set')
+    return rsc.connect(DocumentPosition.toTdpp(pos), ver)
 }

From aa0fae46492d8afa273202267b5c48276541a428 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Tue, 3 Mar 2026 19:06:30 -0500
Subject: [PATCH 3/8] feat: use longer name on newer servers

---
 lean4-infoview-api/src/lspTypes.ts      |  8 +++---
 lean4-infoview-api/src/rpcSessions.ts   |  9 ++++---
 lean4-infoview-api/src/serverVersion.ts | 35 ++++++++++++++++++-------
 3 files changed, 36 insertions(+), 16 deletions(-)

diff --git a/lean4-infoview-api/src/lspTypes.ts b/lean4-infoview-api/src/lspTypes.ts
index 990549fa..3c624b10 100644
--- a/lean4-infoview-api/src/lspTypes.ts
+++ b/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
     }
 }
 
diff --git a/lean4-infoview-api/src/rpcSessions.ts b/lean4-infoview-api/src/rpcSessions.ts
index 12920ac4..0a1479a1 100644
--- a/lean4-infoview-api/src/rpcSessions.ts
+++ b/lean4-infoview-api/src/rpcSessions.ts
@@ -148,10 +148,13 @@ class RpcSessionForFile {
      */
     registerRefs(o: any) {
         if (o instanceof Object) {
-            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>))
+            if (this.serverVersion.le(new ServerVersion(0, 3, 0))) {
+                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>))
+                }
             } else {
-                for (const v of Object.values(o as {})) this.registerRefs(v)
+                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>))
             }
         } else if (o instanceof Array) {
             for (const e of o) this.registerRefs(e)
diff --git a/lean4-infoview-api/src/serverVersion.ts b/lean4-infoview-api/src/serverVersion.ts
index 5007a675..d023b58e 100644
--- a/lean4-infoview-api/src/serverVersion.ts
+++ b/lean4-infoview-api/src/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.le(other)
+    }
 }

From 8d6f5232314043314012a16ee0b242ea7b7c70a2 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Tue, 3 Mar 2026 19:31:04 -0500
Subject: [PATCH 4/8] fix: typo

---
 lean4-infoview-api/src/serverVersion.ts | 2 +-
 lean4-infoview/src/infoview/main.tsx    | 5 ++---
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/lean4-infoview-api/src/serverVersion.ts b/lean4-infoview-api/src/serverVersion.ts
index d023b58e..3d56bff5 100644
--- a/lean4-infoview-api/src/serverVersion.ts
+++ b/lean4-infoview-api/src/serverVersion.ts
@@ -35,6 +35,6 @@ export class ServerVersion {
 
     /** Is `this` version either strictly below or equal to `other`? */
     le(other: ServerVersion): boolean {
-        return this.lt(other) || this.le(other)
+        return this.lt(other) || this.eq(other)
     }
 }
diff --git a/lean4-infoview/src/infoview/main.tsx b/lean4-infoview/src/infoview/main.tsx
index 72e69c50..8747e25f 100644
--- a/lean4-infoview/src/infoview/main.tsx
+++ b/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)

From 1d6863af339beaf095ba9991767bfc2d55332d01 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Tue, 3 Mar 2026 19:38:10 -0500
Subject: [PATCH 5/8] feat: client/server capabilities

---
 lean4-infoview-api/package.json               |  2 +-
 lean4-infoview-api/src/index.ts               |  1 -
 lean4-infoview-api/src/infoviewApi.ts         |  9 ++++--
 lean4-infoview-api/src/rpcSessions.ts         | 28 +++++++++++--------
 lean4-infoview/package.json                   |  4 +--
 lean4-infoview/src/infoview/contexts.ts       |  2 +-
 lean4-infoview/src/infoview/main.tsx          |  2 +-
 lean4-infoview/src/infoview/rpcSessions.tsx   | 14 +++++-----
 .../src/infoview}/serverVersion.ts            |  0
 package-lock.json                             | 10 +++----
 vscode-lean4/package.json                     |  4 +--
 vscode-lean4/src/leanclient.ts                |  7 +++--
 12 files changed, 46 insertions(+), 37 deletions(-)
 rename {lean4-infoview-api/src => lean4-infoview/src/infoview}/serverVersion.ts (100%)

diff --git a/lean4-infoview-api/package.json b/lean4-infoview-api/package.json
index df9d86d0..6da8d666 100644
--- a/lean4-infoview-api/package.json
+++ b/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",
diff --git a/lean4-infoview-api/src/index.ts b/lean4-infoview-api/src/index.ts
index 80ed82b4..12fb8b39 100644
--- a/lean4-infoview-api/src/index.ts
+++ b/lean4-infoview-api/src/index.ts
@@ -2,5 +2,4 @@ export * from './infoviewApi'
 export * from './lspTypes'
 export * from './rpcApi'
 export * from './rpcSessions'
-export * from './serverVersion'
 export * from './util'
diff --git a/lean4-infoview-api/src/infoviewApi.ts b/lean4-infoview-api/src/infoviewApi.ts
index c16db0bb..415fcb0c 100644
--- a/lean4-infoview-api/src/infoviewApi.ts
+++ b/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'
diff --git a/lean4-infoview-api/src/rpcSessions.ts b/lean4-infoview-api/src/rpcSessions.ts
index 0a1479a1..a42f6cc0 100644
--- a/lean4-infoview-api/src/rpcSessions.ts
+++ b/lean4-infoview-api/src/rpcSessions.ts
@@ -1,7 +1,6 @@
-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'
-import { ServerVersion } from './serverVersion'
 
 /**
  * Abstraction of the functionality needed
@@ -84,7 +83,7 @@ class RpcSessionForFile {
     constructor(
         public uri: DocumentUri,
         public sessions: RpcSessions,
-        private serverVersion: ServerVersion,
+        private serverCapabilities: ServerCapabilities<LeanServerCapabilities>,
     ) {
         this.sessionId = (async () => {
             try {
@@ -148,13 +147,20 @@ class RpcSessionForFile {
      */
     registerRefs(o: any) {
         if (o instanceof Object) {
-            if (this.serverVersion.le(new ServerVersion(0, 3, 0))) {
-                if (Object.keys(o as {}).length === 1 && 'p' in o && typeof o.p === 'string') {
+            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 {
-                if (Object.keys(o as {}).length === 1 && '__rpcref' in o && typeof o.__rpcref === 'string')
+                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)
@@ -245,9 +251,9 @@ export class RpcSessions {
 
     constructor(public iface: RpcServerIface) {}
 
-    private connectCore(uri: DocumentUri, serverVersion: ServerVersion): 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, serverVersion)
+        const sess = new RpcSessionForFile(uri, this, serverCapabilities)
         this.sessions.set(uri, sess)
         return sess
     }
@@ -259,8 +265,8 @@ 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, serverVersion: ServerVersion): RpcSessionAtPos {
-        return this.connectCore(pos.textDocument.uri, serverVersion).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. */
diff --git a/lean4-infoview/package.json b/lean4-infoview/package.json
index 486a90ed..4d125939 100644
--- a/lean4-infoview/package.json
+++ b/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",
diff --git a/lean4-infoview/src/infoview/contexts.ts b/lean4-infoview/src/infoview/contexts.ts
index 0efffc9a..7a30e757 100644
--- a/lean4-infoview/src/infoview/contexts.ts
+++ b/lean4-infoview/src/infoview/contexts.ts
@@ -7,10 +7,10 @@ import {
     LeanDiagnostic,
     LeanFileProgressProcessingInfo,
     LeanServerCapabilities,
-    ServerVersion,
 } from '@leanprover/infoview-api'
 
 import { EditorConnection } from './editorConnection'
+import { ServerVersion } from './serverVersion'
 import { DocumentPosition } from './util'
 
 // Type-unsafe initializers for contexts which we immediately set up at the top-level.
diff --git a/lean4-infoview/src/infoview/main.tsx b/lean4-infoview/src/infoview/main.tsx
index 8747e25f..e5e8f465 100644
--- a/lean4-infoview/src/infoview/main.tsx
+++ b/lean4-infoview/src/infoview/main.tsx
@@ -15,7 +15,6 @@ import {
     InfoviewApi,
     LeanFileProgressParams,
     LeanFileProgressProcessingInfo,
-    ServerVersion,
 } from '@leanprover/infoview-api'
 
 import { CapabilityContext, ConfigContext, EditorContext, ProgressContext, VersionContext } from './contexts'
@@ -24,6 +23,7 @@ import { EventEmitter } from './event'
 import { Infos } from './infos'
 import { AllMessages, WithLspDiagnosticsContext } from './messages'
 import { WithRpcSessions } from './rpcSessions'
+import { ServerVersion } from './serverVersion'
 import { useClientNotificationEffect, useEventResult, useServerNotificationState } from './util'
 
 function Main() {
diff --git a/lean4-infoview/src/infoview/rpcSessions.tsx b/lean4-infoview/src/infoview/rpcSessions.tsx
index 86342c32..a03ba340 100644
--- a/lean4-infoview/src/infoview/rpcSessions.tsx
+++ b/lean4-infoview/src/infoview/rpcSessions.tsx
@@ -5,7 +5,7 @@ import type {
     DocumentUri,
     TextDocumentPositionParams,
 } from 'vscode-languageserver-protocol'
-import { EditorContext, EnvPosContext, VersionContext } from './contexts'
+import { CapabilityContext, EditorContext, EnvPosContext } from './contexts'
 import { DocumentPosition, useClientNotificationEffect, useEvent } from './util'
 
 const RpcSessionsContext = React.createContext<RpcSessions | undefined>(undefined)
@@ -56,10 +56,10 @@ function errorRpcSession(err: string): RpcSessionAtPos {
 
 export function useRpcSessionAtTdpp(pos: TextDocumentPositionParams): RpcSessionAtPos {
     const rsc = React.useContext(RpcSessionsContext)
-    const ver = React.useContext(VersionContext)
+    const cap = React.useContext(CapabilityContext)
     if (!rsc) return errorRpcSession('no RPC context set')
-    if (!ver) return errorRpcSession('no server version context set')
-    return rsc.connect(pos, ver)
+    if (!cap) return errorRpcSession('no capability context set')
+    return rsc.connect(pos, cap)
 }
 
 export function useRpcSessionAtPos(pos: DocumentPosition): RpcSessionAtPos {
@@ -86,9 +86,9 @@ export function useRpcSession(): RpcSessionAtPos {
     // because we'd only call it when `pos !== undefined`
     // but hooks must be called unconditionally.
     const rsc = React.useContext(RpcSessionsContext)
-    const ver = React.useContext(VersionContext)
+    const cap = React.useContext(CapabilityContext)
     if (!pos) return errorRpcSession('no position context set')
     if (!rsc) return errorRpcSession('no RPC context set')
-    if (!ver) return errorRpcSession('no server version context set')
-    return rsc.connect(DocumentPosition.toTdpp(pos), ver)
+    if (!cap) return errorRpcSession('no capability context set')
+    return rsc.connect(DocumentPosition.toTdpp(pos), cap)
 }
diff --git a/lean4-infoview-api/src/serverVersion.ts b/lean4-infoview/src/infoview/serverVersion.ts
similarity index 100%
rename from lean4-infoview-api/src/serverVersion.ts
rename to lean4-infoview/src/infoview/serverVersion.ts
diff --git a/package-lock.json b/package-lock.json
index e21264cb..c20a2054 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -28,10 +28,10 @@
         },
         "lean4-infoview": {
             "name": "@leanprover/infoview",
-            "version": "0.11.1",
+            "version": "0.12.0",
             "license": "Apache-2.0",
             "dependencies": {
-                "@leanprover/infoview-api": "~0.11.0",
+                "@leanprover/infoview-api": "~0.12.0",
                 "@vscode-elements/react-elements": "^0.5.0",
                 "@vscode/codicons": "^0.0.40",
                 "es-module-lexer": "^1.5.4",
@@ -68,7 +68,7 @@
         },
         "lean4-infoview-api": {
             "name": "@leanprover/infoview-api",
-            "version": "0.11.0",
+            "version": "0.12.0",
             "license": "Apache-2.0",
             "devDependencies": {
                 "typescript": "^5.4.5",
@@ -16218,8 +16218,8 @@
             "version": "0.0.225",
             "license": "Apache-2.0",
             "dependencies": {
-                "@leanprover/infoview": "~0.11.1",
-                "@leanprover/infoview-api": "~0.11.0",
+                "@leanprover/infoview": "~0.12.0",
+                "@leanprover/infoview-api": "~0.12.0",
                 "@leanprover/unicode-input": "~0.1.9",
                 "@leanprover/unicode-input-component": "~0.2.0",
                 "@vscode-elements/elements": "^1.7.1",
diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
index c50522dd..c37da066 100644
--- a/vscode-lean4/package.json
+++ b/vscode-lean4/package.json
@@ -1779,8 +1779,8 @@
         "test": "node ./out/test/suite/runTest.js"
     },
     "dependencies": {
-        "@leanprover/infoview": "~0.11.1",
-        "@leanprover/infoview-api": "~0.11.0",
+        "@leanprover/infoview": "~0.12.0",
+        "@leanprover/infoview-api": "~0.12.0",
         "@leanprover/unicode-input": "~0.1.9",
         "@leanprover/unicode-input-component": "~0.2.0",
         "@vscode/codicons": "^0.0.36",
diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts
index d372769c..8efb02ef 100644
--- a/vscode-lean4/src/leanclient.ts
+++ b/vscode-lean4/src/leanclient.ts
@@ -36,6 +36,7 @@ import {
     LeanFileProgressParams,
     LeanFileProgressProcessingInfo,
     LeanServerCapabilities,
+    RpcWireFormat,
     ServerStoppedReason,
 } from '@leanprover/infoview-api'
 import {
@@ -97,11 +98,13 @@ function logConfig(): LogConfig | undefined {
 }
 
 interface LeanClientCapabilties {
-    silentDiagnosticSupport?: boolean | undefined
+    silentDiagnosticSupport?: boolean
+    rpcWireFormat?: RpcWireFormat
 }
 
 const leanClientCapabilities: LeanClientCapabilties = {
     silentDiagnosticSupport: true,
+    rpcWireFormat: 'v1'
 }
 
 export type PrepareModuleHierarchyResult =
@@ -117,8 +120,6 @@ export type ModuleHierarchyImportedByResult =
     | { kind: 'StoppedClient' }
     | { kind: 'Unsupported' }
 
-const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&')
-
 export type ServerProgress = Map<ExtUri, LeanFileProgressProcessingInfo[]>
 
 export class LeanClient implements Disposable {

From 35ddc9de941ecba44a968cbdb5a782bc28b45f83 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Fri, 13 Mar 2026 16:16:02 -0400
Subject: [PATCH 6/8] chore: undo change

---
 lean4-infoview/src/index.tsx | 1 +
 1 file changed, 1 insertion(+)

diff --git a/lean4-infoview/src/index.tsx b/lean4-infoview/src/index.tsx
index 5c7d1ca9..b0311b11 100644
--- a/lean4-infoview/src/index.tsx
+++ b/lean4-infoview/src/index.tsx
@@ -10,6 +10,7 @@ export { GoalLocation, GoalsLocation, LocationsContext } from './infoview/goalLo
 export { InteractiveCode, InteractiveCodeProps, Markdown } from './infoview/interactiveCode'
 export { renderInfoview } from './infoview/main'
 export { RpcContext, useRpcSession } from './infoview/rpcSessions'
+export { ServerVersion } from './infoview/serverVersion'
 export { DynamicComponent, DynamicComponentProps, importWidgetModule, PanelWidgetProps } from './infoview/userWidget'
 export {
     DocumentPosition,

From e436397fa7a820c7daeb26929fb588dc7ac56fc9 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Fri, 13 Mar 2026 19:45:16 -0400
Subject: [PATCH 7/8] doc: update

---
 lean4-infoview-api/src/rpcSessions.ts | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/lean4-infoview-api/src/rpcSessions.ts b/lean4-infoview-api/src/rpcSessions.ts
index a42f6cc0..6540e941 100644
--- a/lean4-infoview-api/src/rpcSessions.ts
+++ b/lean4-infoview-api/src/rpcSessions.ts
@@ -1,4 +1,9 @@
-import type { DocumentUri, Position, ServerCapabilities, TextDocumentPositionParams } from 'vscode-languageserver-protocol'
+import type {
+    DocumentUri,
+    Position,
+    ServerCapabilities,
+    TextDocumentPositionParams,
+} from 'vscode-languageserver-protocol'
 import { ClientRequestOptions, LeanServerCapabilities } from './infoviewApi'
 import { RpcCallParams, RpcErrorCode, RpcPtr, RpcReleaseParams } from './lspTypes'
 
@@ -134,16 +139,17 @@ 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) {
@@ -251,7 +257,10 @@ export class RpcSessions {
 
     constructor(public iface: RpcServerIface) {}
 
-    private connectCore(uri: DocumentUri, serverCapabilities: ServerCapabilities<LeanServerCapabilities>): 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, serverCapabilities)
         this.sessions.set(uri, sess)
@@ -265,7 +274,10 @@ 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, serverCapabilities: ServerCapabilities<LeanServerCapabilities>): RpcSessionAtPos {
+    connect(
+        pos: TextDocumentPositionParams,
+        serverCapabilities: ServerCapabilities<LeanServerCapabilities>,
+    ): RpcSessionAtPos {
         return this.connectCore(pos.textDocument.uri, serverCapabilities).at(pos.position)
     }
 

From 6956f81143fd86a5cb090dd8adb6f4867430a21d Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Fri, 13 Mar 2026 19:45:36 -0400
Subject: [PATCH 8/8] chore: bump current-release

---
 lean4-infoview-api/package.json |  2 +-
 package-lock.json               | 37 +++++++++++----------------------
 2 files changed, 13 insertions(+), 26 deletions(-)

diff --git a/lean4-infoview-api/package.json b/lean4-infoview-api/package.json
index 6da8d666..1f3cfe9b 100644
--- a/lean4-infoview-api/package.json
+++ b/lean4-infoview-api/package.json
@@ -9,7 +9,7 @@
     "scripts": {
         "watch": "tsc --watch",
         "watchTest": "tsc --watch",
-        "build": "tsc",
+        "build": "tsc --sourceMap false",
         "build:dev": "tsc"
     },
     "main": "dist/index",
diff --git a/package-lock.json b/package-lock.json
index c20a2054..b9827d32 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -75,17 +75,6 @@
                 "vscode-languageserver-protocol": "^3.17.3"
             }
         },
-        "lean4-infoview/node_modules/@vscode/codicons": {
-            "version": "0.0.40",
-            "resolved": "https://registry.npmjs.org/@vscode/codicons/-/codicons-0.0.40.tgz",
-            "integrity": "sha512-R8sEDXthD86JHsk3xERrMcTN6sMovbk1AXYB5/tGoEYCE8DWwya6al5VLrAmQYXC1bQhUHIfHALj8ijQUs11cQ=="
-        },
-        "lean4-infoview/node_modules/es-module-shims": {
-            "version": "2.8.0",
-            "resolved": "https://registry.npmjs.org/es-module-shims/-/es-module-shims-2.8.0.tgz",
-            "integrity": "sha512-7eBj0nIBTMjg8WspPfHOXVxwvDPeYjTMH7PipzrbecfLS4SFwRvWeakZNsAx0y9yF3TydxrG32tj3y+GKzlpYg==",
-            "license": "MIT"
-        },
         "lean4-unicode-input": {
             "name": "@leanprover/unicode-input",
             "version": "0.1.9",
@@ -2939,10 +2928,9 @@
             }
         },
         "node_modules/@vscode/codicons": {
-            "version": "0.0.32",
-            "resolved": "https://registry.npmjs.org/@vscode/codicons/-/codicons-0.0.32.tgz",
-            "integrity": "sha512-3lgSTWhAzzWN/EPURoY4ZDBEA80OPmnaknNujA3qnI4Iu7AONWd9xF3iE4L+4prIe8E3TUnLQ4pxoaFTEEZNwg==",
-            "dev": true,
+            "version": "0.0.40",
+            "resolved": "https://registry.npmjs.org/@vscode/codicons/-/codicons-0.0.40.tgz",
+            "integrity": "sha512-R8sEDXthD86JHsk3xERrMcTN6sMovbk1AXYB5/tGoEYCE8DWwya6al5VLrAmQYXC1bQhUHIfHALj8ijQUs11cQ==",
             "license": "CC-BY-4.0"
         },
         "node_modules/@vscode/test-electron": {
@@ -5389,17 +5377,17 @@
         },
         "node_modules/current-release": {
             "name": "@leanprover/infoview",
-            "version": "0.8.0",
-            "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.8.0.tgz",
-            "integrity": "sha512-KNun6UdMtJbPHXcCL6zq8B/mvOYiqYlfU5W8xYwcJjXCQUZlrOJJRApHgM6GLxy3G0cPD5IYL0kCPUsfXsLA+g==",
+            "version": "0.12.0",
+            "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.12.0.tgz",
+            "integrity": "sha512-4DbTpK1lmqrpPb+kBFdcDW44kbB26NGtvlIzDLozmvbWkoqajlJdo+Fw3paXga0/9GnOP+KuO019n3obeaMDRg==",
             "dev": true,
             "license": "Apache-2.0",
             "dependencies": {
-                "@leanprover/infoview-api": "~0.5.0",
+                "@leanprover/infoview-api": "~0.12.0",
                 "@vscode-elements/react-elements": "^0.5.0",
-                "@vscode/codicons": "^0.0.32",
+                "@vscode/codicons": "^0.0.40",
                 "es-module-lexer": "^1.5.4",
-                "es-module-shims": "^1.7.3",
+                "es-module-shims": "^2.8.0",
                 "react-fast-compare": "^3.2.2",
                 "tachyons": "^4.12.0",
                 "vscode-languageserver-protocol": "^3.17.3"
@@ -6046,10 +6034,9 @@
             "license": "MIT"
         },
         "node_modules/es-module-shims": {
-            "version": "1.10.0",
-            "resolved": "https://registry.npmjs.org/es-module-shims/-/es-module-shims-1.10.0.tgz",
-            "integrity": "sha512-3PmuShQBd9d8pulTFx6L7HKgncnZ1oeSSbrEfnUasb3Tv974BAvyFtW1HLPJSkh5fCaU9JNZbBzPdbxSwg2zqA==",
-            "dev": true,
+            "version": "2.8.0",
+            "resolved": "https://registry.npmjs.org/es-module-shims/-/es-module-shims-2.8.0.tgz",
+            "integrity": "sha512-7eBj0nIBTMjg8WspPfHOXVxwvDPeYjTMH7PipzrbecfLS4SFwRvWeakZNsAx0y9yF3TydxrG32tj3y+GKzlpYg==",
             "license": "MIT"
         },
         "node_modules/es-object-atoms": {