From 7dbd9f6193c594a5c4ff8e4864bd3081ab3d2ff1 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 26 Apr 2024 18:12:22 -0700 Subject: [PATCH] Use standard LSP requests. --- client/src/extension.ts | 354 ++++--------------- client/src/fstarLspExtensions.ts | 1 + server/src/client_connection.ts | 113 ------ server/src/fstar.ts | 11 +- server/src/fstarLspExtensions.ts | 48 +++ server/src/fstar_connection.ts | 11 +- server/src/fstar_messages.ts | 19 +- server/src/main.ts | 7 +- server/src/server.ts | 590 +++++++++++++++---------------- server/src/signals.ts | 77 ++++ server/src/utils.ts | 8 + 11 files changed, 531 insertions(+), 708 deletions(-) create mode 120000 client/src/fstarLspExtensions.ts delete mode 100644 server/src/client_connection.ts create mode 100644 server/src/fstarLspExtensions.ts create mode 100644 server/src/signals.ts diff --git a/client/src/extension.ts b/client/src/extension.ts index ed190bc..d94ace9 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -7,12 +7,14 @@ import * as path from 'path'; import { workspace, ExtensionContext, Command } from 'vscode'; import * as vscode from 'vscode'; import { - DiagnosticRelatedInformation, LanguageClient, LanguageClientOptions, ServerOptions, - TransportKind + TransportKind, + Range, + Position } from 'vscode-languageclient/node'; +import { StatusNotificationParams, killAllNotification, killAndRestartSolverNotification, restartNotification, statusNotification, verifyToPositionNotification } from './fstarLspExtensions'; let client: LanguageClient; @@ -69,226 +71,64 @@ const proofInProgressDecorationMap : Map = new Map = new Map(); -// Diagnostics raised by the server for each document -interface DocDiagnostics { - lax_diagnostics: vscode.Diagnostic []; - full_diagnostics: vscode.Diagnostic []; -} -const diagnosticsMap : Map = new Map(); -const diagnosticCollection = vscode.languages.createDiagnosticCollection('fstar-vscode-assistant'); - // A background color for text being verified: Not currently used const inProgressBackground = vscode.window.createTextEditorDecorationType({ backgroundColor: 'rgba(100, 0, 255, 0.5)' }); - -// Messags in the small protocol running on top of LSP between the server and client -type ok_kind = 'checked' | 'light-checked'; -interface StatusOkMessage { - uri: string; - ok_kind: ok_kind; - ranges: vscode.Range []; -} - -interface StatusFailedMessage { - uri: string; - ranges: vscode.Range []; -} - -interface StatusClearMessage { - uri: string; -} - -interface StatusStartedMessage { - uri: string; - ranges: vscode.Range []; -} - -interface StatusInProgressMessage { - uri: string; - ranges: vscode.Range []; -} - -interface AlertMessage { - uri: string; - message: string; -} - -interface DiagnosticsMessage { - uri: string; - lax: boolean; - diagnostics: vscode.Diagnostic []; -} - -interface ClearDiagnosticsMessage { - uri: string; -} - -// This function is called when the active editor changes or when a status message is received -// We set the gutter decorations for the document in the new active editor -// if the URI matches the URI of the document in the new active editor -function setActiveEditorDecorationsIfUriMatches(uri: string) { - const editor = vscode.window.activeTextEditor; - if (!editor) { return; } - if (editor.document.uri.toString() === uri) { - //it important to set it in this order since they get overwritten - // First, show the started (...) icons for all the lines where the proof has been launched, - // but only on the suffix of the buffer where the proof has not been completed - // Then, show the hourglass icons for all the lines where the proof is currently running progress - // Then, show the green line icons for all the lines where the proof has succeeded - // Or, show the blue line for all the lines where the proof has lax succeeded - const started = proofStartedDecorationMap.get(uri) ?? []; - const maxCheckLine = Math.max(...(gutterOkDecorationsMap.get(uri) ?? []).map(range => range.end.line)); - const maxLightCheckLine = Math.max(...(gutterLaxDecorationsMap.get(uri) ?? []).map(range => range.end.line)); - const checkLine = Math.max(maxCheckLine, maxLightCheckLine); - const startedIcons : vscode.Range[] = []; - started.forEach(startedRange => { - if (startedRange.end.line > checkLine) { - // find the first line from checkLine + 1 that has some text on it - let startedLine = checkLine + 1; - while (startedLine < startedRange.end.line) { - const lineText = editor.document.lineAt(startedLine).text; - if (lineText.trim().length > 0) { - break; - } - startedLine++; - } - if (startedLine < startedRange.end.line) { - startedIcons.push(new vscode.Range(startedLine, 0, startedRange.end.line, 0)); - } - }}); - editor.setDecorations(gutterIconStarted, startedIcons); - editor.setDecorations(gutterIconHourglass, proofInProgressDecorationMap.get(uri) ?? []); - editor.setDecorations(gutterIconOk, gutterOkDecorationsMap.get(uri) ?? []); - if (fstarVSCodeAssistantSettings.showLightCheckIcon) { - editor.setDecorations(gutterIconLax, gutterLaxDecorationsMap.get(uri) ?? []); +function posToCode(range: Position): vscode.Position { + return new vscode.Position(range.line, range.character); +} + +function rangeToCode(range: Range): vscode.Range { + return new vscode.Range(posToCode(range.start), posToCode(range.end)); +} + +function handleStatus(params: StatusNotificationParams) { + const started: vscode.Range[] = []; + const inProgress: vscode.Range[] = []; + const ok: vscode.Range[] = []; + const lax: vscode.Range[] = []; + + for (const frag of params.fragments) { + const r = rangeToCode(frag.range); + switch (frag.kind) { + case 'ok': + ok.push(r); break; + case 'failed': + case 'light-failed': + break; + case 'lax-ok': + case 'light-ok': + lax.push(r); break; + case 'in-progress': + inProgress.push(r); break; + case 'started': + started.push(r); break; } - // Here's how you would set a background color for a region of text - // editor.setDecorations(inProgressBackground, backgroundColorDecorationMap.get(uri) ?? []); - } -} - -// This function is called when the server sends a statusOk message -// We add the ranges to the map of gutter decorations for the file -// clearing any hourglass decorations -// and set the decorations for the active editor if the URI matches -function handleStatusOk (msg : StatusOkMessage) { - if (msg.ok_kind == "light-checked") { - const currentDecorations : vscode.Range [] = gutterLaxDecorationsMap.get(msg.uri) ?? []; - msg.ranges.forEach (range => { - currentDecorations.push(range); - }); - gutterLaxDecorationsMap.set(msg.uri, currentDecorations); } - else { - const currentDecorations : vscode.Range [] = gutterOkDecorationsMap.get(msg.uri) ?? []; - msg.ranges.forEach (range => { - currentDecorations.push(range); - }); - gutterOkDecorationsMap.set(msg.uri, currentDecorations); - } - // clear hourglasses - proofInProgressDecorationMap.set(msg.uri, []); - setActiveEditorDecorationsIfUriMatches(msg.uri); -} - -// This function is called when the server decided that a chunk has failed verification -// Clear any hourglass and started decorations -function handleStatusFailed (msg : StatusFailedMessage) { - proofInProgressDecorationMap.set(msg.uri, []); - proofStartedDecorationMap.set(msg.uri, []); - setActiveEditorDecorationsIfUriMatches(msg.uri); -} - -// This function is called when the server sends a statusStarted message -// We record the ranges in the proofStartedDecorationMap -// and display the started on those lines -function handleStatusStarted (msg: StatusStartedMessage): void { - // console.log("Received statusClear notification: " +msg); - proofStartedDecorationMap.set(msg.uri, msg.ranges); - setActiveEditorDecorationsIfUriMatches(msg.uri); -} - -// This function is called when the server sends a statusInProgress message -// We record the ranges in the proofInProgressDecorationMap -// and display the hourglass on those lines -function handleStatusInProgress (msg: StatusInProgressMessage): void { - // console.log("Received statusClear notification: " +msg); - proofInProgressDecorationMap.set(msg.uri, msg.ranges); - setActiveEditorDecorationsIfUriMatches(msg.uri); -} - -// This function is called when the server sends a statusClear message -// We clear the gutter decorations for the file -function handleStatusClear (msg: StatusClearMessage): void { - // console.log("Received statusClear notification: " +msg); - gutterOkDecorationsMap.set(msg.uri, []); - gutterLaxDecorationsMap.set(msg.uri, []); - proofStartedDecorationMap.set(msg.uri, []); - proofInProgressDecorationMap.set(msg.uri, []); - diagnosticsMap.set(msg.uri, { lax_diagnostics: [], full_diagnostics: [] }); - const uri = vscode.Uri.parse(msg.uri); - diagnosticCollection.set(uri, []); - setActiveEditorDecorationsIfUriMatches(msg.uri); -} -// This function is called by the server in case F* crashed or was killed -async function handleAlert(msg: AlertMessage) { - await vscode.window.showErrorMessage(msg.message + "\n On document: " + msg.uri); -} + const uri = params.uri; + proofStartedDecorationMap.set(uri, started); + gutterLaxDecorationsMap.set(uri, lax); + gutterOkDecorationsMap.set(uri, ok); + proofInProgressDecorationMap.set(uri, inProgress); -function handleDiagnostics(msg: DiagnosticsMessage) { - const docDiagnostics : DocDiagnostics = - diagnosticsMap.get(msg.uri) ?? { lax_diagnostics: [], full_diagnostics: [] }; - msg.diagnostics.forEach(element => { - if (element.relatedInformation) { - element.relatedInformation.forEach (ri => { - ri.location.uri = vscode.Uri.parse(ri.location.uri.toString()); - }); - } - }); - if (msg.lax) { - docDiagnostics.lax_diagnostics = msg.diagnostics; + if (vscode.window.visibleTextEditors.some(ed => ed.document.uri.toString() === params.uri)) { + updateDecorations(); } - else { - docDiagnostics.full_diagnostics = msg.diagnostics; - } - diagnosticsMap.set(msg.uri, docDiagnostics); - const all_diags = docDiagnostics.lax_diagnostics.concat([]); - function rangeEquals(r1: vscode.Range, r2: vscode.Range) { - return ( - r1.start.line == r2.start.line && - r1.start.character == r2.start.character && - r1.end.line == r2.end.line && r1.end.character == r2.end.character - ); - } - function docContainsDiagnostic(diag: vscode.Diagnostic) { - return all_diags.some(d => rangeEquals(d.range, diag.range) && d.message === diag.message); - } - // De-duplicate diagnostics, because we may get diagnostics from multiple sources - // both the fstar_ide and fstar_lax_ide servers may send diagnostics - docDiagnostics.full_diagnostics.forEach(diag => { - if (!docContainsDiagnostic(diag)) { - all_diags.push(diag); - } - }); - const uri = vscode.Uri.parse(msg.uri); - diagnosticCollection.set(uri, all_diags); -} - -function handleClearDiagnostics(msg : ClearDiagnosticsMessage) { - diagnosticsMap.set(msg.uri, { lax_diagnostics: [], full_diagnostics: [] }); - const uri = vscode.Uri.parse(msg.uri); - diagnosticCollection.set(uri, []); } -// A client-only handler for a active editor changed raised by the editor -// We set the gutter decorations for the document in the new active editor -function handleDidChangeActiveEditor(editor? : vscode.TextEditor) { - if (!editor) return; - // console.log("Active editor changed to " + editor.document.uri.toString()); - setActiveEditorDecorationsIfUriMatches(editor.document.uri.toString()); +function updateDecorations() { + for (const editor of vscode.window.visibleTextEditors) { + const uri = editor.document.uri.toString(); + editor.setDecorations(gutterIconStarted, proofStartedDecorationMap.get(uri) ?? []); + editor.setDecorations(gutterIconHourglass, proofInProgressDecorationMap.get(uri) ?? []); + editor.setDecorations(gutterIconOk, gutterOkDecorationsMap.get(uri) ?? []); + editor.setDecorations(gutterIconLax, + fstarVSCodeAssistantSettings.showLightCheckIcon ? + gutterLaxDecorationsMap.get(uri) ?? [] : []); + } } export async function activate(context: ExtensionContext) { @@ -311,10 +151,7 @@ export async function activate(context: ExtensionContext) { const clientOptions: LanguageClientOptions = { // Register the server for plain text documents documentSelector: [{ scheme: 'file', language: 'fstar'}], - synchronize: { - // Notify the server about file changes to '.clientrc files contained in the workspace - fileEvents: workspace.createFileSystemWatcher('**/.clientrc') - } + diagnosticCollectionName: 'fstar', }; // Create the language client and start the client. @@ -325,73 +162,33 @@ export async function activate(context: ExtensionContext) { clientOptions ); - client.onNotification('fstar-vscode-assistant/statusOk', handleStatusOk); - client.onNotification('fstar-vscode-assistant/statusClear', handleStatusClear); - client.onNotification('fstar-vscode-assistant/statusStarted', handleStatusStarted); - client.onNotification('fstar-vscode-assistant/statusInProgress', handleStatusInProgress); - client.onNotification('fstar-vscode-assistant/statusFailed', handleStatusFailed); - client.onNotification('fstar-vscode-assistant/alert', handleAlert); - client.onNotification('fstar-vscode-assistant/diagnostics', handleDiagnostics); - client.onNotification('fstar-vscode-assistant/clearDiagnostics', handleClearDiagnostics); - vscode.window.onDidChangeActiveTextEditor(handleDidChangeActiveEditor); + client.onNotification(statusNotification, status => handleStatus(status)); + vscode.window.onDidChangeVisibleTextEditors(() => updateDecorations()); // register a command for Ctrl+. - const verifyCommand = vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/verify-to-position', async (textEditor, edit) => { - // console.log('Client: Command executed with uri: ' + textEditor.document.uri + " at positon " + textEditor.selection.active.line + ", " + textEditor.selection.active.character); - await client.sendRequest('fstar-vscode-assistant/verify-to-position', [textEditor.document.uri.toString(), textEditor.selection.active]); - }); - context.subscriptions.push(verifyCommand); + context.subscriptions.push(vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/verify-to-position', textEditor => + client.sendNotification(verifyToPositionNotification, { + uri: textEditor.document.uri.toString(), + lax: false, + position: textEditor.selection.active, + }))); - // register a command for Ctrl+;,Ctrl+. - const reloadAndVerifyCommand = vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/restart', async (textEditor, edit) => { - // console.log('Client: Command executed with uri: ' + textEditor.document.uri); - await client.sendRequest('fstar-vscode-assistant/restart', textEditor.document.uri.toString()); - }); - context.subscriptions.push(reloadAndVerifyCommand); + context.subscriptions.push(vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/restart', textEditor => + client.sendNotification(restartNotification, { uri: textEditor.document.uri.toString() }))); // register a command for Ctrl+Shift+. - const laxVerifyCommand = vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/lax-to-position', async (textEditor, edit) => { - // console.log('Client: Command executed with uri: ' + textEditor.document.uri + " at positon " + textEditor.selection.active.line + ", " + textEditor.selection.active.character); - await client.sendRequest('fstar-vscode-assistant/lax-to-position', [textEditor.document.uri.toString(), textEditor.selection.active]); - }); - context.subscriptions.push(laxVerifyCommand); - - const killAndRestartSolverCommand = - vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/kill-and-restart-solver', async (textEditor, edit) => { - await client.sendRequest('fstar-vscode-assistant/kill-and-restart-solver', [textEditor.document.uri.toString()]); - }); - context.subscriptions.push(killAndRestartSolverCommand); + context.subscriptions.push(vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/lax-to-position', textEditor => + client.sendNotification(verifyToPositionNotification, { + uri: textEditor.document.uri.toString(), + lax: true, + position: textEditor.selection.active, + }))); + + context.subscriptions.push(vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/kill-and-restart-solver', textEditor => + client.sendNotification(killAndRestartSolverNotification, { uri: textEditor.document.uri.toString() }))); - const killAllCommand = - vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/kill-all', async (textEditor, edit) => { - await client.sendRequest('fstar-vscode-assistant/kill-all', []); - }); - context.subscriptions.push(killAllCommand); - - // console.log("Activate called on " + context.asAbsolutePath("/")); - - workspace.onDidChangeTextDocument(async (event) => { - // console.log("OnDidChangeTextDocument"); - const textDoc = event.document; - let minRange : vscode.Range | undefined; - function compareRange (a? : vscode.Range, b? : vscode.Range) : number { - if (!a) { return -1; } - if (!b) { return 1; } - if (a.start.line < b.start.line) return -1; - if (a.start.line > b.start.line) return 1; - if (a.start.character < b.start.character) return -1; - if (a.start.character > b.start.character) return 1; - return 0; - } - event.contentChanges.forEach((change) => { - if (compareRange(minRange, change.range) < 0) { - minRange = change.range; - } - }); - if (minRange) { - await client.sendRequest('fstar-vscode-assistant/text-doc-changed', [textDoc.uri.toString(), minRange]); - } - }); + context.subscriptions.push(vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/kill-all', () => + client.sendNotification(killAllNotification, {}))); workspace.onDidChangeConfiguration((event) => { const cfg = workspace.getConfiguration('fstarVSCodeAssistant'); @@ -407,9 +204,6 @@ export async function activate(context: ExtensionContext) { await client.start(); } -export function deactivate(): Thenable | undefined { - if (!client) { - return undefined; - } - return client.stop(); +export async function deactivate() { + await client?.stop(); } diff --git a/client/src/fstarLspExtensions.ts b/client/src/fstarLspExtensions.ts new file mode 120000 index 0000000..5d8fbf8 --- /dev/null +++ b/client/src/fstarLspExtensions.ts @@ -0,0 +1 @@ +../../server/src/fstarLspExtensions.ts \ No newline at end of file diff --git a/server/src/client_connection.ts b/server/src/client_connection.ts deleted file mode 100644 index d19b3a4..0000000 --- a/server/src/client_connection.ts +++ /dev/null @@ -1,113 +0,0 @@ -import { - createConnection, - Diagnostic, - ProposedFeatures, - Range, - _Connection -} from 'vscode-languageserver/node'; - -//////////////////////////////////////////////////////////////////////////////////// -// Custom client/server protocol -//////////////////////////////////////////////////////////////////////////////////// -/** - * A `ClientConnection` is a connection between the LSP server and client (e.g. the - * vscode extension). - */ -export class ClientConnection { - conn: _Connection; - - constructor() { - // Create a connection for the server, using Node's IPC as a transport. - // Also include all preview / proposed LSP features. - this.conn = createConnection(ProposedFeatures.all); - } - - sendStatusStarted(msg: StatusStartedMessage) { - void this.conn.sendNotification('fstar-vscode-assistant/statusStarted', msg); - } - - sendStatusInProgress(msg: StatusInProgressMessage) { - void this.conn.sendNotification('fstar-vscode-assistant/statusInProgress', msg); - } - - sendStatusOk(msg: StatusOkMessage) { - void this.conn.sendNotification('fstar-vscode-assistant/statusOk', msg); - } - - sendStatusFailed(msg: StatusFailedMessage) { - void this.conn.sendNotification('fstar-vscode-assistant/statusFailed', msg); - } - - sendStatusClear(msg: StatusClearMessage) { - void this.conn.sendNotification('fstar-vscode-assistant/statusClear', msg); - } - - sendAlert(msg: AlertMessage) { - void this.conn.sendNotification('fstar-vscode-assistant/alert', msg); - } - - sendDiagnostics(msg: DiagnosticsMessage) { - void this.conn.sendNotification('fstar-vscode-assistant/diagnostics', msg); - } - - sendClearDiagnostics(msg: ClearDiagnosticsMessage) { - void this.conn.sendNotification('fstar-vscode-assistant/clearDiagnostics', msg); - } -} - - -//////////////////////////////////////////////////////////////////////////////////// -// Messages in a small custom protocol between this server and the client -// (running on top of LSP) -//////////////////////////////////////////////////////////////////////////////////// - -// TODO(klinvill): These message interfaces should be refactored out of the client and server components into a shared library so they both use the same definitions. - -// A message to clear all gutter icons for the document with the given URI -export interface StatusClearMessage { - uri: string; -} - -// A message to set the chevron icons for the prefix of the buffer that has been started -export interface StatusStartedMessage { - uri: string; - ranges: Range[]; // A VSCode range, not an FStarRange -} - -// A message to set hourglass icons for the current chunk being verified -export interface StatusInProgressMessage { - uri: string; - ranges: Range[]; // A VSCode range, not an FStarRange -} - -// A message to dislay various line gutter icons for the document of the given URI -// at the given ranges -export type ok_kind = 'checked' | 'light-checked'; -export interface StatusOkMessage { - uri: string; - ok_kind: ok_kind; - ranges: Range[]; // A VSCode range, not an FStarRange -} - -// A message to clear hourglass gutter icons for the document of the given URI -// at the given ranges -export interface StatusFailedMessage { - uri: string; - ranges: Range[]; // A VSCode range, not an FStarRange -} - -// An alert message for a document, sent if the the F* process crashed -export interface AlertMessage { - uri: string; - message: string; -} - -export interface DiagnosticsMessage { - uri: string; - lax: boolean; - diagnostics: Diagnostic[]; -} - -export interface ClearDiagnosticsMessage { - uri: string; -} diff --git a/server/src/fstar.ts b/server/src/fstar.ts index 9ca0519..7c2d319 100644 --- a/server/src/fstar.ts +++ b/server/src/fstar.ts @@ -1,5 +1,6 @@ import { WorkspaceFolder, + Connection, } from 'vscode-languageserver/node'; import { @@ -14,7 +15,6 @@ import * as path from 'path'; import * as util from 'util'; import { fstarVSCodeAssistantSettings } from './settings'; -import { ClientConnection } from './client_connection'; import { checkFileInDirectory, findFilesByExtension, getEnclosingDirectories } from './utils'; // FStar executable @@ -85,7 +85,7 @@ export class FStar { // Dynamically loads the FStarConfiguration for a given file `textDocument` // before attempting to launch an instance of F*. - static async fromInferredConfig(filePath: string, workspaceFolders: WorkspaceFolder[], connection: ClientConnection, + static async fromInferredConfig(filePath: string, workspaceFolders: WorkspaceFolder[], connection: Connection, configurationSettings: fstarVSCodeAssistantSettings, lax?: 'lax'): Promise { const config = await this.getFStarConfig(filePath, workspaceFolders, connection, configurationSettings); return this.trySpawnFstar(config, filePath, configurationSettings.debug, lax); @@ -105,7 +105,7 @@ export class FStar { }); } - static async parseConfigFile(filePath: string, configFile: string, connection: ClientConnection, configurationSettings: fstarVSCodeAssistantSettings): Promise { + static async parseConfigFile(filePath: string, configFile: string, connection: Connection, configurationSettings: fstarVSCodeAssistantSettings): Promise { const contents = await util.promisify(fs.readFile)(configFile, 'utf8'); function substituteEnvVars(value: string) { return value.replace(/\$([A-Z_]+[A-Z0-9_]*)|\${([A-Z0-9_]*)}/ig, @@ -115,7 +115,8 @@ export class FStar { return resolved_env_var; } else { - connection.sendAlert({ message: "Failed to resolve environment variable " + (a || b), uri: URI.file(filePath).toString() }); + connection.window.showErrorMessage( + `Failed to resolve environment variable ${a || b} for file ${filePath}`); return ""; } }); @@ -206,7 +207,7 @@ export class FStar { // 1. An *.fst.config.json file in a parent directory inside the current workspace // 2. The output printed by `make My.File.fst-in` // 3. A default configuration - static async getFStarConfig(filePath: string, workspaceFolders: WorkspaceFolder[], connection: ClientConnection, configurationSettings: fstarVSCodeAssistantSettings): Promise { + static async getFStarConfig(filePath: string, workspaceFolders: WorkspaceFolder[], connection: Connection, configurationSettings: fstarVSCodeAssistantSettings): Promise { // 1. Config file const configFilepath = await this.findConfigFile(filePath, workspaceFolders, configurationSettings); if (configFilepath) { diff --git a/server/src/fstarLspExtensions.ts b/server/src/fstarLspExtensions.ts new file mode 100644 index 0000000..8bf7dff --- /dev/null +++ b/server/src/fstarLspExtensions.ts @@ -0,0 +1,48 @@ +import { ProtocolNotificationType, Position, Range } from 'vscode-languageserver-protocol'; + +export type StatusKind + = 'ok' + | 'lax-ok' + | 'light-ok' + | 'in-progress' + | 'failed' + | 'light-failed' + | 'started'; + +export interface FragmentStatus { + kind: StatusKind; + range: Range; +} + +export interface StatusNotificationParams { + uri: string; + fragments: FragmentStatus[]; +} +export const statusNotification = + new ProtocolNotificationType('$/fstar/status'); + +export interface RestartParams { + uri: string; +} +export const restartNotification = + new ProtocolNotificationType('$/fstar/restart'); + +export interface KillAndRestartSolverParams { + uri: string; +} +export const killAndRestartSolverNotification = + new ProtocolNotificationType('$/fstar/killAndRestartSolver'); + +export interface KillAllParams {} +export const killAllNotification = + new ProtocolNotificationType('$/fstar/killAll'); + +export interface VerifyToPositionParams { + uri: string; + position: Position; + lax: boolean; +} +export const verifyToPositionNotification = + new ProtocolNotificationType('$/fstar/verifyToPosition'); + +interface RegistrationParams {} \ No newline at end of file diff --git a/server/src/fstar_connection.ts b/server/src/fstar_connection.ts index ffd2f0e..9a74847 100644 --- a/server/src/fstar_connection.ts +++ b/server/src/fstar_connection.ts @@ -37,7 +37,7 @@ export class FStarConnection { bufferedFBR?: FullBufferQuery; }; - onFullBufferResponse: (msg: any) => void = _ => {}; + onFullBufferResponse: (msg: any, query: FullBufferQuery) => void = _ => {}; constructor(private fstar: FStar, public debug: boolean) { // TODO(klinvill): Should try to spawn F* from within this constructor @@ -198,7 +198,7 @@ export class FStarConnection { } // Send a request to F* to check the given code up through a position. - partialBufferRequest(code: string, kind: 'verify-to-position' | 'lax-to-position', position: { line: number, column: number }) { + partialBufferRequest(code: string, kind: 'verify-to-position' | 'lax-to-position', position: FStarPosition) { this.fullBufferQuery({ query: "full-buffer", args: { @@ -207,7 +207,10 @@ export class FStarConnection { code: code, line: 0, column: 0, - "to-position": position + "to-position": { + line: position[0], + column: position[1], + }, } }); } @@ -306,7 +309,7 @@ export class FStarConnection { private handleFBQResponse(msg: any) { const done = msg?.kind === 'message' && msg?.level === 'progress' && msg?.contents?.stage === 'full-buffer-finished'; - this.onFullBufferResponse(msg); + this.onFullBufferResponse(msg, this.fullBufferInProgress!.currentReq); if (done) { const old = this.fullBufferInProgress!; this.fullBufferInProgress = undefined; diff --git a/server/src/fstar_messages.ts b/server/src/fstar_messages.ts index 0286ba3..5178857 100644 --- a/server/src/fstar_messages.ts +++ b/server/src/fstar_messages.ts @@ -93,16 +93,19 @@ export interface IdeCodeFragment { range: FStarRange; } -export interface IdeProgress { - stage: 'full-buffer-started' - | 'full-buffer-fragment-started' - | 'full-buffer-fragment-ok' - | 'full-buffer-fragment-lax-ok' - | 'full-buffer-fragment-failed' - | 'full-buffer-finished'; +export interface IdeProgressStartEnd { + stage: 'full-buffer-started' | 'full-buffer-finished'; +} +export interface IdeProgressFragment { + stage: 'full-buffer-fragment-started' | 'full-buffer-fragment-failed'; + ranges: FStarRange; +} +export interface IdeProgressFragmentCheck { + stage: 'full-buffer-fragment-ok' | 'full-buffer-fragment-lax-ok'; ranges: FStarRange; - "code-fragment"?: IdeCodeFragment + "code-fragment": IdeCodeFragment } +export type IdeProgress = IdeProgressStartEnd | IdeProgressFragment | IdeProgressFragmentCheck; // An auto-complete response diff --git a/server/src/main.ts b/server/src/main.ts index d269f91..dea49df 100644 --- a/server/src/main.ts +++ b/server/src/main.ts @@ -3,21 +3,22 @@ * Licensed under the MIT License. See License.txt in the project root for license information. * ------------------------------------------------------------------------------------------ */ import { - TextDocuments + ProposedFeatures, + TextDocuments, + createConnection, } from 'vscode-languageserver/node'; import { TextDocument } from 'vscode-languageserver-textdocument'; -import { ClientConnection } from './client_connection'; import { Server } from './server'; // Make unhandled rejections non-fatal process.on('unhandledRejection', error => console.log('Unhandled rejection:', error)); // Connection between the LSP server and client (e.g. the extension) -const connection = new ClientConnection(); +const connection = createConnection(ProposedFeatures.all); // Simple text document manager. const documents = new TextDocuments(TextDocument); diff --git a/server/src/server.ts b/server/src/server.ts index 32f032d..fb121bf 100644 --- a/server/src/server.ts +++ b/server/src/server.ts @@ -16,9 +16,8 @@ import { LocationLink, DocumentRangeFormattingParams, TextEdit, - _Connection, + Connection, DiagnosticSeverity, - DiagnosticRelatedInformation } from 'vscode-languageserver/node'; import { @@ -30,22 +29,22 @@ import { } from 'vscode-uri'; import * as cp from 'child_process'; -import * as crypto from 'crypto'; import { defaultSettings, fstarVSCodeAssistantSettings } from './settings'; -import { formatIdeProofState, fstarRangeAsRange, mkPosition, rangeAsFStarRange } from './utils'; -import { ClientConnection, StatusOkMessage, ok_kind } from './client_connection'; +import { formatIdeProofState, fstarPosLe, fstarRangeAsRange, mkPosition, posAsFStarPos, posLe, rangeAsFStarRange } from './utils'; import { FStarConnection } from './fstar_connection'; import { FStar, FStarConfig } from './fstar'; -import { FStarRange, IdeProofState, IdeProgress, IdeDiagnostic, FullBufferQueryResponse, FStarPosition } from './fstar_messages'; +import { FStarRange, IdeProofState, IdeProgress, IdeDiagnostic, FullBufferQueryResponse, FStarPosition, FullBufferQuery } from './fstar_messages'; import * as path from 'path'; import { pathToFileURL } from 'url'; +import { statusNotification, FragmentStatus, killAndRestartSolverNotification, restartNotification, verifyToPositionNotification, killAllNotification } from './fstarLspExtensions'; +import { Debouncer, RateLimiter } from './signals'; // LSP Server // // The LSP Server interfaces with both the Client (e.g. the vscode extension) // and the F* processes that are used to check files. It is started run using -// the `server.run()` method. The `ClientConnection` and text document manager +// the `server.run()` method. The `Connection` and text document manager // are passed in as arguments, following the dependency injection pattern. This // allows for easier mocking out of these connections which in turn allows for // easier testing. @@ -57,14 +56,14 @@ export class Server { workspaceFolders: WorkspaceFolder[] = []; configurationSettings: fstarVSCodeAssistantSettings = defaultSettings; // Connection to the client (the extension in the IDE) - connection: ClientConnection; + connection: Connection; // Client (e.g. extension) capabilities hasConfigurationCapability: boolean = false; hasWorkspaceFolderCapability: boolean = false; hasDiagnosticRelatedInformationCapability: boolean = false; - constructor(connection: ClientConnection, documents: TextDocuments) { + constructor(connection: Connection, documents: TextDocuments) { this.documents = documents; this.connection = connection; @@ -74,27 +73,15 @@ export class Server { // * set event handlers to read the output of the fstar processes // * send the current document to both processes to start typechecking this.documents.onDidOpen(ev => - this.onOpenHandler(ev.document).catch(err => - this.connection.sendAlert({ - uri: ev.document.uri, - message: err.toString(), - }))); + this.onOpenHandler(ev.document) + .catch(err => this.connection.window.showErrorMessage( + `${URI.parse(ev.document.uri).fsPath}: ${err.toString()}`)) + .catch()); // Only keep settings for open documents this.documents.onDidClose(e => { this.documentStates.get(e.document.uri)?.dispose(); this.documentStates.delete(e.document.uri); - // Clear all diagnostics for a document when it is closed - this.connection.sendDiagnostics({ - uri: e.document.uri, - lax: true, - diagnostics: [] - }); - this.connection.sendDiagnostics({ - uri: e.document.uri, - lax: false, - diagnostics: [] - }); }); // The content of a text document has changed. This event is emitted @@ -117,62 +104,54 @@ export class Server { // https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Operators/thiscallbacks // for the official documentation on this behavior, and // https://javascript.info/bind for another explanation. - this.connection.conn.onInitialize(params => this.onInitialize(params)); - this.connection.conn.onInitialized(() => this.onInitializedHandler()); + this.connection.onInitialize(params => this.onInitialize(params)); + this.connection.onInitialized(() => this.onInitializedHandler()); // We don't do anything special when the configuration changes - this.connection.conn.onDidChangeConfiguration(async _change => { - await this.updateConfigurationSettings(); - }); - this.connection.conn.onDidChangeWatchedFiles(_change => { - // Monitored files have change in VSCode - // connection.console.log('We received an file change event'); - }); - this.connection.conn.onCompletion(textDocumentPosition => + this.connection.onDidChangeConfiguration(() => this.updateConfigurationSettings()); + this.connection.onCompletion(textDocumentPosition => this.getDocumentState(textDocumentPosition.textDocument.uri)?.onCompletion(textDocumentPosition)); // This handler resolves additional information for the item selected in // the completion list. - this.connection.conn.onCompletionResolve(item => item); - this.connection.conn.onHover(textDocumentPosition => + this.connection.onCompletionResolve(item => item); + this.connection.onHover(textDocumentPosition => this.getDocumentState(textDocumentPosition.textDocument.uri)?.onHover(textDocumentPosition)); - this.connection.conn.onDefinition(defParams => + this.connection.onDefinition(defParams => this.getDocumentState(defParams.textDocument.uri)?.onDefinition(defParams)); - this.connection.conn.onDocumentRangeFormatting(formatParams => + this.connection.onDocumentRangeFormatting(formatParams => this.getDocumentState(formatParams.textDocument.uri)?.onDocumentRangeFormatting(formatParams)); // Custom events - this.connection.conn.onRequest("fstar-vscode-assistant/verify-to-position", params => - this.getDocumentState(params[0])?.onVerifyToPositionRequest(params)); - this.connection.conn.onRequest("fstar-vscode-assistant/lax-to-position", params => - this.getDocumentState(params[0])?.onLaxToPositionRequest(params)); - this.connection.conn.onRequest("fstar-vscode-assistant/restart", uri => + this.connection.onNotification(verifyToPositionNotification, ({uri, position, lax}) => { + const state = this.getDocumentState(uri); + if (lax) { + state?.laxToPosition(position); + } else { + state?.verifyToPosition(position); + } + }); + this.connection.onNotification(restartNotification, ({uri}) => this.onRestartRequest(uri)); - this.connection.conn.onRequest("fstar-vscode-assistant/text-doc-changed", params => - this.getDocumentState(params[0])?.onTextDocChanged(params)); - this.connection.conn.onRequest("fstar-vscode-assistant/kill-and-restart-solver", uri => + this.connection.onNotification(killAndRestartSolverNotification, ({uri}) => this.getDocumentState(uri)?.killAndRestartSolver()); - this.connection.conn.onRequest("fstar-vscode-assistant/kill-all", params => + this.connection.onNotification(killAllNotification, () => this.onKillAllRequest()); } run() { // Make the text document manager listen on the connection // for open, change and close text document events - this.documents.listen(this.connection.conn); + this.documents.listen(this.connection); // Listen on the connection - this.connection.conn.listen(); + this.connection.listen(); } getDocumentState(uri: string): DocumentState | undefined { return this.documentStates.get(uri); } - getDocument(uri: string): TextDocument | undefined { - return this.documents.get(uri); - } - async updateConfigurationSettings() { - const settings = await this.connection.conn.workspace.getConfiguration('fstarVSCodeAssistant'); + const settings = await this.connection.workspace.getConfiguration('fstarVSCodeAssistant'); if (settings.debug) { console.log("Server got settings: " + JSON.stringify(settings)); } @@ -195,7 +174,7 @@ export class Server { const fstar = FStarConnection.tryCreateFStarConnection(fstar_config, filePath, this.configurationSettings.debug); if (!fstar) return; const fstar_lax = this.configurationSettings.flyCheck ? FStarConnection.tryCreateFStarConnection(fstar_config, filePath, this.configurationSettings.debug, 'lax') : undefined; - + const docState = new DocumentState(doc, fstar_config, this, fstar, fstar_lax); this.documentStates.set(uri, docState); } @@ -255,17 +234,17 @@ export class Server { await this.updateConfigurationSettings(); if (this.hasConfigurationCapability) { // Register for all configuration changes. - await this.connection.conn.client.register(DidChangeConfigurationNotification.type, undefined); + await this.connection.client.register(DidChangeConfigurationNotification.type, undefined); // const settings = connection.workspace.getConfiguration('fstarVSCodeAssistant'); // const settings = connection.workspace.getConfiguration(); // console.log("Server got settings: " + JSON.stringify(settings)); } if (this.hasWorkspaceFolderCapability) { - this.connection.conn.workspace.onDidChangeWorkspaceFolders(_event => { + this.connection.workspace.onDidChangeWorkspaceFolders(_event => { // We don't do anything special when workspace folders change // We should probably reset the workspace configs and re-read the .fst.config.json files if (this.configurationSettings.debug) { - this.connection.conn.console.log('Workspace folder change event received.'); + this.connection.console.log('Workspace folder change event received.'); } }); } @@ -287,13 +266,10 @@ export class Server { docState.fstar_lax?.validateFStarDocument('lax'); } - private async onRestartRequest(uri: any) { - // console.log("Received restart request with parameters: " + uri); - const textDocument = this.getDocument(uri); - if (!textDocument) return; + private async onRestartRequest(uri: string) { + if (!this.documents.get(uri)) return; this.documentStates.get(uri)?.dispose(); this.documentStates.delete(uri); - this.connection.sendStatusClear({ uri: textDocument.uri }); await this.refreshDocumentState(uri); // And ask the lax fstar process to verify it this.getDocumentState(uri)?.fstar_lax?.validateFStarDocument('lax'); @@ -341,19 +317,32 @@ export class DocumentState { // If flycheck is disabled, then we don't spawn the second process and this field is undefined. fstar_lax?: DocumentProcess; + private disposed = false; + constructor(currentDoc: TextDocument, public fstarConfig: FStarConfig, public server: Server, fstar: FStarConnection, fstar_lax?: FStarConnection) { this.uri = currentDoc.uri; - this.fstar = new DocumentProcess(currentDoc, fstarConfig, server, false, fstar); - this.fstar_lax = fstar_lax && new DocumentProcess(currentDoc, fstarConfig, server, true, fstar_lax); + this.fstar = new DocumentProcess(currentDoc, fstarConfig, this, false, fstar); + this.fstar_lax = fstar_lax && new DocumentProcess(currentDoc, fstarConfig, this, true, fstar_lax); } dispose() { + this.disposed = true; this.fstar.dispose(); this.fstar_lax?.dispose(); + + // Clear all diagnostics for a document when it is closed + void this.server.connection.sendDiagnostics({ + uri: this.uri, + diagnostics: [], + }); + void this.server.connection.sendNotification(statusNotification, { + uri: this.uri, + fragments: [], + }); } changeDoc(newDoc: TextDocument) { @@ -372,12 +361,12 @@ export class DocumentState { } verifyToPosition(position: Position) { - this.fstar.validateFStarDocumentToPosition('verify-to-position', { line: position.line + 1, column: position.character }); + this.fstar.validateFStarDocumentToPosition('verify-to-position', position); this.fstar_lax?.validateFStarDocument('lax'); } laxToPosition(position: Position) { - this.fstar.validateFStarDocumentToPosition('lax-to-position', { line: position.line + 1, column: position.character }); + this.fstar.validateFStarDocumentToPosition('lax-to-position', position); this.fstar_lax?.validateFStarDocument('lax'); } @@ -400,62 +389,127 @@ export class DocumentState { return (this.fstar_lax ?? this.fstar).onDocumentRangeFormatting(formatParams); } - onVerifyToPositionRequest(params: any) { - const position: { line: number, character: number } = params[1]; - this.verifyToPosition(position); - } - - onLaxToPositionRequest(params: any) { - const position: { line: number, character: number } = params[1]; - this.laxToPosition(position); - } - - onTextDocChanged(params: any) { - const range: { line: number; character: number }[] = params[1]; - // TODO(klinvill): It looks like this function can only be called for - // non-lax checking. Is that correct? - const fstarPos: FStarPosition = [range[0].line + 1, range[0].character]; - this.fstar?.fstar?.cancelFBQ(fstarPos); - this.fstar_lax?.fstar?.cancelFBQ(fstarPos); - } - async killAndRestartSolver() { // TODO(klinvill): It looks like this function only restarts the // standard F* solver (not the lax one), is this the desired behavior? return this.fstar?.killAndRestartSolver(); } + + sendDiags() { this.diagnosticsRateLimiter.fire(); } + diagnosticsRateLimiter = new RateLimiter(100, () => { + if (this.disposed) return; + + const diags = + [...this.fstar.results.diagnostics, ...this.fstar.results.outOfBandErrors]; + + if (this.fstar_lax) { + // Add diagnostics from the lax position that are after the part processed by the full process. + const lastPos = mkPosition(this.fstar.results.fragments.at(-1)?.range?.end || [1, 1]); + diags.push(...this.fstar_lax.results.diagnostics.filter(d => posLe(lastPos, d.range.start))); + } + + void this.server.connection.sendDiagnostics({ + uri: this.uri, + diagnostics: diags, + }); + }); + + sendStatus() { this.statusRateLimiter.fire(); } + private statusRateLimiter = new RateLimiter(100, () => { + if (this.disposed) return; + + const fragments = [...this.fstar.results.fragments]; + + // TODO: augment with lax process status + + const statusFragments: FragmentStatus[] = []; + for (const frag of fragments) { + statusFragments.push({ + range: fstarRangeAsRange(frag.range), + kind: + frag.ok === undefined ? 'in-progress' : + !frag.ok ? 'failed' : + frag.lax ? 'lax-ok' : 'ok', + }); + } + + const lastPos = mkPosition(this.fstar.results.fragments.at(-1)?.range?.end ?? [1, 0]); + if (this.fstar.startedProcessingToPosition) { + statusFragments.push({ + range: { start: lastPos, end: this.fstar.startedProcessingToPosition }, + kind: 'started', + }); + } + + void this.server.connection.sendNotification(statusNotification, { + uri: this.uri, + fragments: statusFragments, + }); + }); } function isDummyRange(range: FStarRange): boolean { return range.fname === 'dummy'; } +interface FragmentResult { + range: FStarRange; + ok?: boolean; + lax?: boolean; +} + +interface DocumentResults { + fragments: FragmentResult[]; + diagnostics: Diagnostic[]; + proofStates: IdeProofState[]; + outOfBandErrors: Diagnostic[]; +} +function emptyResults(): DocumentResults { + return { + fragments: [], + diagnostics: [], + proofStates: [], + outOfBandErrors: [], + }; +} + +function findFirstDiffPos(a: string, b: string): undefined | number { + let i = 0; + while (i < a.length && i < b.length && a[i] === b[i]) i++; + return i === a.length && i === b.length ? undefined : i; +} + export class DocumentProcess { uri: string; filePath: string; - fstar_diagnostics: Diagnostic[] = []; + // Diagnostics, proof states, ranges of checked fragments, etc. + results: DocumentResults = emptyResults(); + // Full-buffer queries start out by "replaying" diagnostics from already checked fragments. + // During this phase we buffer these in newResults to avoid flickering. + // We switch the buffers when the first fragment is being processed. + private newResults?: DocumentResults; + // When a full-buffer query is in progress, startedProcessingToPosition contains the end-position + startedProcessingToPosition?: Position; - // A proof-state table populated by fstar_ide when running tactics, displayed in onHover - hover_proofstate_info: Map = new Map(); - // A flag to indicate if the prefix of the buffer is stale - prefix_stale: boolean = false; - // We don't want to send too many requests to fstar.exe, so we batch them up // and send only the most recent one. - lastPendingChange?: TextDocument; - changeDispatcher?: NodeJS.Timeout; + // currentDoc is always the current editor document (it is updated in place!) + pendingChange: boolean = false; + lastDocumentSentToFStar: string; constructor(public currentDoc: TextDocument, public fstarConfig: FStarConfig, - public server: Server, + public documentState: DocumentState, public lax: boolean, public fstar: FStarConnection) { this.uri = currentDoc.uri; this.filePath = URI.parse(this.uri).fsPath; - fstar.onFullBufferResponse = res => this.handleSingleFullBufferResponse(res); + this.lastDocumentSentToFStar = currentDoc.getText(); + + fstar.onFullBufferResponse = (res, q) => this.handleSingleFullBufferResponse(res, q); // Send the initial dummy vfs-add request to the fstar processes. fstar.vfsAddRequest(this.filePath, currentDoc.getText()) @@ -464,38 +518,37 @@ export class DocumentProcess { dispose() { this.fstar.close(); - clearTimeout(this.changeDispatcher); + this.changeDispatcher.cancel(); } - get connection() { return this.server.connection; } - + private changeDispatcher = new Debouncer(200, () => { + if (!this.pendingChange) return; + this.validateFStarDocument(this.lax ? 'lax' : 'cache'); + }); changeDoc(newDoc: TextDocument) { - clearTimeout(this.changeDispatcher); - this.lastPendingChange = newDoc; - this.changeDispatcher = setTimeout(() => { - if (!this.lastPendingChange) return; - this.validateFStarDocument(this.lax ? 'lax' : 'cache'); - }, 200); + this.currentDoc = newDoc; + this.changeDispatcher.fire(); + + const diffOff = findFirstDiffPos(this.currentDoc.getText(), this.lastDocumentSentToFStar); + if (diffOff) { + const diffPos = this.currentDoc.positionAt(diffOff); + this.fstar.cancelFBQ(posAsFStarPos(diffPos)); + if (this.startedProcessingToPosition && posLe(diffPos, this.startedProcessingToPosition)) { + this.startedProcessingToPosition = diffPos; + } + } } // Lookup the proof state table for the line at the cursor findIdeProofStateAtLine(position: Position) { - const rangeKey = position.line + 1; - return this.hover_proofstate_info.get(rangeKey); - } - - clearIdeProofProofStateAtRange(range: FStarRange) { - const line_ctr = range.beg[0]; - const end_line_ctr = range.end[0]; - for (let i = line_ctr; i <= end_line_ctr; i++) { - this.hover_proofstate_info.delete(i); - } + const fstarPos = posAsFStarPos(position); + return this.results.proofStates.find((ps) => ps.location.beg[0] === fstarPos[0]); } private applyPendingChange() { - if (this.lastPendingChange) { - this.currentDoc = this.lastPendingChange; - this.lastPendingChange = undefined; + if (this.pendingChange) { + this.pendingChange = false; + this.lastDocumentSentToFStar = this.currentDoc.getText(); } } @@ -504,41 +557,19 @@ export class DocumentProcess { // Clear pending change events, since we're checking it now this.applyPendingChange(); - this.connection.sendClearDiagnostics({ uri: this.uri }); - - if (!this.lax) { - // If this is non-lax requests, send a status clear messages to VSCode - // to clear the gutter icons and error squiggles - // They will be reported again if the document is not verified - this.prefix_stale = false; - this.connection.sendStatusClear({ uri: this.uri }); - const ranges = [Range.create(mkPosition([0, 0]), mkPosition([this.currentDoc.lineCount, 0]))]; - if (kind == "full") { this.connection.sendStatusStarted({ uri: this.uri, ranges: ranges }); } - } - this.fstar.fullBufferRequest(this.currentDoc.getText(), kind, false); } - validateFStarDocumentToPosition(kind: 'verify-to-position' | 'lax-to-position', position: { line: number, column: number }) { + validateFStarDocumentToPosition(kind: 'verify-to-position' | 'lax-to-position', position: Position) { // Clear pending change events, since we're checking it now this.applyPendingChange(); - // console.log("ValidateFStarDocumentToPosition( " + textDocument.uri + ", " + kind); - this.connection.sendClearDiagnostics({ uri: this.uri }); - // If this is non-lax requests, send a status clear messages to VSCode - // to clear the gutter icons and error squiggles - // They will be reported again if the document is not verified - this.prefix_stale = false; - this.connection.sendStatusClear({ uri: this.uri }); - const ranges = [Range.create(mkPosition([0, 0]), mkPosition([position.line, 0]))]; - this.connection.sendStatusStarted({ uri: this.uri, ranges: ranges }); - - this.fstar.partialBufferRequest(this.currentDoc.getText(), kind, position); + this.fstar.partialBufferRequest(this.currentDoc.getText(), kind, posAsFStarPos(position)); } - private handleSingleFullBufferResponse(response: FullBufferQueryResponse) { + private handleSingleFullBufferResponse(response: FullBufferQueryResponse, query: FullBufferQuery) { if (response.kind === 'message' && response.level === 'progress') { - this.handleIdeProgress(response.contents as IdeProgress); + this.handleIdeProgress(response.contents as IdeProgress, query); } else if (response.kind === 'message' && response.level === 'info') { console.info("Info: " + response.contents); } else if (response.kind === 'message' && response.level === 'error') { @@ -550,13 +581,13 @@ export class DocumentProcess { // that show the lines that caused F* to emit a warning. console.warn("Warning: " + response.contents); } else if (response.kind === 'message' && response.level === 'proof-state') { - this.handleIdeProofState(response.contents as IdeProofState); + this.handleIdeProofState(response.contents); } else if (response.kind === 'response') { // TODO(klinvill): if a full-buffer query is interrupted, a null response seems to be sent along with a status. Is this always the behavior that occurs? if (!response.response) { console.info("Query cancelled"); } else if (Array.isArray(response.response)) { - this.handleIdeDiagnostics(response.response as IdeDiagnostic[]); + this.handleIdeDiagnostics(response.response); } else { // ignore } @@ -581,99 +612,104 @@ export class DocumentProcess { return textdocUri; } - // If we get a proof state dump message, we store it in the proof state map private handleIdeProofState(response: IdeProofState) { - // console.log("Got ide proof state " + JSON.stringify(response)); - const range_key = response.location.beg[0]; - const hoverProofStateMap = this.hover_proofstate_info; - if (hoverProofStateMap) { - // console.log("Setting proof state hover info at line: " +range_key); - hoverProofStateMap.set(range_key, response); + if (this.newResults) { + console.error('received proof state before full-buffer-fragmented-started'); } + this.results.proofStates.push(response); } - // If a declaration in a full-buffer is verified, fstar_ide sends - // us first a full-buffer-fragment-started message - // We send a status-ok to the client which will - // and show an hourglass icon in the gutter for those locations - // - // Then we may get a full-buffer-fragment-ok message. - // - // We use that to send a status-ok which will clear the hourglass icon - // and show a checkmark in the gutter for the locations we send - private handleIdeProgress(contents: IdeProgress) { - if (contents.stage == "full-buffer-started") { - this.fstar_diagnostics = []; + private handleIdeProgress(contents: IdeProgress, query: FullBufferQuery) { + if (contents.stage === 'full-buffer-started') { + if (query.args['to-position']) { + const {line, column} = query.args['to-position']; + this.startedProcessingToPosition = mkPosition([line, column]); + } else { + // FIXME: this can be out of date + this.startedProcessingToPosition = this.currentDoc.positionAt(this.currentDoc.getText().length); + } + + this.newResults = emptyResults(); return; } - if (contents.stage == "full-buffer-finished") { - this.connection.sendDiagnostics({ - uri: this.uri, - lax: this.lax, - diagnostics: this.fstar_diagnostics - }); + + if (contents.stage === 'full-buffer-finished') { + if (this.newResults) { + // No fragments were processed. + this.newResults.outOfBandErrors = this.results.outOfBandErrors; + this.newResults.proofStates = this.results.proofStates; + this.results = this.newResults; + this.newResults = undefined; + } else { + // When cancelling an FBQ, F* sends a full-buffer-fragment-started for the last fragment but no full-buffer-fragment-ok + const lastFrag = this.results.fragments.at(-1); + if (lastFrag && lastFrag.ok === undefined) { + this.results.fragments.pop(); + } + } + this.startedProcessingToPosition = undefined; + + this.documentState.sendStatus(); + this.documentState.sendDiags(); return; } - if (this.lax) { return; } - // We don't send intermediate diagnostics and gutter icons for flycheck progress - if (contents.stage == "full-buffer-fragment-ok" || - contents.stage == "full-buffer-fragment-lax-ok") { - if (this.prefix_stale) { return; } - const rng = contents.ranges; - if (!contents["code-fragment"]) { return; } - const code_fragment = contents["code-fragment"]; - const currentText = this.currentDoc.getText(fstarRangeAsRange(code_fragment.range)); - // compute an MD5 digest of currentText.trim - const md5 = crypto.createHash('md5'); - md5.update(currentText.trim()); - const digest = md5.digest('hex'); - if (digest != code_fragment['code-digest']) { - if (this.server.configurationSettings.debug) { - console.log("Not setting gutter ok icon: Digest mismatch at range " + JSON.stringify(rng)); - } - this.prefix_stale = true; - return; + + if (contents.stage === 'full-buffer-fragment-started') { + if (this.newResults) { + // This is the first fragment the server actually processes, + // the previous ones were cached and did not generate proof state infos. + + // So let's preserve those infos from previously. + const rng = fstarRangeAsRange(contents.ranges); + this.newResults.outOfBandErrors.push(...this.results.outOfBandErrors.filter(d => posLe(d.range.end, rng.start))); + this.newResults.proofStates.push(...this.results.proofStates.filter(s => fstarPosLe(s.location.end, contents.ranges.beg))); + + this.results = this.newResults; + this.newResults = undefined; } - const ok_range = Range.create(mkPosition(rng.beg), mkPosition(rng.end)); - let ok_kind: ok_kind; - if (contents.stage == "full-buffer-fragment-lax-ok") { ok_kind = "light-checked"; } - else { ok_kind = "checked"; } - const msg: StatusOkMessage = { - uri: this.uri, - ok_kind: ok_kind, - ranges: [ok_range] - }; - this.connection.sendStatusOk(msg); + + this.results.fragments.push({ + range: contents.ranges, + }); + + this.documentState.sendStatus(); + return; } - if (contents.stage == "full-buffer-fragment-started") { - const rng = contents.ranges; - const ok_range = Range.create(mkPosition(rng.beg), mkPosition(rng.end)); - const msg = { - uri: this.uri, - ranges: [ok_range] - }; - this.connection.sendStatusInProgress(msg); - //If there's any proof state for the range that's starting - //clear it, because we'll get updates from fstar_ide - this.clearIdeProofProofStateAtRange(rng); + if (contents.stage === 'full-buffer-fragment-ok' || contents.stage === 'full-buffer-fragment-lax-ok') { + const ok = true; + const lax = contents.stage !== 'full-buffer-fragment-ok'; + + if (this.newResults) { + // This is a cached result. + this.newResults.fragments.push({ ok, lax, range: contents.ranges }); + return; + } + + const frag = this.results.fragments.at(-1)!; + frag.ok = ok; + frag.lax = lax; + + this.documentState.sendStatus(); + return; } - if (contents.stage == "full-buffer-fragment-failed") { - const rng = contents.ranges; - const ok_range = Range.create(mkPosition(rng.beg), mkPosition(rng.end)); - const msg = { - uri: this.uri, - ranges: [ok_range] - }; - this.connection.sendStatusFailed(msg); + if (contents.stage === 'full-buffer-fragment-failed') { + if (this.newResults) { + console.error('full-buffer-fragment-failed without fill-buffer-fragment-started'); + return; + } + + const frag = this.results.fragments.at(-1)!; + frag.ok = false; + + this.documentState.sendStatus(); + return; } } - // If we get errors and warnings from F*, we send them to VSCode as diagnostics, - // which will show them as squiggles in the editor. - private handleIdeDiagnostics(response: IdeDiagnostic[]) { + ideDiagAsDiag(diag: IdeDiagnostic): Diagnostic { function ideErrorLevelAsDiagnosticSeverity(level: string): DiagnosticSeverity { switch (level) { case "warning": return DiagnosticSeverity.Warning; @@ -682,74 +718,41 @@ export class DocumentProcess { default: return DiagnosticSeverity.Error; } } - if (!response || !(Array.isArray(response))) { - this.connection.sendAlert({ message: "Got invalid response to ide diagnostics request: " + JSON.stringify(response), uri: this.uri }); - return; + + const defPos: Position = {line: 0, character: 0}; + const defRange: Range = {start: defPos, end: defPos}; + + const ranges = [...diag.ranges]; + let mainRange = defRange; + + // Use the first range as the range of the diagnostic if it is in the current file, + // provide the rest as related info. + // Note: this seems to be wrong for pulse. https://github.com/FStarLang/pulse/issues/36 + if (ranges.length > 0 && ranges[0].fname === '') { + mainRange = fstarRangeAsRange(ranges.shift()!); } - const diagnostics: Diagnostic[] = []; - response.forEach((err) => { - let diag: Diagnostic | undefined = undefined; - let shouldAlertErrorInDifferentFile = false; - err.ranges.forEach((rng) => { - if (!diag) { - // First range for this error, construct the diagnostic message. - let mainRange; - const relatedInfo = []; - if (rng.fname != "") { - // This is a diagnostic raised on another file - shouldAlertErrorInDifferentFile = err.level == "error"; - const defaultRange: FStarRange = { - fname: "", - beg: [1, 0], - end: [1, 0] - }; - mainRange = defaultRange; - const relationLocation = { - uri: this.qualifyFilename(rng.fname, this.uri), - range: fstarRangeAsRange(rng) - }; - const ri: DiagnosticRelatedInformation = { - location: relationLocation, - message: "related location" - }; - relatedInfo.push(ri); - } - else { - mainRange = rng; - } - diag = { - severity: ideErrorLevelAsDiagnosticSeverity(err.level), - range: fstarRangeAsRange(mainRange), - message: err.message, - relatedInformation: relatedInfo - }; - } else if (diag) { - const relatedLocation = { - uri: this.qualifyFilename(rng.fname, this.uri), - range: fstarRangeAsRange(rng) - }; - const relatedInfo: DiagnosticRelatedInformation = { - location: relatedLocation, - message: "related location" - }; - if (diag.relatedInformation) { - diag.relatedInformation.push(relatedInfo); - } - } - }); - if (shouldAlertErrorInDifferentFile) { - this.connection.sendAlert({ message: err.message, uri: this.uri }); - } - if (diag) { - diagnostics.push(diag); - } - }); - this.fstar_diagnostics = this.fstar_diagnostics.concat(diagnostics); + + return { + message: diag.message, + severity: ideErrorLevelAsDiagnosticSeverity(diag.level), + range: mainRange, + relatedInformation: ranges.map(rng => ({ + location: { + uri: this.qualifyFilename(rng.fname, this.uri), + range: fstarRangeAsRange(rng), + }, + message: 'related location', + })), + }; + } + + private handleIdeDiagnostics(response: IdeDiagnostic[]) { + (this.newResults ?? this.results).diagnostics.push(...response.map(diag => this.ideDiagAsDiag(diag))); + this.documentState.sendDiags(); } async onCompletion(textDocumentPosition: TextDocumentPositionParams): Promise { - const doc = this.lastPendingChange ?? this.currentDoc; - const word = findWordAtPosition(doc, textDocumentPosition.position); + const word = findWordAtPosition(this.currentDoc, textDocumentPosition.position); if (word.word.length < 2) return; const response = await this.fstar.autocompleteRequest(word.word); if (response.status !== 'success') return; @@ -769,7 +772,6 @@ export class DocumentProcess { } async onHover(textDocumentPosition: TextDocumentPositionParams): Promise { - const textDoc = this.lastPendingChange ?? this.currentDoc; // First, check if we have proof state information for this line const proofState = this.findIdeProofStateAtLine(textDocumentPosition.position); if (proofState) { @@ -781,7 +783,7 @@ export class DocumentProcess { }; } // Otherwise, check the symbol information for this symbol - const word = findWordAtPosition(textDoc, textDocumentPosition.position); + const word = findWordAtPosition(this.currentDoc, textDocumentPosition.position); // The filename '' here must be exactly the same the we used in the full buffer request. const result = await this.fstar.lookupQuery('', textDocumentPosition.position, word.word); if (result.status !== 'success') return; @@ -809,8 +811,7 @@ export class DocumentProcess { // It's very similar to the onHover handler, except that it returns a // LocationLink object instead of a Hover object async onDefinition(defParams: DefinitionParams): Promise { - const textDoc = this.lastPendingChange ?? this.currentDoc; - const word = findWordAtPosition(textDoc, defParams.position); + const word = findWordAtPosition(this.currentDoc, defParams.position); // The filename '' here must be exactly the same the we used in the full buffer request. const result = await this.fstar.lookupQuery('', defParams.position, word.word); if (result.status !== 'success') return []; @@ -823,14 +824,14 @@ export class DocumentProcess { } const range = fstarRangeAsRange(defined_at); return [{ - targetUri: this.qualifyFilename(defined_at.fname, textDoc.uri), + targetUri: this.qualifyFilename(defined_at.fname, this.currentDoc.uri), targetRange: range, targetSelectionRange: range, }]; } else if (result.response.kind === 'module') { const range: Range = {start: {line: 0, character: 0}, end: {line: 0, character: 0}}; return [{ - targetUri: this.qualifyFilename(result.response.path, textDoc.uri), + targetUri: this.qualifyFilename(result.response.path, this.currentDoc.uri), targetRange: range, targetSelectionRange: range, }]; @@ -838,8 +839,7 @@ export class DocumentProcess { } async onDocumentRangeFormatting(formatParams: DocumentRangeFormattingParams) { - const textDoc = this.lastPendingChange ?? this.currentDoc; - const text = textDoc.getText(formatParams.range); + const text = this.currentDoc.getText(formatParams.range); // call fstar.exe synchronously to format the text const format_query = { "query-id": "1", diff --git a/server/src/signals.ts b/server/src/signals.ts new file mode 100644 index 0000000..5b84394 --- /dev/null +++ b/server/src/signals.ts @@ -0,0 +1,77 @@ +/** +Generic interface for a signal processor. + +Input signals are received by calling `fire()`. +The transformed output signal is sent via the `handler()` callback (which is set by the user). +*/ +export interface SignalProc { + fire(): void; + handler: () => void; +} + +/** +Debounces a signal with a settling time of `millis` milliseconds. + +``` +Input: xx x x x x +Output: x +``` + +- The handler is called at most once every `millis` milliseconds. +- If an input is received, then the handler will be called after that, eventually. +- We wait `millis` milliseconds after the last input before calling the handler. +*/ +export class Debouncer implements SignalProc { + constructor(public millis: number, public handler = () => {}) {} + + private timeout?: NodeJS.Timeout; + + cancel() { + if (this.timeout) { + clearTimeout(this.timeout); + this.timeout = undefined; + } + } + + fire() { + this.cancel(); + this.timeout = setTimeout(() => { + this.timeout = undefined; + this.handler(); + }, this.millis); + } +} + +/** +Rate-limits a signal to an interval of `millis` milliseconds. + +``` +Input: xx x x x x +Output: x x x x +``` + +- The handler is called at most once every `millis` milliseconds. +- If an input is received, then the handler will be called after at most `millis` milliseconds. +*/ +export class RateLimiter implements SignalProc { + constructor(public millis: number, public handler = () => {}) {} + + private missedFire = false; + private timeout?: NodeJS.Timeout; + + fire() { + if (this.timeout) { + this.missedFire = true; + } else { + this.timeout = setTimeout(() => { + this.timeout = undefined; + if (this.missedFire) { + this.missedFire = false; + this.handler(); + } + }, this.millis); + // Run async + setTimeout(() => this.handler()); + } + } +} \ No newline at end of file diff --git a/server/src/utils.ts b/server/src/utils.ts index d848d10..0eaa054 100644 --- a/server/src/utils.ts +++ b/server/src/utils.ts @@ -34,6 +34,14 @@ export function rangeAsFStarRange(rng: Range): FStarRange { }; } +export function fstarPosLe(a: FStarPosition, b: FStarPosition) { + return a[0] < b[0] || (a[0] === b[0] && a[1] <= b[1]); +} + +export function posLe(a: Position, b: Position) { + return a.line < b.line || (a.line === b.line && a.character <= b.character); +} + //////////////////////////////////////////////////////////////////////////////////// // PATH and URI Utilities