diff --git a/lean4-infoview-api/package.json b/lean4-infoview-api/package.json index df9d86d0..1f3cfe9b 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", @@ -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/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/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 = { readonly [tag]: T; p: string } +export type RpcPtr = { readonly [tag]: T; __rpcref: string } | { readonly [tag]: T; p: string } // eslint-disable-next-line @typescript-eslint/no-namespace export namespace RpcPtr { export function copy(p: RpcPtr): RpcPtr { - return { p: p.p } as RpcPtr + if ('p' in p) return { p: p.p } as RpcPtr + else return { __rpcref: p.__rpcref } as RpcPtr } /** Turns a reference into a unique string. Useful for React `key`s. */ export function toKey(p: RpcPtr): 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 1fdbb342..6540e941 100644 --- a/lean4-infoview-api/src/rpcSessions.ts +++ b/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, ) { 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)) + 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)) + 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)) + 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, + ): 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, + ): 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/main.tsx b/lean4-infoview/src/infoview/main.tsx index b7cc2c7b..e5e8f465 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) diff --git a/lean4-infoview/src/infoview/rpcSessions.tsx b/lean4-infoview/src/infoview/rpcSessions.tsx index 798aaeab..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 } from './contexts' +import { CapabilityContext, EditorContext, EnvPosContext } from './contexts' import { DocumentPosition, useClientNotificationEffect, useEvent } from './util' const RpcSessionsContext = React.createContext(undefined) @@ -46,20 +46,20 @@ export function WithRpcSessions({ children }: { children: React.ReactNode }) { return {children} } -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(noCtxRpcSession) +export const RpcContext = React.createContext(errorRpcSession('no RPC context set')) /** * Retrieve an RPC session at {@link EnvPosContext}, @@ -82,8 +82,13 @@ export const RpcContext = React.createContext(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) } diff --git a/lean4-infoview/src/infoview/serverVersion.ts b/lean4-infoview/src/infoview/serverVersion.ts index 5007a675..3d56bff5 100644 --- a/lean4-infoview/src/infoview/serverVersion.ts +++ b/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) + } } diff --git a/package-lock.json b/package-lock.json index e21264cb..b9827d32 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,24 +68,13 @@ }, "lean4-infoview-api": { "name": "@leanprover/infoview-api", - "version": "0.11.0", + "version": "0.12.0", "license": "Apache-2.0", "devDependencies": { "typescript": "^5.4.5", "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": { @@ -16218,8 +16205,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 export class LeanClient implements Disposable {