diff --git a/client/src/extension.ts b/client/src/extension.ts index ed190bc..15184aa 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, statusNotification } from './fstarExtensions'; let client: LanguageClient; @@ -69,168 +71,70 @@ 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 []; +function posToCode(range: Position): vscode.Position { + return new vscode.Position(range.line, range.character); } -interface ClearDiagnosticsMessage { - uri: string; +function rangeToCode(range: Range): vscode.Range { + return new vscode.Range(posToCode(range.start), posToCode(range.end)); } -// 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 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); -} + const uri = params.uri; + proofStartedDecorationMap.set(uri, started); + gutterLaxDecorationsMap.set(uri, lax); + gutterOkDecorationsMap.set(uri, ok); + proofInProgressDecorationMap.set(uri, inProgress); -// 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); + if (vscode.window.visibleTextEditors.some(ed => ed.document.uri.toString() === params.uri)) { + updateDecorations(); + } } -// 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); +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) ?? [] : []); + } } // This function is called by the server in case F* crashed or was killed @@ -238,59 +142,6 @@ async function handleAlert(msg: AlertMessage) { await vscode.window.showErrorMessage(msg.message + "\n On document: " + msg.uri); } -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; - } - 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()); -} - export async function activate(context: ExtensionContext) { // The server is implemented in node const serverModule = context.asAbsolutePath( @@ -311,10 +162,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,15 +173,9 @@ 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(statusNotification, status => handleStatus(status)); 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); + vscode.window.onDidChangeVisibleTextEditors(() => updateDecorations()); // register a command for Ctrl+. const verifyCommand = vscode.commands.registerTextEditorCommand('fstar-vscode-assistant/verify-to-position', async (textEditor, edit) => { diff --git a/client/src/fstarExtensions.ts b/client/src/fstarExtensions.ts new file mode 120000 index 0000000..5e05407 --- /dev/null +++ b/client/src/fstarExtensions.ts @@ -0,0 +1 @@ +../../server/src/fstarExtensions.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..1a82871 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/fstarExtensions.ts b/server/src/fstarExtensions.ts new file mode 100644 index 0000000..9d34f1b --- /dev/null +++ b/server/src/fstarExtensions.ts @@ -0,0 +1,25 @@ +import { ProtocolNotificationType, 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: ProtocolNotificationType = + new ProtocolNotificationType('$/fstar/status'); + +interface RegistrationParams {} \ No newline at end of file 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..36c17d1 100644 --- a/server/src/server.ts +++ b/server/src/server.ts @@ -18,7 +18,6 @@ import { TextEdit, _Connection, DiagnosticSeverity, - DiagnosticRelatedInformation } from 'vscode-languageserver/node'; import { @@ -30,22 +29,21 @@ 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, fstarRangeAsRange, mkPosition, posAsFStarPos, rangeAsFStarRange } from './utils'; import { FStarConnection } from './fstar_connection'; import { FStar, FStarConfig } from './fstar'; import { FStarRange, IdeProofState, IdeProgress, IdeDiagnostic, FullBufferQueryResponse, FStarPosition } from './fstar_messages'; import * as path from 'path'; import { pathToFileURL } from 'url'; +import { statusNotification, FragmentStatus } from './fstarExtensions'; // 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 +55,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; @@ -75,26 +73,13 @@ export class Server { // * 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.connection.window.showErrorMessage( + `${URI.parse(ev.document.uri).fsPath}: ${err.toString()}`))); // 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,50 +102,50 @@ 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 => { + this.connection.onDidChangeConfiguration(async _change => { await this.updateConfigurationSettings(); }); - this.connection.conn.onDidChangeWatchedFiles(_change => { + this.connection.onDidChangeWatchedFiles(_change => { // Monitored files have change in VSCode // connection.console.log('We received an file change event'); }); - this.connection.conn.onCompletion(textDocumentPosition => + 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.connection.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.connection.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.onRequest("fstar-vscode-assistant/restart", uri => this.onRestartRequest(uri)); - this.connection.conn.onRequest("fstar-vscode-assistant/text-doc-changed", params => + this.connection.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.onRequest("fstar-vscode-assistant/kill-and-restart-solver", uri => this.getDocumentState(uri)?.killAndRestartSolver()); - this.connection.conn.onRequest("fstar-vscode-assistant/kill-all", params => + this.connection.onRequest("fstar-vscode-assistant/kill-all", params => 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 { @@ -172,7 +157,7 @@ export class Server { } 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)); } @@ -255,17 +240,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.'); } }); } @@ -293,7 +278,6 @@ export class Server { if (!textDocument) 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 +325,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 + this.server.connection.sendDiagnostics({ + uri: this.uri, + diagnostics: [], + }); + void this.server.connection.sendNotification(statusNotification, { + uri: this.uri, + fragments: [], + }); } changeDoc(newDoc: TextDocument) { @@ -424,20 +421,90 @@ export class DocumentState { // standard F* solver (not the lax one), is this the desired behavior? return this.fstar?.killAndRestartSolver(); } + + sendDiags() { + 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: Position = + 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))); + } + + this.server.connection.sendDiagnostics({ + uri: this.uri, + diagnostics: diags, + }); + } + + sendStatus() { + 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', + }); + } + + this.server.connection.sendNotification(statusNotification, { + uri: this.uri, + fragments: statusFragments, + }); + } } function isDummyRange(range: FStarRange): boolean { return range.fname === 'dummy'; } +function fstarPosLe(a: FStarPosition, b: FStarPosition) { + return a[0] < b[0] || (a[0] === b[0] && a[1] <= b[1]); +} + +function posLe(a: Position, b: Position) { + return a.line < b.line || (a.line === b.line && a.character <= b.character); +} + +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: [], + }; +} + export class DocumentProcess { uri: string; filePath: string; - fstar_diagnostics: Diagnostic[] = []; + results: DocumentResults = emptyResults(); + private newResults?: DocumentResults; - // 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; @@ -448,7 +515,7 @@ export class DocumentProcess { constructor(public currentDoc: TextDocument, public fstarConfig: FStarConfig, - public server: Server, + public documentState: DocumentState, public lax: boolean, public fstar: FStarConnection) { this.uri = currentDoc.uri; @@ -467,7 +534,7 @@ export class DocumentProcess { clearTimeout(this.changeDispatcher); } - get connection() { return this.server.connection; } + get connection() { return this.documentState.server.connection; } changeDoc(newDoc: TextDocument) { clearTimeout(this.changeDispatcher); @@ -480,16 +547,8 @@ export class DocumentProcess { // 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() { @@ -504,17 +563,7 @@ 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 }); } - } + // TODO: report status this.fstar.fullBufferRequest(this.currentDoc.getText(), kind, false); } @@ -523,15 +572,12 @@ export class DocumentProcess { // 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 }); + + // TODO: report status this.fstar.partialBufferRequest(this.currentDoc.getText(), kind, position); } @@ -583,13 +629,10 @@ export class DocumentProcess { // 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 @@ -602,78 +645,83 @@ export class DocumentProcess { // 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 = []; + if (contents.stage === "full-buffer-started") { + 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; + } + 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, + }); + + if (!this.lax) // TODO: report lax status + 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.sendDiags(); + if (!this.lax) // TODO: report lax status + 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 (this.newResults) { + console.error('full-buffer-fragment-failed without fill-buffer-fragment-started'); + return; + } + + const frag = this.results.fragments.at(-1)!; + frag.ok = false; + + if (!this.lax) // TODO: report lax status + 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,69 +730,36 @@ 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))); } async onCompletion(textDocumentPosition: TextDocumentPositionParams): Promise {