-
Notifications
You must be signed in to change notification settings - Fork 43
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactor: make RPC independent of infoview
- Loading branch information
Showing
15 changed files
with
409 additions
and
509 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,5 @@ | ||
export * from './lspTypes' | ||
export * from './infoviewApi' | ||
export * from './rpcSessions' | ||
export * from './rpcApi' | ||
export * from './util' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,99 @@ | ||
/** | ||
* Defines TS bindings for RPC calls to the Lean server, | ||
* as well as some utilities which correspond to Lean functions. | ||
* TODO(WN): One would like to eventually auto-generate the bindings from Lean code. | ||
* @module | ||
*/ | ||
|
||
import type { LocationLink, TextDocumentPositionParams } from 'vscode-languageserver-protocol' | ||
import { LeanDiagnostic, RpcPtr } from './lspTypes' | ||
import { RpcSession } from './rpcSessions' | ||
|
||
/** A string where certain (possibly nested) substrings have been decorated with objects of type T. */ | ||
export type TaggedText<T> = | ||
{ text: string } | | ||
{ append: TaggedText<T>[] } | | ||
{ tag: [T, TaggedText<T>] } | ||
|
||
export type InfoWithCtx = RpcPtr<'Lean.Widget.InfoWithCtx'> | ||
|
||
export interface SubexprInfo { | ||
info: InfoWithCtx | ||
subexprPos?: number | ||
} | ||
|
||
export type CodeWithInfos = TaggedText<SubexprInfo> | ||
|
||
/** Information that should appear in a popup when clicking on a subexpression. */ | ||
export interface InfoPopup { | ||
type?: CodeWithInfos | ||
exprExplicit?: CodeWithInfos | ||
doc?: string | ||
} | ||
|
||
export interface InteractiveHypothesisBundle { | ||
isInstance?: boolean, | ||
isType?: boolean, | ||
/** The pretty names of the variables in the bundle. | ||
* If the name is inaccessible this will be `"[anonymous]"`. | ||
* Use `InteractiveHypothesis_accessibleNames` to filter these out. | ||
*/ | ||
names: string[] | ||
/** The free variable id associated with each of the vars listed in `names`. */ | ||
fvarIds?: string[] | ||
type: CodeWithInfos | ||
val?: CodeWithInfos | ||
} | ||
|
||
export interface InteractiveGoal { | ||
hyps: InteractiveHypothesisBundle[] | ||
type: CodeWithInfos | ||
userName?: string | ||
goalPrefix?: string | ||
/** metavariable id associated with the goal. | ||
* This is undefined when the goal is a term goal | ||
* or if we are using an older version of lean. */ | ||
mvarId?: string | ||
} | ||
|
||
export interface InteractiveGoals { | ||
goals: InteractiveGoal[] | ||
} | ||
|
||
export function getInteractiveGoals(rs: RpcSession, pos: TextDocumentPositionParams): Promise<InteractiveGoals | undefined> { | ||
return rs.call('Lean.Widget.getInteractiveGoals', pos); | ||
} | ||
|
||
export function getInteractiveTermGoal(rs: RpcSession, pos: TextDocumentPositionParams): Promise<InteractiveGoal | undefined> { | ||
return rs.call('Lean.Widget.getInteractiveTermGoal', pos); | ||
} | ||
|
||
export type MessageData = RpcPtr<'Lean.MessageData'> | ||
export type MsgEmbed = | ||
{ expr: CodeWithInfos } | | ||
{ goal: InteractiveGoal } | | ||
{ lazyTrace: [number, string, MessageData] } | ||
|
||
export type InteractiveDiagnostic = Omit<LeanDiagnostic, 'message'> & { message: TaggedText<MsgEmbed> } | ||
|
||
export interface LineRange { | ||
start: number; | ||
end: number; | ||
} | ||
|
||
export function getInteractiveDiagnostics(rs: RpcSession, lineRange?: LineRange): Promise<InteractiveDiagnostic[]> { | ||
return rs.call('Lean.Widget.getInteractiveDiagnostics', {lineRange}); | ||
} | ||
|
||
export function InteractiveDiagnostics_msgToInteractive(rs: RpcSession, msg: MessageData, indent: number): Promise<TaggedText<MsgEmbed>> { | ||
return rs.call('Lean.Widget.InteractiveDiagnostics.msgToInteractive', {msg, indent}) | ||
} | ||
|
||
export function InteractiveDiagnostics_infoToInteractive(rs: RpcSession, info: InfoWithCtx): Promise<InfoPopup> { | ||
return rs.call('Lean.Widget.InteractiveDiagnostics.infoToInteractive', info); | ||
} | ||
|
||
export type GoToKind = 'declaration' | 'definition' | 'type' | ||
export function getGoToLocation(rs: RpcSession, kind: GoToKind, info: InfoWithCtx): Promise<LocationLink[]> { | ||
return rs.call('Lean.Widget.getGoToLocation', { kind, info }); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,171 @@ | ||
import type { DocumentUri, TextDocumentPositionParams } from 'vscode-languageserver-protocol'; | ||
import { RpcCallParams, RpcErrorCode, RpcPtr, RpcReleaseParams } from './lspTypes'; | ||
|
||
export interface RpcServerIface { | ||
/** | ||
* Creates an RPC session for the given uri and returns the session id. | ||
* The implementation of `RpcServerIface` takes care to send any required | ||
* keepalive notifications. | ||
*/ | ||
createRpcSession(uri: DocumentUri): Promise<string>; | ||
/** Closes an RPC session created with `createRpcSession`. */ | ||
closeRpcSession(sessionId: string): void; | ||
/** Sends an RPC call to the Lean server. */ | ||
call(request: RpcCallParams): Promise<any>; | ||
/** Sends an RPC reference release notification to the server. */ | ||
release(request: RpcReleaseParams): void; | ||
} | ||
|
||
/** | ||
* An RPC session at a specific point in a file. | ||
* The Lean 4 RPC protocol requires every request to specify a position in the | ||
* file; only `@[serverRpcMethod]` declarations above this positions are callable. | ||
* Implementations of this interface bundle the position. | ||
*/ | ||
export interface RpcSession { | ||
call(method: string, params: any): Promise<any>; | ||
} | ||
|
||
class RpcSessionForFile { | ||
sessionId: Promise<string>; | ||
/** | ||
* `failed` stores a fatal exception indicating that the RPC session can no longer be used. | ||
* For example: the worker crashed, etc. | ||
*/ | ||
failed?: any; | ||
|
||
refsToRelease: RpcPtr<any>[] = []; | ||
finalizers: FinalizationRegistry<RpcPtr<any>>; | ||
|
||
constructor(public uri: DocumentUri, public sessions: RpcSessions) { | ||
this.sessionId = (async () => { | ||
try { | ||
return await sessions.iface.createRpcSession(uri); | ||
} catch (ex) { | ||
this.failWithoutClosing(ex); | ||
throw ex; | ||
} | ||
})(); | ||
|
||
// Here we hook into the JS GC and send release-reference notifications | ||
// whenever the GC finalizes a number of `RpcPtr`s. Requires ES2021. | ||
let releaseTimeout: number | undefined | ||
this.finalizers = new FinalizationRegistry(ptr => { | ||
if (this.failed) return; | ||
this.refsToRelease.push(ptr) | ||
|
||
// We release eagerly instead of delaying when this many refs become garbage | ||
const maxBatchSize = 100 | ||
if (this.refsToRelease.length > maxBatchSize) { | ||
void this.releaseNow(); | ||
clearTimeout(releaseTimeout); | ||
releaseTimeout = undefined; | ||
} else if (releaseTimeout === undefined) { | ||
releaseTimeout = setTimeout(() => { | ||
void this.releaseNow() | ||
releaseTimeout = undefined; | ||
}, 100); | ||
} | ||
}); | ||
} | ||
|
||
async releaseNow() { | ||
const sessionId = await this.sessionId; | ||
if (this.failed || this.refsToRelease.length === 0) return; | ||
this.sessions.iface.release({ | ||
uri: this.uri, | ||
sessionId, | ||
refs: this.refsToRelease, | ||
}); | ||
this.refsToRelease = []; | ||
} | ||
|
||
register(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>)); | ||
} else { | ||
for (const v of Object.values(o as {})) this.register(v); | ||
} | ||
} else if (o instanceof Array) { | ||
for (const e of o) this.register(e); | ||
} | ||
} | ||
|
||
private failWithoutClosing(reason: any): void { | ||
this.failed = reason; | ||
this.sessions.sessions.delete(this.uri); | ||
} | ||
|
||
fail(reason: any) { | ||
this.failed = reason; | ||
this.sessions.sessions.delete(this.uri); | ||
void this.sessionId.then((id) => this.sessions.iface.closeRpcSession(id)); | ||
} | ||
|
||
async call(pos: TextDocumentPositionParams, method: string, params: any): Promise<any> { | ||
const sessionId = await this.sessionId; | ||
if (this.failed) throw this.failed; | ||
try { | ||
const result = await this.sessions.iface.call({ method, params, sessionId, ... pos }); | ||
this.register(result); | ||
return result; | ||
} catch (ex: any) { | ||
if (ex?.code === RpcErrorCode.WorkerCrashed || ex?.code === RpcErrorCode.WorkerExited || | ||
ex?.code === RpcErrorCode.RpcNeedsReconnect) { | ||
this.fail(ex); | ||
} | ||
throw ex; | ||
} | ||
} | ||
|
||
at(pos: TextDocumentPositionParams): RpcSession { | ||
return { call: (method, params) => this.call(pos, method, params) }; | ||
} | ||
} | ||
|
||
/** Manages RPC sessions for multiple files. */ | ||
export class RpcSessions { | ||
/** | ||
* Contains the active `RpcSessionForFile` objects. | ||
* Once an `RpcSessionForFile` is set to failed (e.g. due to a server crash), | ||
* it is removed from this map. The `connect` method will then automatically | ||
* reconnect the next time it is called. | ||
*/ | ||
sessions: Map<DocumentUri, RpcSessionForFile> = new Map(); | ||
|
||
constructor(public iface: RpcServerIface) {} | ||
|
||
private connectCore(uri: DocumentUri): RpcSessionForFile { | ||
if (this.sessions.has(uri)) return this.sessions.get(uri) as RpcSessionForFile; | ||
const sess = new RpcSessionForFile(uri, this); | ||
this.sessions.set(uri, sess); | ||
return sess; | ||
} | ||
|
||
/** | ||
* Returns an `RpcSession` for the given position. | ||
* Calling `connect` multiple times will return the same | ||
* session (with the same session ID). | ||
* A new session is only created if a fatal error occurs (i.e., the worker | ||
* crashes) or the session is closed manually (if the file is closed). | ||
*/ | ||
connect(pos: TextDocumentPositionParams): RpcSession { | ||
return this.connectCore(pos.textDocument.uri).at(pos); | ||
} | ||
|
||
/* Closes the session for the given Uri. */ | ||
closeSessionForFile(uri: DocumentUri): void { | ||
void this.sessions.get(uri)?.fail('file closed'); | ||
} | ||
|
||
closeAllSessions(): void { | ||
for (const k of [...this.sessions.keys()]) this.closeSessionForFile(k); | ||
} | ||
|
||
dispose(): void { | ||
this.closeAllSessions(); | ||
} | ||
} | ||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
import { InteractiveHypothesisBundle, TaggedText } from './rpcApi' | ||
|
||
export function TaggedText_stripTags<T>(tt: TaggedText<T>): string { | ||
const go = (t: TaggedText<T>): string => { | ||
if ('append' in t) | ||
return t.append.reduce<string>((acc, t_) => acc + go(t_), '') | ||
else if ('tag' in t) | ||
return go(t.tag[1]) | ||
else if ('text' in t) | ||
return t.text | ||
return '' | ||
} | ||
return go(tt) | ||
} | ||
|
||
/** Filter out inaccessible / anonymous pretty names from the names list. */ | ||
export function InteractiveHypothesisBundle_accessibleNames(ih : InteractiveHypothesisBundle) : string[] { | ||
return ih.names.filter(x => !x.includes('[anonymous]')) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.