From ad30eaa6d9b6e7166c7753fe05915ed420ee0434 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 10 Aug 2023 23:44:59 +0200 Subject: [PATCH 01/30] Draft --- src/ui/gutterIconsView.ts | 129 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 129 insertions(+) create mode 100644 src/ui/gutterIconsView.ts diff --git a/src/ui/gutterIconsView.ts b/src/ui/gutterIconsView.ts new file mode 100644 index 00000000..f60af25d --- /dev/null +++ b/src/ui/gutterIconsView.ts @@ -0,0 +1,129 @@ +/* eslint-disable max-depth */ +/* eslint-disable @typescript-eslint/brace-style */ +import { Diagnostic, DocumentSymbol, ExtensionContext, Range, Uri, window, workspace } from 'vscode'; +import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; +import CompilationStatusView from './compilationStatusView'; +import { IVerificationGutterStatusParams, LineVerificationStatus } from '../language/api/verificationGutterStatusParams'; +import { NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; +import VerificationSymbolStatusView from './verificationSymbolStatusView'; + +/** + * This class shows verification tasks through the VSCode testing UI. + */ +export default class GutterIconsView { + + + public constructor( + private readonly context: ExtensionContext, + private readonly languageClient: DafnyLanguageClient, + private readonly compilationStatusView: CompilationStatusView) + { + languageClient.onPublishDiagnostics((uri, diagnostics) => { + + }); + } + + private nameToSymbolRange(rootSymbols: DocumentSymbol[]): Map { + + } + + /* + No support for first-time icons yet. For first time we pretend like the symbol was previously verified. + Error context is only triggered if the symbol currently has an error, not if it only had an error and is currently verifying. + */ + private async computeNewGutterIcons(uri: Uri, nameToSymbolRanges: Map, + statuses: NamedVerifiableStatus[], + diagnostics: Diagnostic[]): Promise + { + const document = await workspace.openTextDocument(uri); + const statusPerLine = new Map(); + const linesWithErrors = new Map(); + const lineToSymbolRange = new Map(); + const linesInErrorContext = new Set(); + + for(const range of nameToSymbolRanges.values()) { + for(let line = range.start.line; line < range.end.line; line++) { + lineToSymbolRange.set(line, range); + } + } + const perLineStatus: LineVerificationStatus[] = []; + for(const diagnostic of diagnostics) { + for(let line = diagnostic.range.start.line; line < diagnostic.range.end.line; line++) { + linesWithErrors.set(line, diagnostic.source === 'Parser'); + const contextRange = lineToSymbolRange.get(line)!; + for(let line = contextRange.start.line; line < contextRange.end.line; line++) { + linesInErrorContext.add(line); + } + } + } + + for(const status of statuses) { + const symbolRange = nameToSymbolRanges.get(VerificationSymbolStatusView.convertRange(status.nameRange))!; + for(let line = symbolRange.start.line; line < symbolRange.end.line; line++) { + statusPerLine.set(line, status.status); + } + } + for(let line = 0; line < document.lineCount; line++) { + const error = linesWithErrors.get(line); + if(error === true) { + perLineStatus.push(LineVerificationStatus.ResolutionError); + } else { + let bigNumber: number; + if(error === false) { + bigNumber = LineVerificationStatus.AssertionFailed; + } else { + if(linesInErrorContext.has(line)) { + bigNumber = LineVerificationStatus.ErrorContext; + } else { + bigNumber = LineVerificationStatus.Verified; + } + } + let smallNumber: number; + switch(statusPerLine.get(line)) { + case PublishedVerificationStatus.Stale: + case PublishedVerificationStatus.Queued: + smallNumber = 0; + break; + case PublishedVerificationStatus.Running: + smallNumber = 1; + break; + case PublishedVerificationStatus.Error: + case PublishedVerificationStatus.Correct: + smallNumber = 2; + break; + default: throw new Error(`unknown PublishedVerificationStatus ${statusPerLine.get(line)}`); + } + perLineStatus.push(bigNumber + smallNumber); + } + } + return { uri: uri.toString(), perLineStatus: perLineStatus }; + } + +// export enum LineVerificationStatus { +// // Default value for every line, before the renderer figures it out. +// Nothing = 0, +// // For first-time computation not actively computing but soon. Synonym of "obsolete" +// // (scheduledComputation) +// Scheduled = 1, +// // For first-time computations, actively computing +// Verifying = 2, +// // Also applicable for empty spaces if they are not surrounded by errors. +// Verified = 200, +// VerifiedObsolete = 201, +// VerifiedVerifying = 202, +// // For trees containing children with errors (e.g. methods) +// ErrorContext = 300, +// ErrorContextObsolete = 301, +// ErrorContextVerifying = 302, +// // For individual assertions in error ranges +// AssertionVerifiedInErrorContext = 350, +// AssertionVerifiedInErrorContextObsolete = 351, +// AssertionVerifiedInErrorContextVerifying = 352, +// // For specific lines which have errors on it. They take over verified assertions +// AssertionFailed = 400, +// AssertionFailedObsolete = 401, +// AssertionFailedVerifying = 402, +// // For lines containing resolution or parse errors +// ResolutionError = 500, +// } +} \ No newline at end of file From 7474f9c470556ac35f12c4a6523f83e10fdcaed8 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Aug 2023 12:52:56 +0200 Subject: [PATCH 02/30] Incorrect icons show up in the gutter --- src/ui/dafnyIntegration.ts | 4 +- src/ui/gutterIconsView.ts | 58 ++++++++++++++++++++------ src/ui/verificationGutterStatusView.ts | 2 +- src/ui/verificationSymbolStatusView.ts | 27 ++++++++---- 4 files changed, 68 insertions(+), 23 deletions(-) diff --git a/src/ui/dafnyIntegration.ts b/src/ui/dafnyIntegration.ts index adfbfec1..de1ad54e 100644 --- a/src/ui/dafnyIntegration.ts +++ b/src/ui/dafnyIntegration.ts @@ -10,6 +10,7 @@ import VerificationSymbolStatusView from './verificationSymbolStatusView'; import Configuration from '../configuration'; import { ConfigurationConstants, LanguageServerConstants } from '../constants'; import { DafnyInstaller } from '../language/dafnyInstallation'; +import GutterIconsView from './gutterIconsView'; export default function createAndRegisterDafnyIntegration( installer: DafnyInstaller, @@ -21,8 +22,10 @@ export default function createAndRegisterDafnyIntegration( const compilationStatusView = CompilationStatusView.createAndRegister(installer.context, languageClient, languageServerVersion); let symbolStatusView: VerificationSymbolStatusView | undefined = undefined; const serverSupportsSymbolStatusView = configuredVersionToNumeric('3.8.0') <= configuredVersionToNumeric(languageServerVersion); + const gutterViewUi = VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); if(serverSupportsSymbolStatusView && Configuration.get(ConfigurationConstants.LanguageServer.DisplayVerificationAsTests)) { symbolStatusView = VerificationSymbolStatusView.createAndRegister(installer.context, languageClient, compilationStatusView); + new GutterIconsView(languageClient, gutterViewUi, symbolStatusView); } else { if(serverSupportsSymbolStatusView) { compilationStatusView.registerAfter38Messages(); @@ -30,7 +33,6 @@ export default function createAndRegisterDafnyIntegration( compilationStatusView.registerBefore38Messages(); } } - VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); CompileCommands.createAndRegister(installer); RelatedErrorView.createAndRegister(installer.context, languageClient); DafnyVersionView.createAndRegister(installer, languageServerVersion); diff --git a/src/ui/gutterIconsView.ts b/src/ui/gutterIconsView.ts index f60af25d..626c151d 100644 --- a/src/ui/gutterIconsView.ts +++ b/src/ui/gutterIconsView.ts @@ -1,37 +1,65 @@ /* eslint-disable max-depth */ /* eslint-disable @typescript-eslint/brace-style */ -import { Diagnostic, DocumentSymbol, ExtensionContext, Range, Uri, window, workspace } from 'vscode'; +import { Diagnostic, DocumentSymbol, Range, Uri, languages, commands, workspace, Position } from 'vscode'; import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; -import CompilationStatusView from './compilationStatusView'; import { IVerificationGutterStatusParams, LineVerificationStatus } from '../language/api/verificationGutterStatusParams'; import { NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; import VerificationSymbolStatusView from './verificationSymbolStatusView'; +import VerificationGutterStatusView from './verificationGutterStatusView'; /** * This class shows verification tasks through the VSCode testing UI. */ export default class GutterIconsView { - public constructor( - private readonly context: ExtensionContext, private readonly languageClient: DafnyLanguageClient, - private readonly compilationStatusView: CompilationStatusView) + private readonly gutterViewUi: VerificationGutterStatusView, + private readonly symbolStatusView: VerificationSymbolStatusView) { - languageClient.onPublishDiagnostics((uri, diagnostics) => { - + languageClient.onPublishDiagnostics((uri) => { + this.update(uri); + }); + symbolStatusView.onUpdates(uri => { + this.update(uri); }); } - private nameToSymbolRange(rootSymbols: DocumentSymbol[]): Map { + private async update(uri: Uri) { + const rootSymbols = await commands.executeCommand('vscode.executeDocumentSymbolProvider', uri) as DocumentSymbol[] | undefined; + if(rootSymbols === undefined) { + return; + } + const nameToSymbolRange = this.getNameToSymbolRange(rootSymbols); + const diagnostics = languages.getDiagnostics(uri); + const symbolStatus = this.symbolStatusView.getUpdatesForFile(uri.toString()); + if(symbolStatus === undefined) { + return; + } + const icons = await this.computeNewGutterIcons(uri, nameToSymbolRange, symbolStatus.namedVerifiables, diagnostics); + this.gutterViewUi.updateVerificationStatusGutter(icons); + } + + private getNameToSymbolRange(rootSymbols: DocumentSymbol[]): Map { + const result = new Map(); + const stack = rootSymbols; + while(stack.length > 0) { + const top = stack.pop()!; + const children = top.children ?? []; + stack.push(...children); + result.set(positionToString(top.selectionRange.start), top.range); + } + return result; } /* No support for first-time icons yet. For first time we pretend like the symbol was previously verified. Error context is only triggered if the symbol currently has an error, not if it only had an error and is currently verifying. */ - private async computeNewGutterIcons(uri: Uri, nameToSymbolRanges: Map, + private async computeNewGutterIcons( + uri: Uri, + nameToSymbolRanges: Map, statuses: NamedVerifiableStatus[], diagnostics: Diagnostic[]): Promise { @@ -58,8 +86,9 @@ export default class GutterIconsView { } for(const status of statuses) { - const symbolRange = nameToSymbolRanges.get(VerificationSymbolStatusView.convertRange(status.nameRange))!; - for(let line = symbolRange.start.line; line < symbolRange.end.line; line++) { + const convertedRange = VerificationSymbolStatusView.convertRange(status.nameRange); + const symbolRange = nameToSymbolRanges.get(positionToString(convertedRange.start))!; + for(let line = symbolRange.start.line; line <= symbolRange.end.line; line++) { statusPerLine.set(line, status.status); } } @@ -89,6 +118,7 @@ export default class GutterIconsView { break; case PublishedVerificationStatus.Error: case PublishedVerificationStatus.Correct: + case undefined: smallNumber = 2; break; default: throw new Error(`unknown PublishedVerificationStatus ${statusPerLine.get(line)}`); @@ -126,4 +156,8 @@ export default class GutterIconsView { // // For lines containing resolution or parse errors // ResolutionError = 500, // } -} \ No newline at end of file +} + +function positionToString(start: Position): string { + return `${start.line},${start.character}`; +} diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 2e9f92f1..92a68602 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -308,7 +308,7 @@ export default class VerificationGutterStatusView { } // Entry point when receiving IVErificationStatusGutter - private async updateVerificationStatusGutter(params: IVerificationGutterStatusParams): Promise { + public async updateVerificationStatusGutter(params: IVerificationGutterStatusParams): Promise { if(this.areParamsOutdated(params)) { return; } diff --git a/src/ui/verificationSymbolStatusView.ts b/src/ui/verificationSymbolStatusView.ts index 0793248a..2d77049d 100644 --- a/src/ui/verificationSymbolStatusView.ts +++ b/src/ui/verificationSymbolStatusView.ts @@ -1,5 +1,7 @@ /* eslint-disable max-depth */ -import { commands, ExtensionContext, workspace, tests, Range, Position, Uri, TestRunRequest, TestController, TestRun, DocumentSymbol, TestItem, TestItemCollection, TextDocument, TestRunProfileKind, window } from 'vscode'; +import { commands, ExtensionContext, workspace, tests, Range, Position, Uri, + TestRunRequest, TestController, TestRun, DocumentSymbol, TestItem, TestItemCollection, TextDocument, TestRunProfileKind, window, + Event, EventEmitter } from 'vscode'; import { Range as lspRange, Position as lspPosition } from 'vscode-languageclient'; import { IVerificationSymbolStatusParams, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; @@ -34,6 +36,17 @@ export default class VerificationSymbolStatusView { return new VerificationSymbolStatusView(context, languageClient, compilationStatusView); } + private itemStates: Map = new Map(); + private itemRuns: Map = new Map(); + private readonly runItemsLeft: Map = new Map(); + private readonly updateListenersPerFile: Map> = new Map(); + private readonly updatesPerFile: Map = new Map(); + private readonly controller: TestController; + private automaticRunEnd: boolean = false; + private noRunCreationInProgress: Promise = Promise.resolve(); + private readonly _onUpdates: EventEmitter = new EventEmitter(); + public onUpdates: Event = this._onUpdates.event; + public constructor( private readonly context: ExtensionContext, private readonly languageClient: DafnyLanguageClient, @@ -75,14 +88,9 @@ export default class VerificationSymbolStatusView { }); } - private itemStates: Map = new Map(); - private itemRuns: Map = new Map(); - private readonly runItemsLeft: Map = new Map(); - private readonly updateListenersPerFile: Map> = new Map(); - private readonly updatesPerFile: Map = new Map(); - private readonly controller: TestController; - private automaticRunEnd: boolean = false; - private noRunCreationInProgress: Promise = Promise.resolve(); + public getUpdatesForFile(uri: string): IVerificationSymbolStatusParams | undefined { + return this.updatesPerFile.get(uri); + } private createController(): TestController { const controller = tests.createTestController('verificationStatus', 'Verification Status'); @@ -168,6 +176,7 @@ export default class VerificationSymbolStatusView { rootSymbols: DocumentSymbol[] | undefined) { this.updatesPerFile.set(params.uri, params); + this._onUpdates.fire(document.uri); if(window.activeTextEditor?.document.uri.toString() !== params.uri.toString()) { return; } From 06bcee73d291c8e38e08967f7dd65e1725f2fddc Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Aug 2023 13:04:05 +0200 Subject: [PATCH 03/30] Icons seem correct at first glance --- src/ui/gutterIconsView.ts | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/ui/gutterIconsView.ts b/src/ui/gutterIconsView.ts index 626c151d..50c2630b 100644 --- a/src/ui/gutterIconsView.ts +++ b/src/ui/gutterIconsView.ts @@ -1,6 +1,6 @@ /* eslint-disable max-depth */ /* eslint-disable @typescript-eslint/brace-style */ -import { Diagnostic, DocumentSymbol, Range, Uri, languages, commands, workspace, Position } from 'vscode'; +import { Diagnostic, DiagnosticSeverity, DocumentSymbol, Range, Uri, languages, commands, workspace, Position } from 'vscode'; import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; import { IVerificationGutterStatusParams, LineVerificationStatus } from '../language/api/verificationGutterStatusParams'; import { NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; @@ -65,7 +65,7 @@ export default class GutterIconsView { { const document = await workspace.openTextDocument(uri); const statusPerLine = new Map(); - const linesWithErrors = new Map(); + const errorLineSource = new Map(); const lineToSymbolRange = new Map(); const linesInErrorContext = new Set(); @@ -76,8 +76,11 @@ export default class GutterIconsView { } const perLineStatus: LineVerificationStatus[] = []; for(const diagnostic of diagnostics) { - for(let line = diagnostic.range.start.line; line < diagnostic.range.end.line; line++) { - linesWithErrors.set(line, diagnostic.source === 'Parser'); + if(diagnostic.severity !== DiagnosticSeverity.Error) { + continue; + } + for(let line = diagnostic.range.start.line; line <= diagnostic.range.end.line; line++) { + errorLineSource.set(line, diagnostic.source ?? ''); // TODO what about the resolver? const contextRange = lineToSymbolRange.get(line)!; for(let line = contextRange.start.line; line < contextRange.end.line; line++) { linesInErrorContext.add(line); @@ -93,12 +96,12 @@ export default class GutterIconsView { } } for(let line = 0; line < document.lineCount; line++) { - const error = linesWithErrors.get(line); - if(error === true) { + const error = errorLineSource.get(line); + if(error === 'Parser') { perLineStatus.push(LineVerificationStatus.ResolutionError); } else { let bigNumber: number; - if(error === false) { + if(error !== undefined) { bigNumber = LineVerificationStatus.AssertionFailed; } else { if(linesInErrorContext.has(line)) { @@ -111,15 +114,15 @@ export default class GutterIconsView { switch(statusPerLine.get(line)) { case PublishedVerificationStatus.Stale: case PublishedVerificationStatus.Queued: - smallNumber = 0; + smallNumber = 1; break; case PublishedVerificationStatus.Running: - smallNumber = 1; + smallNumber = 2; break; case PublishedVerificationStatus.Error: case PublishedVerificationStatus.Correct: case undefined: - smallNumber = 2; + smallNumber = 0; break; default: throw new Error(`unknown PublishedVerificationStatus ${statusPerLine.get(line)}`); } From 0b463b820d3a7f2d9bb8d2f293fd89a54480bdba Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Aug 2023 16:09:07 +0200 Subject: [PATCH 04/30] Seems pretty good --- src/ui/gutterIconsView.ts | 88 ++++++++++++-------------- src/ui/verificationGutterStatusView.ts | 21 +++--- src/ui/verificationSymbolStatusView.ts | 29 +++++---- 3 files changed, 68 insertions(+), 70 deletions(-) diff --git a/src/ui/gutterIconsView.ts b/src/ui/gutterIconsView.ts index 50c2630b..5a6fa69f 100644 --- a/src/ui/gutterIconsView.ts +++ b/src/ui/gutterIconsView.ts @@ -33,12 +33,9 @@ export default class GutterIconsView { const nameToSymbolRange = this.getNameToSymbolRange(rootSymbols); const diagnostics = languages.getDiagnostics(uri); const symbolStatus = this.symbolStatusView.getUpdatesForFile(uri.toString()); - if(symbolStatus === undefined) { - return; - } - const icons = await this.computeNewGutterIcons(uri, nameToSymbolRange, symbolStatus.namedVerifiables, diagnostics); - this.gutterViewUi.updateVerificationStatusGutter(icons); + const icons = await this.computeNewGutterIcons(uri, nameToSymbolRange, symbolStatus?.namedVerifiables, diagnostics); + this.gutterViewUi.updateVerificationStatusGutter(icons, false); } private getNameToSymbolRange(rootSymbols: DocumentSymbol[]): Map { @@ -55,12 +52,11 @@ export default class GutterIconsView { /* No support for first-time icons yet. For first time we pretend like the symbol was previously verified. - Error context is only triggered if the symbol currently has an error, not if it only had an error and is currently verifying. */ private async computeNewGutterIcons( uri: Uri, - nameToSymbolRanges: Map, - statuses: NamedVerifiableStatus[], + nameToSymbolRanges: Map | undefined, + statuses: NamedVerifiableStatus[] | undefined, diagnostics: Diagnostic[]): Promise { const document = await workspace.openTextDocument(uri); @@ -68,10 +64,13 @@ export default class GutterIconsView { const errorLineSource = new Map(); const lineToSymbolRange = new Map(); const linesInErrorContext = new Set(); + const linesToSkip = new Set(); - for(const range of nameToSymbolRanges.values()) { - for(let line = range.start.line; line < range.end.line; line++) { - lineToSymbolRange.set(line, range); + if(nameToSymbolRanges !== undefined) { + for(const range of nameToSymbolRanges.values()) { + for(let line = range.start.line; line < range.end.line; line++) { + lineToSymbolRange.set(line, range); + } } } const perLineStatus: LineVerificationStatus[] = []; @@ -80,24 +79,43 @@ export default class GutterIconsView { continue; } for(let line = diagnostic.range.start.line; line <= diagnostic.range.end.line; line++) { - errorLineSource.set(line, diagnostic.source ?? ''); // TODO what about the resolver? - const contextRange = lineToSymbolRange.get(line)!; - for(let line = contextRange.start.line; line < contextRange.end.line; line++) { - linesInErrorContext.add(line); + errorLineSource.set(line, diagnostic.source ?? ''); + const contextRange = lineToSymbolRange.get(line); + if(contextRange === undefined) { + continue; + } + for(let contextLine = contextRange.start.line; line < contextRange.end.line; line++) { + linesInErrorContext.add(contextLine); } } } - for(const status of statuses) { - const convertedRange = VerificationSymbolStatusView.convertRange(status.nameRange); - const symbolRange = nameToSymbolRanges.get(positionToString(convertedRange.start))!; - for(let line = symbolRange.start.line; line <= symbolRange.end.line; line++) { - statusPerLine.set(line, status.status); + if(nameToSymbolRanges === undefined || statuses === undefined) { + for(let line = 0; line < document.lineCount; line++) { + statusPerLine.set(line, PublishedVerificationStatus.Stale); + } + } else { + for(const status of statuses) { + const convertedRange = VerificationSymbolStatusView.convertRange(status.nameRange); + const symbolRange = nameToSymbolRanges.get(positionToString(convertedRange.start)); + linesToSkip.add(convertedRange.start.line); + if(symbolRange === undefined) { + console.error('symbol mismatch between documentSymbol and symbolStatus API'); + continue; + } + for(let line = symbolRange.start.line; line <= symbolRange.end.line; line++) { + statusPerLine.set(line, status.status); + } } } for(let line = 0; line < document.lineCount; line++) { + if(linesToSkip.has(line)) { + perLineStatus.push(LineVerificationStatus.Nothing); + continue; + } + const error = errorLineSource.get(line); - if(error === 'Parser') { + if(error === 'Parser' || error === 'Resolver') { // TODO what about the resolver? perLineStatus.push(LineVerificationStatus.ResolutionError); } else { let bigNumber: number; @@ -131,34 +149,6 @@ export default class GutterIconsView { } return { uri: uri.toString(), perLineStatus: perLineStatus }; } - -// export enum LineVerificationStatus { -// // Default value for every line, before the renderer figures it out. -// Nothing = 0, -// // For first-time computation not actively computing but soon. Synonym of "obsolete" -// // (scheduledComputation) -// Scheduled = 1, -// // For first-time computations, actively computing -// Verifying = 2, -// // Also applicable for empty spaces if they are not surrounded by errors. -// Verified = 200, -// VerifiedObsolete = 201, -// VerifiedVerifying = 202, -// // For trees containing children with errors (e.g. methods) -// ErrorContext = 300, -// ErrorContextObsolete = 301, -// ErrorContextVerifying = 302, -// // For individual assertions in error ranges -// AssertionVerifiedInErrorContext = 350, -// AssertionVerifiedInErrorContextObsolete = 351, -// AssertionVerifiedInErrorContextVerifying = 352, -// // For specific lines which have errors on it. They take over verified assertions -// AssertionFailed = 400, -// AssertionFailedObsolete = 401, -// AssertionFailedVerifying = 402, -// // For lines containing resolution or parse errors -// ResolutionError = 500, -// } } function positionToString(start: Position): string { diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 92a68602..fc3d66c1 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -117,7 +117,7 @@ export default class VerificationGutterStatusView { context.subscriptions.push( workspace.onDidCloseTextDocument(document => instance.clearVerificationDiagnostics(document.uri.toString())), window.onDidChangeActiveTextEditor(editor => instance.refreshDisplayedVerificationGutterStatuses(editor)), - languageClient.onVerificationStatusGutter(params => instance.updateVerificationStatusGutter(params)) + languageClient.onVerificationStatusGutter(params => instance.updateVerificationStatusGutter(params, true)) ); return instance; } @@ -258,13 +258,18 @@ export default class VerificationGutterStatusView { // Converts the IVerificationStatusGutter to a map from line verification status // to an array of ranges that VSCode can consume. - private async getRangesOfLineStatus(params: IVerificationGutterStatusParams): Promise> { + private async getRangesOfLineStatus(params: IVerificationGutterStatusParams, skipVerificationSymbolHeaders: boolean): Promise> { const perLineStatus = this.addCosmetics(params.perLineStatus); - const symbolParams - = params.perLineStatus.indexOf(LineVerificationStatus.ResolutionError) > 0 ? [] - : await (this.symbolStatusView?.getVerifiableRanges(params.uri) ?? Promise.resolve([])); - const originalLinesToSkip = symbolParams.map(range => range.start.line).sort((a, b) => a - b); + let originalLinesToSkip: number[]; + if(skipVerificationSymbolHeaders) { + const symbolParams + = params.perLineStatus.indexOf(LineVerificationStatus.ResolutionError) > 0 ? [] + : await (this.symbolStatusView?.getVerifiableRanges(params.uri) ?? Promise.resolve([])); + originalLinesToSkip = symbolParams.map(range => range.start.line).sort((a, b) => a - b); + } else { + originalLinesToSkip = []; + } return VerificationGutterStatusView.perLineStatusToRanges(perLineStatus, originalLinesToSkip); } @@ -308,13 +313,13 @@ export default class VerificationGutterStatusView { } // Entry point when receiving IVErificationStatusGutter - public async updateVerificationStatusGutter(params: IVerificationGutterStatusParams): Promise { + public async updateVerificationStatusGutter(params: IVerificationGutterStatusParams, skipVerificationSymbolHeaders: boolean): Promise { if(this.areParamsOutdated(params)) { return; } params.uri = Uri.parse(params.uri).toString();// Makes the Uri canonical const documentPath = getVsDocumentPath(params); - const ranges = await this.getRangesOfLineStatus(params); + const ranges = await this.getRangesOfLineStatus(params, skipVerificationSymbolHeaders); const newData: LinearVerificationGutterStatus = { decorations: ranges, diff --git a/src/ui/verificationSymbolStatusView.ts b/src/ui/verificationSymbolStatusView.ts index 2d77049d..b56edcc1 100644 --- a/src/ui/verificationSymbolStatusView.ts +++ b/src/ui/verificationSymbolStatusView.ts @@ -99,22 +99,25 @@ export default class VerificationSymbolStatusView { const runningItems: TestItem[] = []; let outerResolve: () => void; await this.noRunCreationInProgress; - this.noRunCreationInProgress = new Promise((resolve) => { - outerResolve = resolve; - }); - - const runs = items.map(item => this.languageClient.runVerification({ position: item.range!.start, textDocument: { uri: item.uri!.toString() } })); - for(const index in runs) { - const success = await runs[index]; - if(success) { - runningItems.push(items[index]); + try { + this.noRunCreationInProgress = new Promise((resolve) => { + outerResolve = resolve; + }); + + const runs = items.map(item => this.languageClient.runVerification({ position: item.range!.start, textDocument: { uri: item.uri!.toString() } })); + for(const index in runs) { + const success = await runs[index]; + if(success) { + runningItems.push(items[index]); + } } - } - if(runningItems.length > 0) { - this.createRun(runningItems); + if(runningItems.length > 0) { + this.createRun(runningItems); + } + } finally { + outerResolve!(); } - outerResolve!(); }, true); return controller; } From 1845185b1d2c936e135049a065ad3bfe141373cf Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Aug 2023 16:13:08 +0200 Subject: [PATCH 05/30] Refactoring --- src/ui/gutterIconsView.ts | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/src/ui/gutterIconsView.ts b/src/ui/gutterIconsView.ts index 5a6fa69f..acef3ede 100644 --- a/src/ui/gutterIconsView.ts +++ b/src/ui/gutterIconsView.ts @@ -61,7 +61,7 @@ export default class GutterIconsView { { const document = await workspace.openTextDocument(uri); const statusPerLine = new Map(); - const errorLineSource = new Map(); + const lineToErrorSource = new Map(); const lineToSymbolRange = new Map(); const linesInErrorContext = new Set(); const linesToSkip = new Set(); @@ -79,7 +79,7 @@ export default class GutterIconsView { continue; } for(let line = diagnostic.range.start.line; line <= diagnostic.range.end.line; line++) { - errorLineSource.set(line, diagnostic.source ?? ''); + lineToErrorSource.set(line, diagnostic.source ?? ''); const contextRange = lineToSymbolRange.get(line); if(contextRange === undefined) { continue; @@ -114,8 +114,8 @@ export default class GutterIconsView { continue; } - const error = errorLineSource.get(line); - if(error === 'Parser' || error === 'Resolver') { // TODO what about the resolver? + const error = lineToErrorSource.get(line); + if(error === 'Parser' || error === 'Resolver') { perLineStatus.push(LineVerificationStatus.ResolutionError); } else { let bigNumber: number; @@ -132,15 +132,15 @@ export default class GutterIconsView { switch(statusPerLine.get(line)) { case PublishedVerificationStatus.Stale: case PublishedVerificationStatus.Queued: - smallNumber = 1; + smallNumber = GutterIconProgress.Stale; break; case PublishedVerificationStatus.Running: - smallNumber = 2; + smallNumber = GutterIconProgress.Running; break; case PublishedVerificationStatus.Error: case PublishedVerificationStatus.Correct: case undefined: - smallNumber = 0; + smallNumber = GutterIconProgress.Done; break; default: throw new Error(`unknown PublishedVerificationStatus ${statusPerLine.get(line)}`); } @@ -151,6 +151,12 @@ export default class GutterIconsView { } } +export enum GutterIconProgress { + Stale = 1, + Running = 2, + Done = 0 +} + function positionToString(start: Position): string { return `${start.line},${start.character}`; } From 6f86f2b13b8e4519afe7b80281b105f6b8bf3ac9 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Aug 2023 16:26:26 +0200 Subject: [PATCH 06/30] Do not get server gutter icons --- src/language/dafnyLanguageClient.ts | 2 +- src/ui/dafnyIntegration.ts | 4 +++- src/ui/gutterIconsView.ts | 18 +++++++++--------- 3 files changed, 13 insertions(+), 11 deletions(-) diff --git a/src/language/dafnyLanguageClient.ts b/src/language/dafnyLanguageClient.ts index ae6caa01..4b856695 100644 --- a/src/language/dafnyLanguageClient.ts +++ b/src/language/dafnyLanguageClient.ts @@ -34,7 +34,7 @@ function getLanguageServerLaunchArgsNew(): string[] { getVerifierCachingPolicy(), `--cores:${cores}`, `--notify-ghostness:${Configuration.get(ConfigurationConstants.LanguageServer.MarkGhostStatements)}`, - `--notify-line-verification-status:${Configuration.get(ConfigurationConstants.LanguageServer.DisplayGutterStatus)}`, + '--notify-line-verification-status:false', ...getDafnyPluginsArgument(), ...launchArgs ]; diff --git a/src/ui/dafnyIntegration.ts b/src/ui/dafnyIntegration.ts index de1ad54e..b5ba1639 100644 --- a/src/ui/dafnyIntegration.ts +++ b/src/ui/dafnyIntegration.ts @@ -25,7 +25,9 @@ export default function createAndRegisterDafnyIntegration( const gutterViewUi = VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); if(serverSupportsSymbolStatusView && Configuration.get(ConfigurationConstants.LanguageServer.DisplayVerificationAsTests)) { symbolStatusView = VerificationSymbolStatusView.createAndRegister(installer.context, languageClient, compilationStatusView); - new GutterIconsView(languageClient, gutterViewUi, symbolStatusView); + if(Configuration.get(ConfigurationConstants.LanguageServer.DisplayGutterStatus) === 'true') { + new GutterIconsView(languageClient, gutterViewUi, symbolStatusView); + } } else { if(serverSupportsSymbolStatusView) { compilationStatusView.registerAfter38Messages(); diff --git a/src/ui/gutterIconsView.ts b/src/ui/gutterIconsView.ts index acef3ede..2f79fc73 100644 --- a/src/ui/gutterIconsView.ts +++ b/src/ui/gutterIconsView.ts @@ -118,33 +118,33 @@ export default class GutterIconsView { if(error === 'Parser' || error === 'Resolver') { perLineStatus.push(LineVerificationStatus.ResolutionError); } else { - let bigNumber: number; + let resultStatus: number; if(error !== undefined) { - bigNumber = LineVerificationStatus.AssertionFailed; + resultStatus = LineVerificationStatus.AssertionFailed; } else { if(linesInErrorContext.has(line)) { - bigNumber = LineVerificationStatus.ErrorContext; + resultStatus = LineVerificationStatus.ErrorContext; } else { - bigNumber = LineVerificationStatus.Verified; + resultStatus = LineVerificationStatus.Verified; } } - let smallNumber: number; + let progressStatus: number; switch(statusPerLine.get(line)) { case PublishedVerificationStatus.Stale: case PublishedVerificationStatus.Queued: - smallNumber = GutterIconProgress.Stale; + progressStatus = GutterIconProgress.Stale; break; case PublishedVerificationStatus.Running: - smallNumber = GutterIconProgress.Running; + progressStatus = GutterIconProgress.Running; break; case PublishedVerificationStatus.Error: case PublishedVerificationStatus.Correct: case undefined: - smallNumber = GutterIconProgress.Done; + progressStatus = GutterIconProgress.Done; break; default: throw new Error(`unknown PublishedVerificationStatus ${statusPerLine.get(line)}`); } - perLineStatus.push(bigNumber + smallNumber); + perLineStatus.push(resultStatus + progressStatus); } } return { uri: uri.toString(), perLineStatus: perLineStatus }; From 6c86aae913722b13ec6f4794eb042088fcbbe431 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Aug 2023 16:59:31 +0200 Subject: [PATCH 07/30] Fix --- src/ui/dafnyIntegration.ts | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ui/dafnyIntegration.ts b/src/ui/dafnyIntegration.ts index b5ba1639..0c1a844a 100644 --- a/src/ui/dafnyIntegration.ts +++ b/src/ui/dafnyIntegration.ts @@ -25,7 +25,8 @@ export default function createAndRegisterDafnyIntegration( const gutterViewUi = VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); if(serverSupportsSymbolStatusView && Configuration.get(ConfigurationConstants.LanguageServer.DisplayVerificationAsTests)) { symbolStatusView = VerificationSymbolStatusView.createAndRegister(installer.context, languageClient, compilationStatusView); - if(Configuration.get(ConfigurationConstants.LanguageServer.DisplayGutterStatus) === 'true') { + const displayGutterStatus = Configuration.get(ConfigurationConstants.LanguageServer.DisplayGutterStatus); + if(displayGutterStatus) { new GutterIconsView(languageClient, gutterViewUi, symbolStatusView); } } else { From dd7aec712c1c1b91ff3d060be5e417b5f650f436 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Aug 2023 10:45:03 +0200 Subject: [PATCH 08/30] Fixes and refactoring --- src/ui/dafnyIntegration.ts | 14 +++++++------ src/ui/gutterIconsView.ts | 13 ++++++------ src/ui/symbolStatusService.ts | 29 ++++++++++++++++++++++++++ src/ui/verificationSymbolStatusView.ts | 27 +++++++----------------- 4 files changed, 50 insertions(+), 33 deletions(-) create mode 100644 src/ui/symbolStatusService.ts diff --git a/src/ui/dafnyIntegration.ts b/src/ui/dafnyIntegration.ts index 0c1a844a..9ea99beb 100644 --- a/src/ui/dafnyIntegration.ts +++ b/src/ui/dafnyIntegration.ts @@ -11,6 +11,7 @@ import Configuration from '../configuration'; import { ConfigurationConstants, LanguageServerConstants } from '../constants'; import { DafnyInstaller } from '../language/dafnyInstallation'; import GutterIconsView from './gutterIconsView'; +import SymbolStatusService from './symbolStatusService'; export default function createAndRegisterDafnyIntegration( installer: DafnyInstaller, @@ -22,13 +23,9 @@ export default function createAndRegisterDafnyIntegration( const compilationStatusView = CompilationStatusView.createAndRegister(installer.context, languageClient, languageServerVersion); let symbolStatusView: VerificationSymbolStatusView | undefined = undefined; const serverSupportsSymbolStatusView = configuredVersionToNumeric('3.8.0') <= configuredVersionToNumeric(languageServerVersion); - const gutterViewUi = VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); + const symbolStatusService = new SymbolStatusService(installer.context, languageClient); if(serverSupportsSymbolStatusView && Configuration.get(ConfigurationConstants.LanguageServer.DisplayVerificationAsTests)) { - symbolStatusView = VerificationSymbolStatusView.createAndRegister(installer.context, languageClient, compilationStatusView); - const displayGutterStatus = Configuration.get(ConfigurationConstants.LanguageServer.DisplayGutterStatus); - if(displayGutterStatus) { - new GutterIconsView(languageClient, gutterViewUi, symbolStatusView); - } + symbolStatusView = VerificationSymbolStatusView.createAndRegister(installer.context, languageClient, symbolStatusService, compilationStatusView); } else { if(serverSupportsSymbolStatusView) { compilationStatusView.registerAfter38Messages(); @@ -36,6 +33,11 @@ export default function createAndRegisterDafnyIntegration( compilationStatusView.registerBefore38Messages(); } } + const displayGutterStatus = Configuration.get(ConfigurationConstants.LanguageServer.DisplayGutterStatus); + if(displayGutterStatus) { + const gutterViewUi = VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); + new GutterIconsView(languageClient, gutterViewUi, symbolStatusService); + } CompileCommands.createAndRegister(installer); RelatedErrorView.createAndRegister(installer.context, languageClient); DafnyVersionView.createAndRegister(installer, languageServerVersion); diff --git a/src/ui/gutterIconsView.ts b/src/ui/gutterIconsView.ts index 2f79fc73..11e5ad63 100644 --- a/src/ui/gutterIconsView.ts +++ b/src/ui/gutterIconsView.ts @@ -6,22 +6,21 @@ import { IVerificationGutterStatusParams, LineVerificationStatus } from '../lang import { NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; import VerificationSymbolStatusView from './verificationSymbolStatusView'; import VerificationGutterStatusView from './verificationGutterStatusView'; +import SymbolStatusService from './symbolStatusService'; -/** - * This class shows verification tasks through the VSCode testing UI. - */ +// TODO merge with VerificationGutterStatusView export default class GutterIconsView { public constructor( private readonly languageClient: DafnyLanguageClient, private readonly gutterViewUi: VerificationGutterStatusView, - private readonly symbolStatusView: VerificationSymbolStatusView) + private readonly symbolStatusService: SymbolStatusService) { languageClient.onPublishDiagnostics((uri) => { this.update(uri); }); - symbolStatusView.onUpdates(uri => { - this.update(uri); + symbolStatusService.onUpdates(params => { + this.update(Uri.parse(params.uri)); }); } @@ -32,7 +31,7 @@ export default class GutterIconsView { } const nameToSymbolRange = this.getNameToSymbolRange(rootSymbols); const diagnostics = languages.getDiagnostics(uri); - const symbolStatus = this.symbolStatusView.getUpdatesForFile(uri.toString()); + const symbolStatus = this.symbolStatusService.getUpdatesForFile(uri.toString()); const icons = await this.computeNewGutterIcons(uri, nameToSymbolRange, symbolStatus?.namedVerifiables, diagnostics); this.gutterViewUi.updateVerificationStatusGutter(icons, false); diff --git a/src/ui/symbolStatusService.ts b/src/ui/symbolStatusService.ts new file mode 100644 index 00000000..64c430c6 --- /dev/null +++ b/src/ui/symbolStatusService.ts @@ -0,0 +1,29 @@ +import { ExtensionContext, Event, EventEmitter } from 'vscode'; +import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; +import { IVerificationSymbolStatusParams } from '../language/api/verificationSymbolStatusParams'; + + +/** + * This class shows verification tasks through the VSCode testing UI. + */ +export default class SymbolStatusService { + private readonly updatesPerFile: Map = new Map(); + private readonly _onUpdates: EventEmitter = new EventEmitter(); + public onUpdates: Event = this._onUpdates.event; + + public constructor( + context: ExtensionContext, + languageClient: DafnyLanguageClient) { + + context.subscriptions.push( + languageClient.onVerificationSymbolStatus(params => { + this.updatesPerFile.set(params.uri, params); + this._onUpdates.fire(params); + }) + ); + } + + public getUpdatesForFile(uri: string): IVerificationSymbolStatusParams | undefined { + return this.updatesPerFile.get(uri); + } +} \ No newline at end of file diff --git a/src/ui/verificationSymbolStatusView.ts b/src/ui/verificationSymbolStatusView.ts index b56edcc1..b06eed0d 100644 --- a/src/ui/verificationSymbolStatusView.ts +++ b/src/ui/verificationSymbolStatusView.ts @@ -1,11 +1,11 @@ /* eslint-disable max-depth */ import { commands, ExtensionContext, workspace, tests, Range, Position, Uri, - TestRunRequest, TestController, TestRun, DocumentSymbol, TestItem, TestItemCollection, TextDocument, TestRunProfileKind, window, - Event, EventEmitter } from 'vscode'; + TestRunRequest, TestController, TestRun, DocumentSymbol, TestItem, TestItemCollection, TextDocument, TestRunProfileKind, window } from 'vscode'; import { Range as lspRange, Position as lspPosition } from 'vscode-languageclient'; import { IVerificationSymbolStatusParams, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; import CompilationStatusView from './compilationStatusView'; +import SymbolStatusService from './symbolStatusService'; interface ResolveablePromise { promise: Promise; @@ -17,13 +17,6 @@ interface ItemRunState { startedRunningTime?: number; } -export function createAndRegister( - context: ExtensionContext, - languageClient: DafnyLanguageClient, - compilationStatusView: CompilationStatusView): VerificationSymbolStatusView { - return new VerificationSymbolStatusView(context, languageClient, compilationStatusView); -} - /** * This class shows verification tasks through the VSCode testing UI. */ @@ -32,8 +25,9 @@ export default class VerificationSymbolStatusView { public static createAndRegister( context: ExtensionContext, languageClient: DafnyLanguageClient, + symbolStatusService: SymbolStatusService, compilationStatusView: CompilationStatusView): VerificationSymbolStatusView { - return new VerificationSymbolStatusView(context, languageClient, compilationStatusView); + return new VerificationSymbolStatusView(context, languageClient, symbolStatusService, compilationStatusView); } private itemStates: Map = new Map(); @@ -44,12 +38,11 @@ export default class VerificationSymbolStatusView { private readonly controller: TestController; private automaticRunEnd: boolean = false; private noRunCreationInProgress: Promise = Promise.resolve(); - private readonly _onUpdates: EventEmitter = new EventEmitter(); - public onUpdates: Event = this._onUpdates.event; public constructor( private readonly context: ExtensionContext, private readonly languageClient: DafnyLanguageClient, + symbolStatusService: SymbolStatusService, private readonly compilationStatusView: CompilationStatusView) { this.controller = this.createController(); context.subscriptions.push(this.controller); @@ -73,7 +66,7 @@ export default class VerificationSymbolStatusView { this.updatesPerFile.delete(uriString); }, this, context.subscriptions); context.subscriptions.push( - languageClient.onVerificationSymbolStatus(params => this.update(params)), + symbolStatusService.onUpdates(params => this.update(params)), languageClient.onCompilationStatus(params => compilationStatusView.compilationStatusChangedForBefore38(params)) ); window.onDidChangeActiveTextEditor(e => { @@ -88,10 +81,6 @@ export default class VerificationSymbolStatusView { }); } - public getUpdatesForFile(uri: string): IVerificationSymbolStatusParams | undefined { - return this.updatesPerFile.get(uri); - } - private createController(): TestController { const controller = tests.createTestController('verificationStatus', 'Verification Status'); controller.createRunProfile('Verify', TestRunProfileKind.Run, async (request) => { @@ -161,8 +150,8 @@ export default class VerificationSymbolStatusView { } private async update(params: IVerificationSymbolStatusParams): Promise { - await this.noRunCreationInProgress; const uri = Uri.parse(params.uri); + await this.noRunCreationInProgress; params.uri = uri.toString(); const document = await workspace.openTextDocument(uri); const rootSymbols = await commands.executeCommand('vscode.executeDocumentSymbolProvider', uri) as DocumentSymbol[] | undefined; @@ -178,8 +167,6 @@ export default class VerificationSymbolStatusView { document: TextDocument, rootSymbols: DocumentSymbol[] | undefined) { - this.updatesPerFile.set(params.uri, params); - this._onUpdates.fire(document.uri); if(window.activeTextEditor?.document.uri.toString() !== params.uri.toString()) { return; } From 50ec76355764d0f395e645d42272c83d5f401f8a Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Aug 2023 16:28:41 +0200 Subject: [PATCH 09/30] Add test for computeGutterIcons and fix bugs --- src/test/suite/extension.test.ts | 79 ++++++++++++++++++++++++++++++++ src/ui/gutterIconsView.ts | 22 ++++----- 2 files changed, 90 insertions(+), 11 deletions(-) diff --git a/src/test/suite/extension.test.ts b/src/test/suite/extension.test.ts index 3aaec575..5c231be3 100644 --- a/src/test/suite/extension.test.ts +++ b/src/test/suite/extension.test.ts @@ -13,6 +13,10 @@ import { Messages } from '../../ui/messages'; import { DafnyCommands } from '../../commands'; import VerificationGutterStatusView from '../../ui/verificationGutterStatusView'; import { DocumentSymbol } from 'vscode'; +import GutterIconsView from '../../ui/gutterIconsView'; +import { PublishedVerificationStatus } from '../../language/api/verificationSymbolStatusParams'; +import { LineVerificationStatus } from '../../language/api/verificationGutterStatusParams'; +import exp = require('constants'); const mockedWorkspace = MockingUtils.mockedWorkspace(); const mockedVsCode = { @@ -143,6 +147,81 @@ suite('Verification Gutter', () => { assert.deepStrictEqual([ new vscode.Range(7, 1, 8, 1) ], ranges.get(2)); assert.deepStrictEqual([ new vscode.Range(3, 1, 3, 1), new vscode.Range(5, 1, 5, 1) ], ranges.get(0)); }); + + test('computeResolvedGutterIcons', () => { + /* + method Foo() { // Stale + assert false; // No error + } + + method Bat() { // Stale + assert false; // Outdated error + } + + method Bar() { // Queued + assert false; + } + + method Baz() { // Running + assert false; + } + + method Fom() { // Correct + assert true; + } + + method Faz() { // Error + assert true; + assert false; // Error + } + */ + const computedIcons = GutterIconsView.computeGutterIcons(24, new Map([ + [ '0,7', new vscode.Range(0, 0, 2, 1) ], + [ '4,7', new vscode.Range(4, 0, 6, 1) ], + [ '8,7', new vscode.Range(8, 0, 10, 1) ], + [ '12,7', new vscode.Range(12, 0, 14, 1) ], + [ '16,7', new vscode.Range(16, 0, 18, 1) ], + [ '20,7', new vscode.Range(20, 0, 23, 1) ] + ]), [ + { nameRange: new vscode.Range(0, 7, 0, 10), status: PublishedVerificationStatus.Stale }, + { nameRange: new vscode.Range(4, 7, 4, 10), status: PublishedVerificationStatus.Stale }, + { nameRange: new vscode.Range(8, 7, 8, 10), status: PublishedVerificationStatus.Queued }, + { nameRange: new vscode.Range(12, 7, 12, 10), status: PublishedVerificationStatus.Running }, + { nameRange: new vscode.Range(16, 7, 16, 10), status: PublishedVerificationStatus.Correct }, + { nameRange: new vscode.Range(20, 7, 20, 10), status: PublishedVerificationStatus.Error } + ], [ + new vscode.Diagnostic(new vscode.Range(5, 2, 5, 14), 'Outdated, could not prove assertion', vscode.DiagnosticSeverity.Error), + new vscode.Diagnostic(new vscode.Range(17, 2, 17, 14), 'some warning', vscode.DiagnosticSeverity.Warning), + new vscode.Diagnostic(new vscode.Range(22, 2, 22, 14), 'could not prove assertion', vscode.DiagnosticSeverity.Error) + ]); + const expected = [ + LineVerificationStatus.Nothing, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.Verified, + LineVerificationStatus.Nothing, + LineVerificationStatus.AssertionFailedObsolete, + LineVerificationStatus.ErrorContextObsolete, + LineVerificationStatus.Verified, + LineVerificationStatus.Nothing, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.Verified, + LineVerificationStatus.Nothing, + LineVerificationStatus.VerifiedVerifying, + LineVerificationStatus.VerifiedVerifying, + LineVerificationStatus.Verified, + LineVerificationStatus.Nothing, + LineVerificationStatus.Verified, + LineVerificationStatus.Verified, + LineVerificationStatus.Verified, + LineVerificationStatus.Nothing, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.AssertionFailed, + LineVerificationStatus.ErrorContext + ]; + assert.strictEqual(expected, computedIcons); + }); }); suite('commands', () => { diff --git a/src/ui/gutterIconsView.ts b/src/ui/gutterIconsView.ts index 11e5ad63..2754cb74 100644 --- a/src/ui/gutterIconsView.ts +++ b/src/ui/gutterIconsView.ts @@ -2,7 +2,7 @@ /* eslint-disable @typescript-eslint/brace-style */ import { Diagnostic, DiagnosticSeverity, DocumentSymbol, Range, Uri, languages, commands, workspace, Position } from 'vscode'; import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; -import { IVerificationGutterStatusParams, LineVerificationStatus } from '../language/api/verificationGutterStatusParams'; +import { LineVerificationStatus } from '../language/api/verificationGutterStatusParams'; import { NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; import VerificationSymbolStatusView from './verificationSymbolStatusView'; import VerificationGutterStatusView from './verificationGutterStatusView'; @@ -33,8 +33,9 @@ export default class GutterIconsView { const diagnostics = languages.getDiagnostics(uri); const symbolStatus = this.symbolStatusService.getUpdatesForFile(uri.toString()); - const icons = await this.computeNewGutterIcons(uri, nameToSymbolRange, symbolStatus?.namedVerifiables, diagnostics); - this.gutterViewUi.updateVerificationStatusGutter(icons, false); + const document = await workspace.openTextDocument(uri); + const perLineStatus = GutterIconsView.computeGutterIcons(document.lineCount, nameToSymbolRange, symbolStatus?.namedVerifiables, diagnostics); + this.gutterViewUi.updateVerificationStatusGutter({ uri: uri.toString(), perLineStatus: perLineStatus }, false); } private getNameToSymbolRange(rootSymbols: DocumentSymbol[]): Map { @@ -52,13 +53,12 @@ export default class GutterIconsView { /* No support for first-time icons yet. For first time we pretend like the symbol was previously verified. */ - private async computeNewGutterIcons( - uri: Uri, + public static computeGutterIcons( + lineCount: number, nameToSymbolRanges: Map | undefined, statuses: NamedVerifiableStatus[] | undefined, - diagnostics: Diagnostic[]): Promise + diagnostics: Diagnostic[]): LineVerificationStatus[] { - const document = await workspace.openTextDocument(uri); const statusPerLine = new Map(); const lineToErrorSource = new Map(); const lineToSymbolRange = new Map(); @@ -83,14 +83,14 @@ export default class GutterIconsView { if(contextRange === undefined) { continue; } - for(let contextLine = contextRange.start.line; line < contextRange.end.line; line++) { + for(let contextLine = contextRange.start.line; contextLine <= contextRange.end.line; contextLine++) { linesInErrorContext.add(contextLine); } } } if(nameToSymbolRanges === undefined || statuses === undefined) { - for(let line = 0; line < document.lineCount; line++) { + for(let line = 0; line < lineCount; line++) { statusPerLine.set(line, PublishedVerificationStatus.Stale); } } else { @@ -107,7 +107,7 @@ export default class GutterIconsView { } } } - for(let line = 0; line < document.lineCount; line++) { + for(let line = 0; line < lineCount; line++) { if(linesToSkip.has(line)) { perLineStatus.push(LineVerificationStatus.Nothing); continue; @@ -146,7 +146,7 @@ export default class GutterIconsView { perLineStatus.push(resultStatus + progressStatus); } } - return { uri: uri.toString(), perLineStatus: perLineStatus }; + return perLineStatus; } } From 151e8797b78365dba23fc44157c61c0fd32fd82f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Aug 2023 16:34:39 +0200 Subject: [PATCH 10/30] Add test for computing gutter icons when there is parse error --- src/test/suite/extension.test.ts | 37 +++++++++++++++++++++++++++++++- src/ui/gutterIconsView.ts | 5 +---- 2 files changed, 37 insertions(+), 5 deletions(-) diff --git a/src/test/suite/extension.test.ts b/src/test/suite/extension.test.ts index 5c231be3..e1b19be9 100644 --- a/src/test/suite/extension.test.ts +++ b/src/test/suite/extension.test.ts @@ -148,7 +148,42 @@ suite('Verification Gutter', () => { assert.deepStrictEqual([ new vscode.Range(3, 1, 3, 1), new vscode.Range(5, 1, 5, 1) ], ranges.get(0)); }); - test('computeResolvedGutterIcons', () => { + test.only('computeGutterIconsParseError', () => { + /* + method Foo() { + parse(;)Error + } + + method Bat() { + assert false; // Outdated error + } + + method Fom() { + assert true; + } + */ + const parseError = new vscode.Diagnostic(new vscode.Range(1, 2, 1, 15), 'Some parse error', vscode.DiagnosticSeverity.Error); + parseError.source = 'Parser'; + const computedIcons = GutterIconsView.computeGutterIcons(10, undefined, undefined, [ + parseError, + new vscode.Diagnostic(new vscode.Range(5, 2, 5, 14), 'Outdated: could not prove assertion', vscode.DiagnosticSeverity.Error) + ]); + const expected = [ + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.ResolutionError, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.AssertionFailedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete + ]; + assert.strictEqual(expected, computedIcons); + }); + + test('computeGutterIconsResolved', () => { /* method Foo() { // Stale assert false; // No error diff --git a/src/ui/gutterIconsView.ts b/src/ui/gutterIconsView.ts index 2754cb74..4470cf3b 100644 --- a/src/ui/gutterIconsView.ts +++ b/src/ui/gutterIconsView.ts @@ -26,10 +26,7 @@ export default class GutterIconsView { private async update(uri: Uri) { const rootSymbols = await commands.executeCommand('vscode.executeDocumentSymbolProvider', uri) as DocumentSymbol[] | undefined; - if(rootSymbols === undefined) { - return; - } - const nameToSymbolRange = this.getNameToSymbolRange(rootSymbols); + const nameToSymbolRange = rootSymbols === undefined ? undefined : this.getNameToSymbolRange(rootSymbols); const diagnostics = languages.getDiagnostics(uri); const symbolStatus = this.symbolStatusService.getUpdatesForFile(uri.toString()); From c777d946f8956e7681d0bb767b7ee8902df2e848 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Aug 2023 16:39:24 +0200 Subject: [PATCH 11/30] Combine similar classes --- src/test/suite/extension.test.ts | 8 +- src/ui/dafnyIntegration.ts | 4 +- src/ui/gutterIconsView.ts | 158 ------------------------- src/ui/verificationGutterStatusView.ts | 152 +++++++++++++++++++++++- 4 files changed, 152 insertions(+), 170 deletions(-) delete mode 100644 src/ui/gutterIconsView.ts diff --git a/src/test/suite/extension.test.ts b/src/test/suite/extension.test.ts index e1b19be9..78e06ce8 100644 --- a/src/test/suite/extension.test.ts +++ b/src/test/suite/extension.test.ts @@ -13,10 +13,8 @@ import { Messages } from '../../ui/messages'; import { DafnyCommands } from '../../commands'; import VerificationGutterStatusView from '../../ui/verificationGutterStatusView'; import { DocumentSymbol } from 'vscode'; -import GutterIconsView from '../../ui/gutterIconsView'; import { PublishedVerificationStatus } from '../../language/api/verificationSymbolStatusParams'; import { LineVerificationStatus } from '../../language/api/verificationGutterStatusParams'; -import exp = require('constants'); const mockedWorkspace = MockingUtils.mockedWorkspace(); const mockedVsCode = { @@ -148,7 +146,7 @@ suite('Verification Gutter', () => { assert.deepStrictEqual([ new vscode.Range(3, 1, 3, 1), new vscode.Range(5, 1, 5, 1) ], ranges.get(0)); }); - test.only('computeGutterIconsParseError', () => { + test('computeGutterIconsParseError', () => { /* method Foo() { parse(;)Error @@ -164,7 +162,7 @@ suite('Verification Gutter', () => { */ const parseError = new vscode.Diagnostic(new vscode.Range(1, 2, 1, 15), 'Some parse error', vscode.DiagnosticSeverity.Error); parseError.source = 'Parser'; - const computedIcons = GutterIconsView.computeGutterIcons(10, undefined, undefined, [ + const computedIcons = VerificationGutterStatusView.computeGutterIcons(10, undefined, undefined, [ parseError, new vscode.Diagnostic(new vscode.Range(5, 2, 5, 14), 'Outdated: could not prove assertion', vscode.DiagnosticSeverity.Error) ]); @@ -210,7 +208,7 @@ suite('Verification Gutter', () => { assert false; // Error } */ - const computedIcons = GutterIconsView.computeGutterIcons(24, new Map([ + const computedIcons = VerificationGutterStatusView.computeGutterIcons(24, new Map([ [ '0,7', new vscode.Range(0, 0, 2, 1) ], [ '4,7', new vscode.Range(4, 0, 6, 1) ], [ '8,7', new vscode.Range(8, 0, 10, 1) ], diff --git a/src/ui/dafnyIntegration.ts b/src/ui/dafnyIntegration.ts index 9ea99beb..131c9689 100644 --- a/src/ui/dafnyIntegration.ts +++ b/src/ui/dafnyIntegration.ts @@ -10,7 +10,6 @@ import VerificationSymbolStatusView from './verificationSymbolStatusView'; import Configuration from '../configuration'; import { ConfigurationConstants, LanguageServerConstants } from '../constants'; import { DafnyInstaller } from '../language/dafnyInstallation'; -import GutterIconsView from './gutterIconsView'; import SymbolStatusService from './symbolStatusService'; export default function createAndRegisterDafnyIntegration( @@ -35,8 +34,7 @@ export default function createAndRegisterDafnyIntegration( } const displayGutterStatus = Configuration.get(ConfigurationConstants.LanguageServer.DisplayGutterStatus); if(displayGutterStatus) { - const gutterViewUi = VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); - new GutterIconsView(languageClient, gutterViewUi, symbolStatusService); + VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusService, symbolStatusView); } CompileCommands.createAndRegister(installer); RelatedErrorView.createAndRegister(installer.context, languageClient); diff --git a/src/ui/gutterIconsView.ts b/src/ui/gutterIconsView.ts deleted file mode 100644 index 4470cf3b..00000000 --- a/src/ui/gutterIconsView.ts +++ /dev/null @@ -1,158 +0,0 @@ -/* eslint-disable max-depth */ -/* eslint-disable @typescript-eslint/brace-style */ -import { Diagnostic, DiagnosticSeverity, DocumentSymbol, Range, Uri, languages, commands, workspace, Position } from 'vscode'; -import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; -import { LineVerificationStatus } from '../language/api/verificationGutterStatusParams'; -import { NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; -import VerificationSymbolStatusView from './verificationSymbolStatusView'; -import VerificationGutterStatusView from './verificationGutterStatusView'; -import SymbolStatusService from './symbolStatusService'; - -// TODO merge with VerificationGutterStatusView -export default class GutterIconsView { - - public constructor( - private readonly languageClient: DafnyLanguageClient, - private readonly gutterViewUi: VerificationGutterStatusView, - private readonly symbolStatusService: SymbolStatusService) - { - languageClient.onPublishDiagnostics((uri) => { - this.update(uri); - }); - symbolStatusService.onUpdates(params => { - this.update(Uri.parse(params.uri)); - }); - } - - private async update(uri: Uri) { - const rootSymbols = await commands.executeCommand('vscode.executeDocumentSymbolProvider', uri) as DocumentSymbol[] | undefined; - const nameToSymbolRange = rootSymbols === undefined ? undefined : this.getNameToSymbolRange(rootSymbols); - const diagnostics = languages.getDiagnostics(uri); - const symbolStatus = this.symbolStatusService.getUpdatesForFile(uri.toString()); - - const document = await workspace.openTextDocument(uri); - const perLineStatus = GutterIconsView.computeGutterIcons(document.lineCount, nameToSymbolRange, symbolStatus?.namedVerifiables, diagnostics); - this.gutterViewUi.updateVerificationStatusGutter({ uri: uri.toString(), perLineStatus: perLineStatus }, false); - } - - private getNameToSymbolRange(rootSymbols: DocumentSymbol[]): Map { - const result = new Map(); - const stack = rootSymbols; - while(stack.length > 0) { - const top = stack.pop()!; - const children = top.children ?? []; - stack.push(...children); - result.set(positionToString(top.selectionRange.start), top.range); - } - return result; - } - - /* - No support for first-time icons yet. For first time we pretend like the symbol was previously verified. - */ - public static computeGutterIcons( - lineCount: number, - nameToSymbolRanges: Map | undefined, - statuses: NamedVerifiableStatus[] | undefined, - diagnostics: Diagnostic[]): LineVerificationStatus[] - { - const statusPerLine = new Map(); - const lineToErrorSource = new Map(); - const lineToSymbolRange = new Map(); - const linesInErrorContext = new Set(); - const linesToSkip = new Set(); - - if(nameToSymbolRanges !== undefined) { - for(const range of nameToSymbolRanges.values()) { - for(let line = range.start.line; line < range.end.line; line++) { - lineToSymbolRange.set(line, range); - } - } - } - const perLineStatus: LineVerificationStatus[] = []; - for(const diagnostic of diagnostics) { - if(diagnostic.severity !== DiagnosticSeverity.Error) { - continue; - } - for(let line = diagnostic.range.start.line; line <= diagnostic.range.end.line; line++) { - lineToErrorSource.set(line, diagnostic.source ?? ''); - const contextRange = lineToSymbolRange.get(line); - if(contextRange === undefined) { - continue; - } - for(let contextLine = contextRange.start.line; contextLine <= contextRange.end.line; contextLine++) { - linesInErrorContext.add(contextLine); - } - } - } - - if(nameToSymbolRanges === undefined || statuses === undefined) { - for(let line = 0; line < lineCount; line++) { - statusPerLine.set(line, PublishedVerificationStatus.Stale); - } - } else { - for(const status of statuses) { - const convertedRange = VerificationSymbolStatusView.convertRange(status.nameRange); - const symbolRange = nameToSymbolRanges.get(positionToString(convertedRange.start)); - linesToSkip.add(convertedRange.start.line); - if(symbolRange === undefined) { - console.error('symbol mismatch between documentSymbol and symbolStatus API'); - continue; - } - for(let line = symbolRange.start.line; line <= symbolRange.end.line; line++) { - statusPerLine.set(line, status.status); - } - } - } - for(let line = 0; line < lineCount; line++) { - if(linesToSkip.has(line)) { - perLineStatus.push(LineVerificationStatus.Nothing); - continue; - } - - const error = lineToErrorSource.get(line); - if(error === 'Parser' || error === 'Resolver') { - perLineStatus.push(LineVerificationStatus.ResolutionError); - } else { - let resultStatus: number; - if(error !== undefined) { - resultStatus = LineVerificationStatus.AssertionFailed; - } else { - if(linesInErrorContext.has(line)) { - resultStatus = LineVerificationStatus.ErrorContext; - } else { - resultStatus = LineVerificationStatus.Verified; - } - } - let progressStatus: number; - switch(statusPerLine.get(line)) { - case PublishedVerificationStatus.Stale: - case PublishedVerificationStatus.Queued: - progressStatus = GutterIconProgress.Stale; - break; - case PublishedVerificationStatus.Running: - progressStatus = GutterIconProgress.Running; - break; - case PublishedVerificationStatus.Error: - case PublishedVerificationStatus.Correct: - case undefined: - progressStatus = GutterIconProgress.Done; - break; - default: throw new Error(`unknown PublishedVerificationStatus ${statusPerLine.get(line)}`); - } - perLineStatus.push(resultStatus + progressStatus); - } - } - return perLineStatus; - } -} - -export enum GutterIconProgress { - Stale = 1, - Running = 2, - Done = 0 -} - -function positionToString(start: Position): string { - return `${start.line},${start.character}`; -} diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index fc3d66c1..555b9295 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -1,5 +1,5 @@ /* eslint-disable max-depth */ -import { Range, window, ExtensionContext, workspace, TextEditor, TextEditorDecorationType, Uri } from 'vscode'; +import { Range, window, ExtensionContext, workspace, TextEditor, TextEditorDecorationType, Uri, Position, DocumentSymbol, Diagnostic, DiagnosticSeverity, commands, languages } from 'vscode'; import { Disposable } from 'vscode-languageclient'; import { IVerificationGutterStatusParams, @@ -11,6 +11,8 @@ import { import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; import { getVsDocumentPath } from '../tools/vscode'; import VerificationSymbolStatusView from './verificationSymbolStatusView'; +import { NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; +import SymbolStatusService from './symbolStatusService'; const DELAY_IF_RESOLUTION_ERROR = 2000; const ANIMATION_INTERVAL = 200; @@ -57,7 +59,9 @@ export default class VerificationGutterStatusView { private static readonly emptyLinearVerificationDiagnostics: Map = VerificationGutterStatusView.FillLineVerificationStatusMap(); - private constructor(context: ExtensionContext, private readonly symbolStatusView: VerificationSymbolStatusView | undefined) { + private constructor(context: ExtensionContext, + private readonly symbolStatusService: SymbolStatusService, + private readonly symbolStatusView: VerificationSymbolStatusView | undefined) { const icon = VerificationGutterStatusView.makeIconAux(false, context); const grayIcon = VerificationGutterStatusView.makeIconAux(true, context); const lvs = LineVerificationStatus; @@ -112,8 +116,17 @@ export default class VerificationGutterStatusView { public static createAndRegister( context: ExtensionContext, languageClient: DafnyLanguageClient, + symbolStatusService: SymbolStatusService, symbolStatusView: VerificationSymbolStatusView | undefined): VerificationGutterStatusView { - const instance = new VerificationGutterStatusView(context, symbolStatusView); + const instance = new VerificationGutterStatusView(context, symbolStatusService, symbolStatusView); + languageClient.onPublishDiagnostics((uri) => { + instance.update(uri); + }); + symbolStatusService.onUpdates(params => { + instance.update(Uri.parse(params.uri)); + }); + + context.subscriptions.push( workspace.onDidCloseTextDocument(document => instance.clearVerificationDiagnostics(document.uri.toString())), window.onDidChangeActiveTextEditor(editor => instance.refreshDisplayedVerificationGutterStatuses(editor)), @@ -122,6 +135,127 @@ export default class VerificationGutterStatusView { return instance; } + private async update(uri: Uri) { + const rootSymbols = await commands.executeCommand('vscode.executeDocumentSymbolProvider', uri) as DocumentSymbol[] | undefined; + const nameToSymbolRange = rootSymbols === undefined ? undefined : this.getNameToSymbolRange(rootSymbols); + const diagnostics = languages.getDiagnostics(uri); + const symbolStatus = this.symbolStatusService.getUpdatesForFile(uri.toString()); + + const document = await workspace.openTextDocument(uri); + const perLineStatus = VerificationGutterStatusView.computeGutterIcons(document.lineCount, nameToSymbolRange, symbolStatus?.namedVerifiables, diagnostics); + this.updateVerificationStatusGutter({ uri: uri.toString(), perLineStatus: perLineStatus }, false); + } + + private getNameToSymbolRange(rootSymbols: DocumentSymbol[]): Map { + const result = new Map(); + const stack = rootSymbols; + while(stack.length > 0) { + const top = stack.pop()!; + const children = top.children ?? []; + stack.push(...children); + result.set(positionToString(top.selectionRange.start), top.range); + } + return result; + } + + /* + No support for first-time icons yet. For first time we pretend like the symbol was previously verified. + */ + public static computeGutterIcons( + lineCount: number, + nameToSymbolRanges: Map | undefined, + statuses: NamedVerifiableStatus[] | undefined, + diagnostics: Diagnostic[]): LineVerificationStatus[] { + const statusPerLine = new Map(); + const lineToErrorSource = new Map(); + const lineToSymbolRange = new Map(); + const linesInErrorContext = new Set(); + const linesToSkip = new Set(); + + if(nameToSymbolRanges !== undefined) { + for(const range of nameToSymbolRanges.values()) { + for(let line = range.start.line; line < range.end.line; line++) { + lineToSymbolRange.set(line, range); + } + } + } + const perLineStatus: LineVerificationStatus[] = []; + for(const diagnostic of diagnostics) { + if(diagnostic.severity !== DiagnosticSeverity.Error) { + continue; + } + for(let line = diagnostic.range.start.line; line <= diagnostic.range.end.line; line++) { + lineToErrorSource.set(line, diagnostic.source ?? ''); + const contextRange = lineToSymbolRange.get(line); + if(contextRange === undefined) { + continue; + } + for(let contextLine = contextRange.start.line; contextLine <= contextRange.end.line; contextLine++) { + linesInErrorContext.add(contextLine); + } + } + } + + if(nameToSymbolRanges === undefined || statuses === undefined) { + for(let line = 0; line < lineCount; line++) { + statusPerLine.set(line, PublishedVerificationStatus.Stale); + } + } else { + for(const status of statuses) { + const convertedRange = VerificationSymbolStatusView.convertRange(status.nameRange); + const symbolRange = nameToSymbolRanges.get(positionToString(convertedRange.start)); + linesToSkip.add(convertedRange.start.line); + if(symbolRange === undefined) { + console.error('symbol mismatch between documentSymbol and symbolStatus API'); + continue; + } + for(let line = symbolRange.start.line; line <= symbolRange.end.line; line++) { + statusPerLine.set(line, status.status); + } + } + } + for(let line = 0; line < lineCount; line++) { + if(linesToSkip.has(line)) { + perLineStatus.push(LineVerificationStatus.Nothing); + continue; + } + + const error = lineToErrorSource.get(line); + if(error === 'Parser' || error === 'Resolver') { + perLineStatus.push(LineVerificationStatus.ResolutionError); + } else { + let resultStatus: number; + if(error !== undefined) { + resultStatus = LineVerificationStatus.AssertionFailed; + } else { + if(linesInErrorContext.has(line)) { + resultStatus = LineVerificationStatus.ErrorContext; + } else { + resultStatus = LineVerificationStatus.Verified; + } + } + let progressStatus: number; + switch(statusPerLine.get(line)) { + case PublishedVerificationStatus.Stale: + case PublishedVerificationStatus.Queued: + progressStatus = GutterIconProgress.Stale; + break; + case PublishedVerificationStatus.Running: + progressStatus = GutterIconProgress.Running; + break; + case PublishedVerificationStatus.Error: + case PublishedVerificationStatus.Correct: + case undefined: + progressStatus = GutterIconProgress.Done; + break; + default: throw new Error(`unknown PublishedVerificationStatus ${statusPerLine.get(line)}`); + } + perLineStatus.push(resultStatus + progressStatus); + } + } + return perLineStatus; + } + /// Creation of an decoration type private static iconOf(context: ExtensionContext, path: string, grayMode: boolean): TextEditorDecorationType { const icon = context.asAbsolutePath(`images/${path}.png`); @@ -402,4 +536,14 @@ export default class VerificationGutterStatusView { } } } -} \ No newline at end of file +} + +export enum GutterIconProgress { + Stale = 1, + Running = 2, + Done = 0 +} + +function positionToString(start: Position): string { + return `${start.line},${start.character}`; +} From b929ec8bcd331d4f394b1e723b435ed793d0b40c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Aug 2023 16:40:31 +0200 Subject: [PATCH 12/30] Remove comment --- src/ui/verificationGutterStatusView.ts | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 555b9295..9486c3f6 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -158,9 +158,6 @@ export default class VerificationGutterStatusView { return result; } - /* - No support for first-time icons yet. For first time we pretend like the symbol was previously verified. - */ public static computeGutterIcons( lineCount: number, nameToSymbolRanges: Map | undefined, From c3b1cde28b84fb22519aa3f051dbc6f7b898cf28 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Aug 2023 16:45:57 +0200 Subject: [PATCH 13/30] Fix tests --- src/test/suite/extension.test.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/test/suite/extension.test.ts b/src/test/suite/extension.test.ts index 78e06ce8..aca33cbc 100644 --- a/src/test/suite/extension.test.ts +++ b/src/test/suite/extension.test.ts @@ -178,7 +178,7 @@ suite('Verification Gutter', () => { LineVerificationStatus.VerifiedObsolete, LineVerificationStatus.VerifiedObsolete ]; - assert.strictEqual(expected, computedIcons); + assert.equal(expected, computedIcons); }); test('computeGutterIconsResolved', () => { @@ -253,7 +253,7 @@ suite('Verification Gutter', () => { LineVerificationStatus.AssertionFailed, LineVerificationStatus.ErrorContext ]; - assert.strictEqual(expected, computedIcons); + assert.equal(expected, computedIcons); }); }); From c4ecc2811d8cfdb5dc21e4ea7ebfb54d02072c21 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Aug 2023 17:24:06 +0200 Subject: [PATCH 14/30] Fix tests --- src/test/suite/extension.test.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/test/suite/extension.test.ts b/src/test/suite/extension.test.ts index aca33cbc..fcfa1504 100644 --- a/src/test/suite/extension.test.ts +++ b/src/test/suite/extension.test.ts @@ -178,7 +178,7 @@ suite('Verification Gutter', () => { LineVerificationStatus.VerifiedObsolete, LineVerificationStatus.VerifiedObsolete ]; - assert.equal(expected, computedIcons); + assert.deepStrictEqual(expected, computedIcons); }); test('computeGutterIconsResolved', () => { @@ -253,7 +253,7 @@ suite('Verification Gutter', () => { LineVerificationStatus.AssertionFailed, LineVerificationStatus.ErrorContext ]; - assert.equal(expected, computedIcons); + assert.deepStrictEqual(expected, computedIcons); }); }); From 3cd62099553fbe8f19142c4b9fc5b4e57b36db88 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 29 Aug 2023 17:46:58 +0200 Subject: [PATCH 15/30] Update gutter icons if line count changes --- src/ui/verificationGutterStatusView.ts | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 9486c3f6..d5c751e7 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -125,7 +125,11 @@ export default class VerificationGutterStatusView { symbolStatusService.onUpdates(params => { instance.update(Uri.parse(params.uri)); }); - + workspace.onDidChangeTextDocument(e => { + if(instance.lineCountsPerDocument.get(e.document.uri) !== e.document.lineCount) { + instance.update(e.document.uri); + } + }); context.subscriptions.push( workspace.onDidCloseTextDocument(document => instance.clearVerificationDiagnostics(document.uri.toString())), @@ -135,6 +139,7 @@ export default class VerificationGutterStatusView { return instance; } + private readonly lineCountsPerDocument = new Map(); private async update(uri: Uri) { const rootSymbols = await commands.executeCommand('vscode.executeDocumentSymbolProvider', uri) as DocumentSymbol[] | undefined; const nameToSymbolRange = rootSymbols === undefined ? undefined : this.getNameToSymbolRange(rootSymbols); @@ -142,6 +147,8 @@ export default class VerificationGutterStatusView { const symbolStatus = this.symbolStatusService.getUpdatesForFile(uri.toString()); const document = await workspace.openTextDocument(uri); + + this.lineCountsPerDocument.set(document.uri, document.lineCount); const perLineStatus = VerificationGutterStatusView.computeGutterIcons(document.lineCount, nameToSymbolRange, symbolStatus?.namedVerifiables, diagnostics); this.updateVerificationStatusGutter({ uri: uri.toString(), perLineStatus: perLineStatus }, false); } From 3932318878b6a9e50252bab02cf175bec261bfd4 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 4 Sep 2023 11:52:03 +0200 Subject: [PATCH 16/30] Remove onVerificationStatusGutter --- src/language/dafnyLanguageClient.ts | 5 ----- src/ui/verificationGutterStatusView.ts | 1 - 2 files changed, 6 deletions(-) diff --git a/src/language/dafnyLanguageClient.ts b/src/language/dafnyLanguageClient.ts index 4b856695..af5ca3a7 100644 --- a/src/language/dafnyLanguageClient.ts +++ b/src/language/dafnyLanguageClient.ts @@ -7,7 +7,6 @@ import { DafnyDocumentFilter } from '../tools/vscode'; import { ICompilationStatusParams, IVerificationCompletedParams, IVerificationStartedParams } from './api/compilationStatus'; import { ICounterexampleItem, ICounterexampleParams } from './api/counterExample'; import { IGhostDiagnosticsParams } from './api/ghostDiagnostics'; -import { IVerificationGutterStatusParams as IVerificationGutterStatusParams } from './api/verificationGutterStatusParams'; import { IVerificationSymbolStatusParams } from './api/verificationSymbolStatusParams'; import { DafnyInstaller } from './dafnyInstallation'; import * as os from 'os'; @@ -169,10 +168,6 @@ export class DafnyLanguageClient extends LanguageClient { return this.onNotification('dafny/ghost/diagnostics', callback); } - public onVerificationStatusGutter(callback: (params: IVerificationGutterStatusParams) => void): Disposable { - return this.onNotification('dafny/verification/status/gutter', callback); - } - public onVerificationSymbolStatus(callback: (params: IVerificationSymbolStatusParams) => void): Disposable { return this.onNotification('dafny/textDocument/symbolStatus', callback); } diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index fb8f438d..40a11d28 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -126,7 +126,6 @@ export default class VerificationGutterStatusView { context.subscriptions.push( workspace.onDidCloseTextDocument(document => instance.clearVerificationDiagnostics(document.uri.toString())), window.onDidChangeActiveTextEditor(editor => instance.refreshDisplayedVerificationGutterStatuses(editor)), - languageClient.onVerificationStatusGutter(params => instance.updateVerificationStatusGutter(params)), symbolStatusService.onUpdates(params => { instance.update(Uri.parse(params.uri)); From e8eca42f716e0ea848a44c6d60ec45cf93715843 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 4 Sep 2023 11:53:33 +0200 Subject: [PATCH 17/30] Rename --- src/ui/verificationGutterStatusView.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 40a11d28..7c25f767 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -150,7 +150,7 @@ export default class VerificationGutterStatusView { this.lineCountsPerDocument.set(document.uri, document.lineCount); const perLineStatus = VerificationGutterStatusView.computeGutterIcons(document.lineCount, nameToSymbolRange, symbolStatus?.namedVerifiables, diagnostics); - this.updateVerificationStatusGutter({ uri: uri.toString(), perLineStatus: perLineStatus }, false); + this.updateUsingLineStatus({ uri: uri.toString(), perLineStatus: perLineStatus }); } private getNameToSymbolRange(rootSymbols: DocumentSymbol[]): Map { @@ -447,7 +447,7 @@ export default class VerificationGutterStatusView { } // Entry point when receiving IVErificationStatusGutter - private updateVerificationStatusGutter(params: IVerificationGutterStatusParams) { + private updateUsingLineStatus(params: IVerificationGutterStatusParams) { if(this.areParamsOutdated(params)) { return; } From 2d91e8556f391858cdaccbd97e038ee3c1b5a25d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 4 Sep 2023 12:31:38 +0200 Subject: [PATCH 18/30] Now using the ranges from the test item collection to update the gutter icons --- .../api/verificationGutterStatusParams.ts | 1 + src/ui/dafnyIntegration.ts | 6 ++-- src/ui/symbolStatusService.ts | 29 ----------------- src/ui/verificationGutterStatusView.ts | 22 ++++++------- src/ui/verificationSymbolStatusView.ts | 31 ++++++++++++------- 5 files changed, 33 insertions(+), 56 deletions(-) delete mode 100644 src/ui/symbolStatusService.ts diff --git a/src/language/api/verificationGutterStatusParams.ts b/src/language/api/verificationGutterStatusParams.ts index c21a19fa..2cc8230c 100644 --- a/src/language/api/verificationGutterStatusParams.ts +++ b/src/language/api/verificationGutterStatusParams.ts @@ -1,3 +1,4 @@ + import { DocumentUri, integer } from 'vscode-languageclient'; export interface IVerificationGutterStatusParams { diff --git a/src/ui/dafnyIntegration.ts b/src/ui/dafnyIntegration.ts index 131c9689..cf2b9baf 100644 --- a/src/ui/dafnyIntegration.ts +++ b/src/ui/dafnyIntegration.ts @@ -10,7 +10,6 @@ import VerificationSymbolStatusView from './verificationSymbolStatusView'; import Configuration from '../configuration'; import { ConfigurationConstants, LanguageServerConstants } from '../constants'; import { DafnyInstaller } from '../language/dafnyInstallation'; -import SymbolStatusService from './symbolStatusService'; export default function createAndRegisterDafnyIntegration( installer: DafnyInstaller, @@ -22,9 +21,8 @@ export default function createAndRegisterDafnyIntegration( const compilationStatusView = CompilationStatusView.createAndRegister(installer.context, languageClient, languageServerVersion); let symbolStatusView: VerificationSymbolStatusView | undefined = undefined; const serverSupportsSymbolStatusView = configuredVersionToNumeric('3.8.0') <= configuredVersionToNumeric(languageServerVersion); - const symbolStatusService = new SymbolStatusService(installer.context, languageClient); if(serverSupportsSymbolStatusView && Configuration.get(ConfigurationConstants.LanguageServer.DisplayVerificationAsTests)) { - symbolStatusView = VerificationSymbolStatusView.createAndRegister(installer.context, languageClient, symbolStatusService, compilationStatusView); + symbolStatusView = VerificationSymbolStatusView.createAndRegister(installer.context, languageClient, compilationStatusView); } else { if(serverSupportsSymbolStatusView) { compilationStatusView.registerAfter38Messages(); @@ -34,7 +32,7 @@ export default function createAndRegisterDafnyIntegration( } const displayGutterStatus = Configuration.get(ConfigurationConstants.LanguageServer.DisplayGutterStatus); if(displayGutterStatus) { - VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusService, symbolStatusView); + VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); } CompileCommands.createAndRegister(installer); RelatedErrorView.createAndRegister(installer.context, languageClient); diff --git a/src/ui/symbolStatusService.ts b/src/ui/symbolStatusService.ts deleted file mode 100644 index 64c430c6..00000000 --- a/src/ui/symbolStatusService.ts +++ /dev/null @@ -1,29 +0,0 @@ -import { ExtensionContext, Event, EventEmitter } from 'vscode'; -import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; -import { IVerificationSymbolStatusParams } from '../language/api/verificationSymbolStatusParams'; - - -/** - * This class shows verification tasks through the VSCode testing UI. - */ -export default class SymbolStatusService { - private readonly updatesPerFile: Map = new Map(); - private readonly _onUpdates: EventEmitter = new EventEmitter(); - public onUpdates: Event = this._onUpdates.event; - - public constructor( - context: ExtensionContext, - languageClient: DafnyLanguageClient) { - - context.subscriptions.push( - languageClient.onVerificationSymbolStatus(params => { - this.updatesPerFile.set(params.uri, params); - this._onUpdates.fire(params); - }) - ); - } - - public getUpdatesForFile(uri: string): IVerificationSymbolStatusParams | undefined { - return this.updatesPerFile.get(uri); - } -} \ No newline at end of file diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 7c25f767..06b95a2c 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -12,7 +12,6 @@ import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; import { getVsDocumentPath } from '../tools/vscode'; import VerificationSymbolStatusView from './verificationSymbolStatusView'; import { NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; -import SymbolStatusService from './symbolStatusService'; const DELAY_IF_RESOLUTION_ERROR = 2000; const ANIMATION_INTERVAL = 200; @@ -60,7 +59,6 @@ export default class VerificationGutterStatusView { = VerificationGutterStatusView.FillLineVerificationStatusMap(); private constructor(context: ExtensionContext, - private readonly symbolStatusService: SymbolStatusService, private readonly symbolStatusView: VerificationSymbolStatusView | undefined) { const icon = VerificationGutterStatusView.makeIconAux(false, context); const grayIcon = VerificationGutterStatusView.makeIconAux(true, context); @@ -116,9 +114,8 @@ export default class VerificationGutterStatusView { public static createAndRegister( context: ExtensionContext, languageClient: DafnyLanguageClient, - symbolStatusService: SymbolStatusService, symbolStatusView: VerificationSymbolStatusView | undefined): VerificationGutterStatusView { - const instance = new VerificationGutterStatusView(context, symbolStatusService, symbolStatusView); + const instance = new VerificationGutterStatusView(context, symbolStatusView); languageClient.onPublishDiagnostics((uri) => { instance.update(uri); }); @@ -126,16 +123,19 @@ export default class VerificationGutterStatusView { context.subscriptions.push( workspace.onDidCloseTextDocument(document => instance.clearVerificationDiagnostics(document.uri.toString())), window.onDidChangeActiveTextEditor(editor => instance.refreshDisplayedVerificationGutterStatuses(editor)), - - symbolStatusService.onUpdates(params => { - instance.update(Uri.parse(params.uri)); - }), workspace.onDidChangeTextDocument(e => { if(instance.lineCountsPerDocument.get(e.document.uri) !== e.document.lineCount) { instance.update(e.document.uri); } }) ); + if(symbolStatusView !== undefined) { + context.subscriptions.push( + symbolStatusView.onUpdates(uri => { + instance.update(uri); + }) + ); + } return instance; } @@ -144,12 +144,12 @@ export default class VerificationGutterStatusView { const rootSymbols = await commands.executeCommand('vscode.executeDocumentSymbolProvider', uri) as DocumentSymbol[] | undefined; const nameToSymbolRange = rootSymbols === undefined ? undefined : this.getNameToSymbolRange(rootSymbols); const diagnostics = languages.getDiagnostics(uri); - const symbolStatus = this.symbolStatusService.getUpdatesForFile(uri.toString()); + const verifiableRanges = this.symbolStatusView!.getVerifiableRangesForUri(uri); const document = await workspace.openTextDocument(uri); this.lineCountsPerDocument.set(document.uri, document.lineCount); - const perLineStatus = VerificationGutterStatusView.computeGutterIcons(document.lineCount, nameToSymbolRange, symbolStatus?.namedVerifiables, diagnostics); + const perLineStatus = VerificationGutterStatusView.computeGutterIcons(document.lineCount, nameToSymbolRange, verifiableRanges, diagnostics); this.updateUsingLineStatus({ uri: uri.toString(), perLineStatus: perLineStatus }); } @@ -403,7 +403,7 @@ export default class VerificationGutterStatusView { const symbolParams = params.perLineStatus.indexOf(LineVerificationStatus.ResolutionError) > 0 ? [] : (this.symbolStatusView?.getVerifiableRangesForUri(uri) ?? []); - const originalLinesToSkip = symbolParams.map(range => range.start.line).sort((a, b) => a - b); + const originalLinesToSkip = symbolParams.map(range => range.nameRange.start.line).sort((a, b) => a - b); return VerificationGutterStatusView.perLineStatusToRanges(perLineStatus, originalLinesToSkip); } diff --git a/src/ui/verificationSymbolStatusView.ts b/src/ui/verificationSymbolStatusView.ts index bc02b1e0..cf1d761e 100644 --- a/src/ui/verificationSymbolStatusView.ts +++ b/src/ui/verificationSymbolStatusView.ts @@ -1,10 +1,9 @@ /* eslint-disable max-depth */ -import { commands, ExtensionContext, workspace, tests, Range, Position, Uri, TestRunRequest, TestController, TestRun, DocumentSymbol, TestItem, TestItemCollection, TextDocument, TestRunProfileKind } from 'vscode'; +import { commands, ExtensionContext, workspace, Event, tests, Range, Position, Uri, TestRunRequest, TestController, TestRun, DocumentSymbol, TestItem, TestItemCollection, TextDocument, TestRunProfileKind, EventEmitter } from 'vscode'; import { Range as lspRange, Position as lspPosition } from 'vscode-languageclient'; -import { IVerificationSymbolStatusParams, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; +import { IVerificationSymbolStatusParams, NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; import CompilationStatusView from './compilationStatusView'; -import SymbolStatusService from './symbolStatusService'; class ResolveablePromise { private _resolve: (value: T) => void = () => {}; @@ -38,9 +37,8 @@ export default class VerificationSymbolStatusView { public static createAndRegister( context: ExtensionContext, languageClient: DafnyLanguageClient, - symbolStatusService: SymbolStatusService, compilationStatusView: CompilationStatusView): VerificationSymbolStatusView { - return new VerificationSymbolStatusView(context, languageClient, symbolStatusService, compilationStatusView); + return new VerificationSymbolStatusView(context, languageClient, compilationStatusView); } private itemStates: Map = new Map(); @@ -49,17 +47,20 @@ export default class VerificationSymbolStatusView { private readonly controller: TestController; private automaticRunEnd: boolean = false; private noRunCreationInProgress: Promise = Promise.resolve(); + private readonly _onUpdates: EventEmitter = new EventEmitter(); + public onUpdates: Event = this._onUpdates.event; public constructor( private readonly context: ExtensionContext, private readonly languageClient: DafnyLanguageClient, - symbolStatusService: SymbolStatusService, private readonly compilationStatusView: CompilationStatusView) { this.controller = this.createController(); context.subscriptions.push(this.controller); context.subscriptions.push( - symbolStatusService.onUpdates(params => this.update(params)), + languageClient.onVerificationSymbolStatus(params => { + this.update(params); + }), languageClient.onCompilationStatus(params => compilationStatusView.compilationStatusChangedForBefore38(params)) ); } @@ -176,6 +177,7 @@ export default class VerificationSymbolStatusView { controller.items.add(leafItem); } } + this._onUpdates.fire(document.uri); const allTestItems: TestItem[] = []; function collectTestItems(collection: TestItemCollection) { @@ -202,6 +204,8 @@ export default class VerificationSymbolStatusView { const newItemRuns = new Map(); params.namedVerifiables.forEach((element, index) => { const testItem = leafItems[index]; + this.statuses.set(testItem.id, element.status); + const itemRunState = this.itemRuns.get(testItem.id)!; if(this.itemStates.get(testItem.id) === element.status) { const isRunning = itemRunState !== undefined; @@ -330,15 +334,18 @@ export default class VerificationSymbolStatusView { return new Position(position.line, position.character); } - public getVerifiableRangesForUri(uri: Uri): Range[] { + private readonly statuses: Map = new Map(); + + public getVerifiableRangesForUri(uri: Uri): NamedVerifiableStatus[] { const stack: TestItemCollection[] = [ this.controller.items ]; - const ranges: Range[] = []; + const ranges: NamedVerifiableStatus[] = []; while(stack.length !== 0) { const top = stack.pop()!; top.forEach(child => { - if(child.uri === uri) { - if(child.range !== undefined) { - ranges.push(child.range); + if(child.uri?.toString() === uri.toString()) { + const status = this.statuses.get(child.id); + if(child.range !== undefined && status !== undefined) { + ranges.push({ nameRange: child.range, status: status }); } stack.push(child.children); } From 9b88302fdc341556465085d7dade5cd9e4fb9d34 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 6 Sep 2023 17:47:07 +0200 Subject: [PATCH 19/30] Use ResolutionCompleted --- src/language/api/compilationStatus.ts | 1 + src/ui/compilationStatusView.ts | 31 +++++++++++++++----------- src/ui/verificationSymbolStatusView.ts | 3 ++- 3 files changed, 21 insertions(+), 14 deletions(-) diff --git a/src/language/api/compilationStatus.ts b/src/language/api/compilationStatus.ts index 8c8c9f6d..3a90dcf5 100644 --- a/src/language/api/compilationStatus.ts +++ b/src/language/api/compilationStatus.ts @@ -6,6 +6,7 @@ export enum CompilationStatus { Resolving = 'ResolutionStarted', ResolutionFailed = 'ResolutionFailed', PreparingVerification = 'PreparingVerification', + ResolutionSucceeded = 'ResolutionSucceeded', CompilationSucceeded = 'CompilationSucceeded', VerificationStarted = 'VerificationStarted', VerificationFailed = 'VerificationFailed', diff --git a/src/ui/compilationStatusView.ts b/src/ui/compilationStatusView.ts index 9ce3ddef..b261b9db 100644 --- a/src/ui/compilationStatusView.ts +++ b/src/ui/compilationStatusView.ts @@ -54,19 +54,24 @@ export default class CompilationStatusView { private readonly documentStatusMessages = new Map(); private constructor(private readonly statusBarItem: StatusBarItem, + private readonly symbolStatusView: VerificationSymbolStatusView, private readonly languageClient: DafnyLanguageClient, private readonly context: ExtensionContext) {} - public static createAndRegister(context: ExtensionContext, languageClient: DafnyLanguageClient, languageServerVersion: string): CompilationStatusView { + public static createAndRegister(context: ExtensionContext, + languageClient: DafnyLanguageClient, + symbolStatusView: VerificationSymbolStatusView, + languageServerVersion: string): CompilationStatusView { const statusBarItem = window.createStatusBarItem(StatusBarAlignment.Left, StatusBarPriority); statusBarItem.command = DafnyCommands.OpenStatusBarMenu; - const view = new CompilationStatusView(statusBarItem, languageClient, context); + const view = new CompilationStatusView(statusBarItem, symbolStatusView, languageClient, context); const statusBarActionView = new StatusBarActionView(view, languageServerVersion, context); context.subscriptions.push( commands.registerCommand(DafnyCommands.OpenStatusBarMenu, () => statusBarActionView.openStatusBarMenu()), workspace.onDidCloseTextDocument(document => view.documentClosed(document)), workspace.onDidChangeTextDocument(() => view.updateActiveDocumentStatus()), window.onDidChangeActiveTextEditor(() => view.updateActiveDocumentStatus()), + symbolStatusView.onUpdates(uri => view.updateStatusBar(uri)), enableOnlyForDafnyDocuments(statusBarItem), statusBarItem ); @@ -84,7 +89,6 @@ export default class CompilationStatusView { public registerAfter38Messages(): void { this.context.subscriptions.push( this.languageClient.onCompilationStatus(params => this.compilationStatusChangedForBefore38(params)), - this.languageClient.onVerificationSymbolStatus(params => this.updateStatusBar(params)) ); } @@ -122,6 +126,7 @@ export default class CompilationStatusView { CompilationStatus.Resolving, CompilationStatus.ParsingFailed, CompilationStatus.ResolutionFailed, + CompilationStatus.ResolutionSucceeded, CompilationStatus.PreparingVerification, CompilationStatus.CompilationSucceeded ]); @@ -174,15 +179,15 @@ export default class CompilationStatusView { return this.documentStatusMessages.get(document)?.message ?? ''; } - public async updateStatusBar(params: IVerificationSymbolStatusParams): Promise { - const completed = params.namedVerifiables.filter(v => v.status >= PublishedVerificationStatus.Error).length; - const queued = params.namedVerifiables.filter(v => v.status === PublishedVerificationStatus.Queued); - const running = params.namedVerifiables.filter(v => v.status === PublishedVerificationStatus.Running); - const total = params.namedVerifiables.length; + public async updateStatusBar(uri: Uri): Promise { + const document = await workspace.openTextDocument(uri); + const statuses = this.symbolStatusView.getVerifiableRangesForUri(uri); + const completed = statuses.filter(v => v.status >= PublishedVerificationStatus.Error).length; + const queued = statuses.filter(v => v.status === PublishedVerificationStatus.Queued); + const running = statuses.filter(v => v.status === PublishedVerificationStatus.Running); + const total = statuses.length; let message: string; - params.uri = Uri.parse(params.uri).toString();// Makes the Uri canonical if(running.length > 0 || queued.length > 0) { - const document = await workspace.openTextDocument(Uri.parse(params.uri)); const verifying = running.map(item => document.getText(VerificationSymbolStatusView.convertRange(item.nameRange))).join(', '); message = `$(sync~spin) Verified ${completed}/${total}`; if(running.length > 0) { @@ -191,8 +196,8 @@ export default class CompilationStatusView { message += ', preparing verification'; } } else { - const skipped = params.namedVerifiables.filter(v => v.status === PublishedVerificationStatus.Stale).length; - const errors = params.namedVerifiables.filter(v => v.status === PublishedVerificationStatus.Error).length; + const skipped = statuses.filter(v => v.status === PublishedVerificationStatus.Stale).length; + const errors = statuses.filter(v => v.status === PublishedVerificationStatus.Error).length; const succeeded = completed - errors; if(errors === 0) { @@ -205,6 +210,6 @@ export default class CompilationStatusView { message = `${Messages.CompilationStatus.VerificationFailed} ${(errors > 1 ? `${errors} declarations` : 'the declaration')}`; } } - this.setDocumentStatusMessage(params.uri.toString(), message, params.version); + this.setDocumentStatusMessage(uri.toString(), message, document.version); } } diff --git a/src/ui/verificationSymbolStatusView.ts b/src/ui/verificationSymbolStatusView.ts index 0681c5d1..00f460bc 100644 --- a/src/ui/verificationSymbolStatusView.ts +++ b/src/ui/verificationSymbolStatusView.ts @@ -161,7 +161,6 @@ export default class VerificationSymbolStatusView { document: TextDocument, rootSymbols: DocumentSymbol[] | undefined) { - this.compilationStatusView.updateStatusBar(params); const controller = this.controller; this.clearItemsForUri(document.uri); @@ -179,6 +178,8 @@ export default class VerificationSymbolStatusView { } } + this._onUpdates.fire(document.uri); + const allTestItems: TestItem[] = []; function collectTestItems(collection: TestItemCollection) { collection.forEach(item => { From b0fcc05807d8337ca07a032b14dcc895372523c4 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 7 Sep 2023 16:22:56 +0200 Subject: [PATCH 20/30] Correctly handle ResolutionSucceeded notification --- src/ui/compilationStatusView.ts | 48 +++++++++++++++------- src/ui/dafnyIntegration.ts | 10 +---- src/ui/verificationGutterStatusView.ts | 2 +- src/ui/verificationSymbolStatusView.ts | 57 +++++++++++++------------- 4 files changed, 64 insertions(+), 53 deletions(-) diff --git a/src/ui/compilationStatusView.ts b/src/ui/compilationStatusView.ts index b261b9db..f55873cb 100644 --- a/src/ui/compilationStatusView.ts +++ b/src/ui/compilationStatusView.ts @@ -6,7 +6,7 @@ import { getVsDocumentPath } from '../tools/vscode'; import { enableOnlyForDafnyDocuments } from '../tools/visibility'; import { Messages } from './messages'; import StatusBarActionView from './statusBarActionView'; -import { IVerificationSymbolStatusParams, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; +import { PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; import VerificationSymbolStatusView from './verificationSymbolStatusView'; const StatusBarPriority = 10; @@ -54,27 +54,37 @@ export default class CompilationStatusView { private readonly documentStatusMessages = new Map(); private constructor(private readonly statusBarItem: StatusBarItem, - private readonly symbolStatusView: VerificationSymbolStatusView, private readonly languageClient: DafnyLanguageClient, private readonly context: ExtensionContext) {} public static createAndRegister(context: ExtensionContext, languageClient: DafnyLanguageClient, - symbolStatusView: VerificationSymbolStatusView, + symbolStatusView: VerificationSymbolStatusView | undefined, languageServerVersion: string): CompilationStatusView { const statusBarItem = window.createStatusBarItem(StatusBarAlignment.Left, StatusBarPriority); statusBarItem.command = DafnyCommands.OpenStatusBarMenu; - const view = new CompilationStatusView(statusBarItem, symbolStatusView, languageClient, context); + const view = new CompilationStatusView(statusBarItem, languageClient, context); const statusBarActionView = new StatusBarActionView(view, languageServerVersion, context); context.subscriptions.push( commands.registerCommand(DafnyCommands.OpenStatusBarMenu, () => statusBarActionView.openStatusBarMenu()), workspace.onDidCloseTextDocument(document => view.documentClosed(document)), workspace.onDidChangeTextDocument(() => view.updateActiveDocumentStatus()), window.onDidChangeActiveTextEditor(() => view.updateActiveDocumentStatus()), - symbolStatusView.onUpdates(uri => view.updateStatusBar(uri)), enableOnlyForDafnyDocuments(statusBarItem), statusBarItem ); + + if(symbolStatusView === undefined) { + view.registerBefore38Messages(); + } else { + context.subscriptions.push( + symbolStatusView.onUpdates(uri => view.showVerifiableRangesInStatusBar(uri, symbolStatusView)) + ); + + context.subscriptions.push( + languageClient.onCompilationStatus(params => view.compilationStatusChangedAfter38(params)) + ); + } return view; } @@ -86,12 +96,6 @@ export default class CompilationStatusView { ); } - public registerAfter38Messages(): void { - this.context.subscriptions.push( - this.languageClient.onCompilationStatus(params => this.compilationStatusChangedForBefore38(params)), - ); - } - // Backwards compatibility for versions of Dafny <= 3.8.0 private verificationStarted(params: IVerificationStartedParams): void { this.documentStatusMessages.set( @@ -130,10 +134,22 @@ export default class CompilationStatusView { CompilationStatus.PreparingVerification, CompilationStatus.CompilationSucceeded ]); - public compilationStatusChangedForBefore38(params: ICompilationStatusParams): void { + public compilationStatusChangedAfter38(params: ICompilationStatusParams): void { if(this.areParamsOutdated(params)) { return; } + if(params.status === CompilationStatus.ResolutionSucceeded) { + const verifiableRangeMessage = this.verifiableRangeMessages.get(params.uri); + if(verifiableRangeMessage === undefined) { + this.compilationStatusChangedAfter38({ ...params, status: CompilationStatus.Resolving }); + } else { + this.setDocumentStatusMessage( + getVsDocumentPath(params), + verifiableRangeMessage, + params.version); + } + return; + } if(CompilationStatusView.handledMessages.has(params.status)) { this.setDocumentStatusMessage( getVsDocumentPath(params), @@ -179,9 +195,10 @@ export default class CompilationStatusView { return this.documentStatusMessages.get(document)?.message ?? ''; } - public async updateStatusBar(uri: Uri): Promise { + private readonly verifiableRangeMessages = new Map(); + public async showVerifiableRangesInStatusBar(uri: Uri, symbolStatusView: VerificationSymbolStatusView): Promise { const document = await workspace.openTextDocument(uri); - const statuses = this.symbolStatusView.getVerifiableRangesForUri(uri); + const statuses = symbolStatusView.getVerifiableRangesForUri(uri); const completed = statuses.filter(v => v.status >= PublishedVerificationStatus.Error).length; const queued = statuses.filter(v => v.status === PublishedVerificationStatus.Queued); const running = statuses.filter(v => v.status === PublishedVerificationStatus.Running); @@ -207,9 +224,10 @@ export default class CompilationStatusView { message = `Verified ${succeeded} declarations, skipped ${skipped}`; } } else { - message = `${Messages.CompilationStatus.VerificationFailed} ${(errors > 1 ? `${errors} declarations` : 'the declaration')}`; + message = `${Messages.CompilationStatus.VerificationFailed} ${(errors > 1 ? `${errors} declarations` : 'a declaration')}`; } } + this.verifiableRangeMessages.set(uri.toString(), message); this.setDocumentStatusMessage(uri.toString(), message, document.version); } } diff --git a/src/ui/dafnyIntegration.ts b/src/ui/dafnyIntegration.ts index adfbfec1..f876ccd5 100644 --- a/src/ui/dafnyIntegration.ts +++ b/src/ui/dafnyIntegration.ts @@ -18,18 +18,12 @@ export default function createAndRegisterDafnyIntegration( ): void { CounterexamplesView.createAndRegister(installer.context, languageClient); GhostDiagnosticsView.createAndRegister(installer.context, languageClient); - const compilationStatusView = CompilationStatusView.createAndRegister(installer.context, languageClient, languageServerVersion); let symbolStatusView: VerificationSymbolStatusView | undefined = undefined; const serverSupportsSymbolStatusView = configuredVersionToNumeric('3.8.0') <= configuredVersionToNumeric(languageServerVersion); if(serverSupportsSymbolStatusView && Configuration.get(ConfigurationConstants.LanguageServer.DisplayVerificationAsTests)) { - symbolStatusView = VerificationSymbolStatusView.createAndRegister(installer.context, languageClient, compilationStatusView); - } else { - if(serverSupportsSymbolStatusView) { - compilationStatusView.registerAfter38Messages(); - } else { - compilationStatusView.registerBefore38Messages(); - } + symbolStatusView = VerificationSymbolStatusView.createAndRegister(installer.context, languageClient); } + CompilationStatusView.createAndRegister(installer.context, languageClient, symbolStatusView, languageServerVersion); VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); CompileCommands.createAndRegister(installer); RelatedErrorView.createAndRegister(installer.context, languageClient); diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 5f657707..0e4bf10b 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -265,7 +265,7 @@ export default class VerificationGutterStatusView { const symbolParams = params.perLineStatus.indexOf(LineVerificationStatus.ResolutionError) > 0 ? [] : (this.symbolStatusView?.getVerifiableRangesForUri(uri) ?? []); - const originalLinesToSkip = symbolParams.map(range => range.start.line).sort((a, b) => a - b); + const originalLinesToSkip = symbolParams.map(range => range.nameRange.start.line).sort((a, b) => a - b); return VerificationGutterStatusView.perLineStatusToRanges(perLineStatus, originalLinesToSkip); } diff --git a/src/ui/verificationSymbolStatusView.ts b/src/ui/verificationSymbolStatusView.ts index 00f460bc..c4e215b1 100644 --- a/src/ui/verificationSymbolStatusView.ts +++ b/src/ui/verificationSymbolStatusView.ts @@ -1,9 +1,8 @@ /* eslint-disable max-depth */ -import { commands, ExtensionContext, workspace, tests, Range, Position, Uri, TestRunRequest, TestController, TestRun, DocumentSymbol, TestItem, TestItemCollection, TextDocument, TestRunProfileKind } from 'vscode'; +import { commands, ExtensionContext, workspace, Event, tests, Range, Position, Uri, TestRunRequest, TestController, TestRun, DocumentSymbol, TestItem, TestItemCollection, TextDocument, TestRunProfileKind, EventEmitter } from 'vscode'; import { Range as lspRange, Position as lspPosition } from 'vscode-languageclient'; -import { IVerificationSymbolStatusParams, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; +import { IVerificationSymbolStatusParams, NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; -import CompilationStatusView from './compilationStatusView'; class ResolveablePromise { private _resolve: (value: T) => void = () => {}; @@ -29,13 +28,6 @@ interface ItemRunState { startedRunningTime?: number; } -export function createAndRegister( - context: ExtensionContext, - languageClient: DafnyLanguageClient, - compilationStatusView: CompilationStatusView): VerificationSymbolStatusView { - return new VerificationSymbolStatusView(context, languageClient, compilationStatusView); -} - /** * This class shows verification tasks through the VSCode testing UI. */ @@ -43,30 +35,32 @@ export default class VerificationSymbolStatusView { public static createAndRegister( context: ExtensionContext, - languageClient: DafnyLanguageClient, - compilationStatusView: CompilationStatusView): VerificationSymbolStatusView { - return new VerificationSymbolStatusView(context, languageClient, compilationStatusView); + languageClient: DafnyLanguageClient): VerificationSymbolStatusView { + return new VerificationSymbolStatusView(context, languageClient); } + private itemStates: Map = new Map(); + private itemRuns: Map = new Map(); + private readonly runItemsLeft: Map = new Map(); + private readonly controller: TestController; + private automaticRunEnd: boolean = false; + private noRunCreationInProgress: Promise = Promise.resolve(); + private readonly _onUpdates: EventEmitter = new EventEmitter(); + public onUpdates: Event = this._onUpdates.event; + public constructor( private readonly context: ExtensionContext, - private readonly languageClient: DafnyLanguageClient, - private readonly compilationStatusView: CompilationStatusView) { + private readonly languageClient: DafnyLanguageClient) { this.controller = this.createController(); context.subscriptions.push(this.controller); context.subscriptions.push( - languageClient.onVerificationSymbolStatus(params => this.update(params)), - languageClient.onCompilationStatus(params => compilationStatusView.compilationStatusChangedForBefore38(params)) + languageClient.onVerificationSymbolStatus(params => { + this.update(params); + }) ); } - private itemStates: Map = new Map(); - private itemRuns: Map = new Map(); - private readonly runItemsLeft: Map = new Map(); - private readonly controller: TestController; - private automaticRunEnd: boolean = false; - private noRunCreationInProgress: Promise = Promise.resolve(); private createController(): TestController { const controller = tests.createTestController('verificationStatus', 'Verification Status'); @@ -138,6 +132,7 @@ export default class VerificationSymbolStatusView { await this.noRunCreationInProgress; const uri = Uri.parse(params.uri); + await this.noRunCreationInProgress; params.uri = uri.toString(); const document = await workspace.openTextDocument(uri); const rootSymbols = await commands.executeCommand('vscode.executeDocumentSymbolProvider', uri) as DocumentSymbol[] | undefined; @@ -177,7 +172,6 @@ export default class VerificationSymbolStatusView { controller.items.add(leafItem); } } - this._onUpdates.fire(document.uri); const allTestItems: TestItem[] = []; @@ -205,6 +199,8 @@ export default class VerificationSymbolStatusView { const newItemRuns = new Map(); params.namedVerifiables.forEach((element, index) => { const testItem = leafItems[index]; + this.leafStatuses.set(testItem.id, element.status); + const itemRunState = this.itemRuns.get(testItem.id)!; if(this.itemStates.get(testItem.id) === element.status) { const isRunning = itemRunState !== undefined; @@ -333,15 +329,18 @@ export default class VerificationSymbolStatusView { return new Position(position.line, position.character); } - public getVerifiableRangesForUri(uri: Uri): Range[] { + private readonly leafStatuses: Map = new Map(); + + public getVerifiableRangesForUri(uri: Uri): NamedVerifiableStatus[] { const stack: TestItemCollection[] = [ this.controller.items ]; - const ranges: Range[] = []; + const ranges: NamedVerifiableStatus[] = []; while(stack.length !== 0) { const top = stack.pop()!; top.forEach(child => { - if(child.uri === uri) { - if(child.range !== undefined) { - ranges.push(child.range); + if(child.uri?.toString() === uri.toString()) { + const status = this.leafStatuses.get(child.id); + if(child.range !== undefined && status !== undefined) { + ranges.push({ nameRange: child.range, status: status }); } stack.push(child.children); } From e928e1817c93a6ee2d9fe4702b94c34cc8666139 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 7 Sep 2023 16:27:36 +0200 Subject: [PATCH 21/30] Refactoring --- src/ui/compilationStatusView.ts | 22 ++++++++++++---------- src/ui/dafnyIntegration.ts | 2 +- 2 files changed, 13 insertions(+), 11 deletions(-) diff --git a/src/ui/compilationStatusView.ts b/src/ui/compilationStatusView.ts index f55873cb..8f65e896 100644 --- a/src/ui/compilationStatusView.ts +++ b/src/ui/compilationStatusView.ts @@ -6,7 +6,7 @@ import { getVsDocumentPath } from '../tools/vscode'; import { enableOnlyForDafnyDocuments } from '../tools/visibility'; import { Messages } from './messages'; import StatusBarActionView from './statusBarActionView'; -import { PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; +import { IVerificationSymbolStatusParams, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; import VerificationSymbolStatusView from './verificationSymbolStatusView'; const StatusBarPriority = 10; @@ -59,7 +59,7 @@ export default class CompilationStatusView { public static createAndRegister(context: ExtensionContext, languageClient: DafnyLanguageClient, - symbolStatusView: VerificationSymbolStatusView | undefined, + useOnVerificationSymbolStatus: boolean, languageServerVersion: string): CompilationStatusView { const statusBarItem = window.createStatusBarItem(StatusBarAlignment.Left, StatusBarPriority); statusBarItem.command = DafnyCommands.OpenStatusBarMenu; @@ -74,16 +74,16 @@ export default class CompilationStatusView { statusBarItem ); - if(symbolStatusView === undefined) { - view.registerBefore38Messages(); - } else { - context.subscriptions.push( - symbolStatusView.onUpdates(uri => view.showVerifiableRangesInStatusBar(uri, symbolStatusView)) - ); + if(useOnVerificationSymbolStatus) { + languageClient.onVerificationSymbolStatus(params => { + view.showVerifiableRangesInStatusBar(params); + }); context.subscriptions.push( languageClient.onCompilationStatus(params => view.compilationStatusChangedAfter38(params)) ); + } else { + view.registerBefore38Messages(); } return view; } @@ -196,9 +196,11 @@ export default class CompilationStatusView { } private readonly verifiableRangeMessages = new Map(); - public async showVerifiableRangesInStatusBar(uri: Uri, symbolStatusView: VerificationSymbolStatusView): Promise { + public async showVerifiableRangesInStatusBar(params: IVerificationSymbolStatusParams): Promise { + const uri = Uri.parse(params.uri); + const document = await workspace.openTextDocument(uri); - const statuses = symbolStatusView.getVerifiableRangesForUri(uri); + const statuses = params.namedVerifiables; const completed = statuses.filter(v => v.status >= PublishedVerificationStatus.Error).length; const queued = statuses.filter(v => v.status === PublishedVerificationStatus.Queued); const running = statuses.filter(v => v.status === PublishedVerificationStatus.Running); diff --git a/src/ui/dafnyIntegration.ts b/src/ui/dafnyIntegration.ts index f876ccd5..f38b275f 100644 --- a/src/ui/dafnyIntegration.ts +++ b/src/ui/dafnyIntegration.ts @@ -23,7 +23,7 @@ export default function createAndRegisterDafnyIntegration( if(serverSupportsSymbolStatusView && Configuration.get(ConfigurationConstants.LanguageServer.DisplayVerificationAsTests)) { symbolStatusView = VerificationSymbolStatusView.createAndRegister(installer.context, languageClient); } - CompilationStatusView.createAndRegister(installer.context, languageClient, symbolStatusView, languageServerVersion); + CompilationStatusView.createAndRegister(installer.context, languageClient, serverSupportsSymbolStatusView, languageServerVersion); VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); CompileCommands.createAndRegister(installer); RelatedErrorView.createAndRegister(installer.context, languageClient); From d4307d49a285eef58d15aeae118addf704a6d345 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 7 Sep 2023 16:30:33 +0200 Subject: [PATCH 22/30] Reduce changes --- src/ui/compilationStatusView.ts | 1 + src/ui/verificationGutterStatusView.ts | 2 +- src/ui/verificationSymbolStatusView.ts | 46 +++++++++++--------------- 3 files changed, 22 insertions(+), 27 deletions(-) diff --git a/src/ui/compilationStatusView.ts b/src/ui/compilationStatusView.ts index 8f65e896..aa217944 100644 --- a/src/ui/compilationStatusView.ts +++ b/src/ui/compilationStatusView.ts @@ -141,6 +141,7 @@ export default class CompilationStatusView { if(params.status === CompilationStatus.ResolutionSucceeded) { const verifiableRangeMessage = this.verifiableRangeMessages.get(params.uri); if(verifiableRangeMessage === undefined) { + // If we have not yet received verification symbols, then pretend we're still resolving. this.compilationStatusChangedAfter38({ ...params, status: CompilationStatus.Resolving }); } else { this.setDocumentStatusMessage( diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 0e4bf10b..5f657707 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -265,7 +265,7 @@ export default class VerificationGutterStatusView { const symbolParams = params.perLineStatus.indexOf(LineVerificationStatus.ResolutionError) > 0 ? [] : (this.symbolStatusView?.getVerifiableRangesForUri(uri) ?? []); - const originalLinesToSkip = symbolParams.map(range => range.nameRange.start.line).sort((a, b) => a - b); + const originalLinesToSkip = symbolParams.map(range => range.start.line).sort((a, b) => a - b); return VerificationGutterStatusView.perLineStatusToRanges(perLineStatus, originalLinesToSkip); } diff --git a/src/ui/verificationSymbolStatusView.ts b/src/ui/verificationSymbolStatusView.ts index c4e215b1..0ca29b37 100644 --- a/src/ui/verificationSymbolStatusView.ts +++ b/src/ui/verificationSymbolStatusView.ts @@ -1,7 +1,7 @@ /* eslint-disable max-depth */ -import { commands, ExtensionContext, workspace, Event, tests, Range, Position, Uri, TestRunRequest, TestController, TestRun, DocumentSymbol, TestItem, TestItemCollection, TextDocument, TestRunProfileKind, EventEmitter } from 'vscode'; +import { commands, ExtensionContext, workspace, tests, Range, Position, Uri, TestRunRequest, TestController, TestRun, DocumentSymbol, TestItem, TestItemCollection, TextDocument, TestRunProfileKind } from 'vscode'; import { Range as lspRange, Position as lspPosition } from 'vscode-languageclient'; -import { IVerificationSymbolStatusParams, NamedVerifiableStatus, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; +import { IVerificationSymbolStatusParams, PublishedVerificationStatus } from '../language/api/verificationSymbolStatusParams'; import { DafnyLanguageClient } from '../language/dafnyLanguageClient'; class ResolveablePromise { @@ -28,6 +28,12 @@ interface ItemRunState { startedRunningTime?: number; } +export function createAndRegister( + context: ExtensionContext, + languageClient: DafnyLanguageClient): VerificationSymbolStatusView { + return new VerificationSymbolStatusView(context, languageClient); +} + /** * This class shows verification tasks through the VSCode testing UI. */ @@ -39,15 +45,6 @@ export default class VerificationSymbolStatusView { return new VerificationSymbolStatusView(context, languageClient); } - private itemStates: Map = new Map(); - private itemRuns: Map = new Map(); - private readonly runItemsLeft: Map = new Map(); - private readonly controller: TestController; - private automaticRunEnd: boolean = false; - private noRunCreationInProgress: Promise = Promise.resolve(); - private readonly _onUpdates: EventEmitter = new EventEmitter(); - public onUpdates: Event = this._onUpdates.event; - public constructor( private readonly context: ExtensionContext, private readonly languageClient: DafnyLanguageClient) { @@ -55,12 +52,16 @@ export default class VerificationSymbolStatusView { context.subscriptions.push(this.controller); context.subscriptions.push( - languageClient.onVerificationSymbolStatus(params => { - this.update(params); - }) + languageClient.onVerificationSymbolStatus(params => this.update(params)) ); } + private itemStates: Map = new Map(); + private itemRuns: Map = new Map(); + private readonly runItemsLeft: Map = new Map(); + private readonly controller: TestController; + private automaticRunEnd: boolean = false; + private noRunCreationInProgress: Promise = Promise.resolve(); private createController(): TestController { const controller = tests.createTestController('verificationStatus', 'Verification Status'); @@ -132,7 +133,6 @@ export default class VerificationSymbolStatusView { await this.noRunCreationInProgress; const uri = Uri.parse(params.uri); - await this.noRunCreationInProgress; params.uri = uri.toString(); const document = await workspace.openTextDocument(uri); const rootSymbols = await commands.executeCommand('vscode.executeDocumentSymbolProvider', uri) as DocumentSymbol[] | undefined; @@ -172,7 +172,6 @@ export default class VerificationSymbolStatusView { controller.items.add(leafItem); } } - this._onUpdates.fire(document.uri); const allTestItems: TestItem[] = []; function collectTestItems(collection: TestItemCollection) { @@ -199,8 +198,6 @@ export default class VerificationSymbolStatusView { const newItemRuns = new Map(); params.namedVerifiables.forEach((element, index) => { const testItem = leafItems[index]; - this.leafStatuses.set(testItem.id, element.status); - const itemRunState = this.itemRuns.get(testItem.id)!; if(this.itemStates.get(testItem.id) === element.status) { const isRunning = itemRunState !== undefined; @@ -329,18 +326,15 @@ export default class VerificationSymbolStatusView { return new Position(position.line, position.character); } - private readonly leafStatuses: Map = new Map(); - - public getVerifiableRangesForUri(uri: Uri): NamedVerifiableStatus[] { + public getVerifiableRangesForUri(uri: Uri): Range[] { const stack: TestItemCollection[] = [ this.controller.items ]; - const ranges: NamedVerifiableStatus[] = []; + const ranges: Range[] = []; while(stack.length !== 0) { const top = stack.pop()!; top.forEach(child => { - if(child.uri?.toString() === uri.toString()) { - const status = this.leafStatuses.get(child.id); - if(child.range !== undefined && status !== undefined) { - ranges.push({ nameRange: child.range, status: status }); + if(child.uri === uri) { + if(child.range !== undefined) { + ranges.push(child.range); } stack.push(child.children); } From 29f43a69ff187682098bf438e11fa74b76b01ac5 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 7 Sep 2023 17:02:25 +0200 Subject: [PATCH 23/30] Remove unused method --- src/ui/verificationSymbolStatusView.ts | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/ui/verificationSymbolStatusView.ts b/src/ui/verificationSymbolStatusView.ts index 0ca29b37..e4765455 100644 --- a/src/ui/verificationSymbolStatusView.ts +++ b/src/ui/verificationSymbolStatusView.ts @@ -28,12 +28,6 @@ interface ItemRunState { startedRunningTime?: number; } -export function createAndRegister( - context: ExtensionContext, - languageClient: DafnyLanguageClient): VerificationSymbolStatusView { - return new VerificationSymbolStatusView(context, languageClient); -} - /** * This class shows verification tasks through the VSCode testing UI. */ From 29e8b869e4247613229b6112c17a669e50d0b00e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 7 Sep 2023 17:18:41 +0200 Subject: [PATCH 24/30] Enable duplicate event registration --- src/language/dafnyLanguageClient.ts | 11 +++++++---- src/ui/compilationStatusView.ts | 7 +++---- src/ui/dafnyIntegration.ts | 4 ++-- src/ui/verificationSymbolStatusView.ts | 2 +- 4 files changed, 13 insertions(+), 11 deletions(-) diff --git a/src/language/dafnyLanguageClient.ts b/src/language/dafnyLanguageClient.ts index ae6caa01..895cd198 100644 --- a/src/language/dafnyLanguageClient.ts +++ b/src/language/dafnyLanguageClient.ts @@ -1,4 +1,4 @@ -import { Disposable, Uri, Diagnostic } from 'vscode'; +import { Disposable, Uri, Diagnostic, EventEmitter, Event } from 'vscode'; import { HandleDiagnosticsSignature, LanguageClient, LanguageClientOptions, ServerOptions, TextDocumentPositionParams } from 'vscode-languageclient/node'; import Configuration from '../configuration'; @@ -127,6 +127,9 @@ export class DafnyLanguageClient extends LanguageClient { private readonly diagnosticsListeners: DiagnosticListener[], forceDebug?: boolean) { super(id, name, serverOptions, clientOptions, forceDebug); this.diagnosticsListeners = diagnosticsListeners; + this.onReady().then(() => { + this.onNotification('dafny/textDocument/symbolStatus', params => this._onVerificationSymbolStatus.fire(params)); + }); } public getCounterexamples(param: ICounterexampleParams): Promise { @@ -173,9 +176,9 @@ export class DafnyLanguageClient extends LanguageClient { return this.onNotification('dafny/verification/status/gutter', callback); } - public onVerificationSymbolStatus(callback: (params: IVerificationSymbolStatusParams) => void): Disposable { - return this.onNotification('dafny/textDocument/symbolStatus', callback); - } + private readonly _onVerificationSymbolStatus: EventEmitter = new EventEmitter(); + + public OnVerificationSymbolStatus: Event = this._onVerificationSymbolStatus.event; public onCompilationStatus(callback: (params: ICompilationStatusParams) => void): Disposable { return this.onNotification('dafny/compilation/status', callback); diff --git a/src/ui/compilationStatusView.ts b/src/ui/compilationStatusView.ts index aa217944..3c9a8be4 100644 --- a/src/ui/compilationStatusView.ts +++ b/src/ui/compilationStatusView.ts @@ -75,11 +75,10 @@ export default class CompilationStatusView { ); if(useOnVerificationSymbolStatus) { - languageClient.onVerificationSymbolStatus(params => { - view.showVerifiableRangesInStatusBar(params); - }); - context.subscriptions.push( + languageClient.OnVerificationSymbolStatus(params => { + view.showVerifiableRangesInStatusBar(params); + }), languageClient.onCompilationStatus(params => view.compilationStatusChangedAfter38(params)) ); } else { diff --git a/src/ui/dafnyIntegration.ts b/src/ui/dafnyIntegration.ts index f38b275f..f24ea02f 100644 --- a/src/ui/dafnyIntegration.ts +++ b/src/ui/dafnyIntegration.ts @@ -18,12 +18,12 @@ export default function createAndRegisterDafnyIntegration( ): void { CounterexamplesView.createAndRegister(installer.context, languageClient); GhostDiagnosticsView.createAndRegister(installer.context, languageClient); - let symbolStatusView: VerificationSymbolStatusView | undefined = undefined; const serverSupportsSymbolStatusView = configuredVersionToNumeric('3.8.0') <= configuredVersionToNumeric(languageServerVersion); + CompilationStatusView.createAndRegister(installer.context, languageClient, serverSupportsSymbolStatusView, languageServerVersion); + let symbolStatusView: VerificationSymbolStatusView | undefined = undefined; if(serverSupportsSymbolStatusView && Configuration.get(ConfigurationConstants.LanguageServer.DisplayVerificationAsTests)) { symbolStatusView = VerificationSymbolStatusView.createAndRegister(installer.context, languageClient); } - CompilationStatusView.createAndRegister(installer.context, languageClient, serverSupportsSymbolStatusView, languageServerVersion); VerificationGutterStatusView.createAndRegister(installer.context, languageClient, symbolStatusView); CompileCommands.createAndRegister(installer); RelatedErrorView.createAndRegister(installer.context, languageClient); diff --git a/src/ui/verificationSymbolStatusView.ts b/src/ui/verificationSymbolStatusView.ts index e4765455..d59ceabf 100644 --- a/src/ui/verificationSymbolStatusView.ts +++ b/src/ui/verificationSymbolStatusView.ts @@ -46,7 +46,7 @@ export default class VerificationSymbolStatusView { context.subscriptions.push(this.controller); context.subscriptions.push( - languageClient.onVerificationSymbolStatus(params => this.update(params)) + languageClient.OnVerificationSymbolStatus(params => this.update(params)) ); } From d8933944808326c46b5218cdf3df3a672a95562e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 8 Sep 2023 14:54:38 +0200 Subject: [PATCH 25/30] Outdated errors also create error context --- src/ui/verificationGutterStatusView.ts | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 06b95a2c..7f54460c 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -185,7 +185,8 @@ export default class VerificationGutterStatusView { } const perLineStatus: LineVerificationStatus[] = []; for(const diagnostic of diagnostics) { - if(diagnostic.severity !== DiagnosticSeverity.Error) { + const outdatedError = diagnostic.message.startsWith('Outdated: '); + if(diagnostic.severity !== DiagnosticSeverity.Error && !outdatedError) { continue; } for(let line = diagnostic.range.start.line; line <= diagnostic.range.end.line; line++) { From a2ac4b522a3d58d4c7f28b51e61727a806d23ce3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 8 Sep 2023 15:28:00 +0200 Subject: [PATCH 26/30] Update tests and add support for related diagnostics --- src/test/suite/extension.test.ts | 74 +++++++++++++++++--------- src/ui/verificationGutterStatusView.ts | 32 +++++++---- 2 files changed, 72 insertions(+), 34 deletions(-) diff --git a/src/test/suite/extension.test.ts b/src/test/suite/extension.test.ts index fcfa1504..04c37304 100644 --- a/src/test/suite/extension.test.ts +++ b/src/test/suite/extension.test.ts @@ -152,20 +152,28 @@ suite('Verification Gutter', () => { parse(;)Error } - method Bat() { - assert false; // Outdated error + method Bat() + ensures false + { + if (true) { + return; + } else { + return; + } } method Fom() { assert true; } */ + const uri = vscode.Uri.parse('file:///woops.dfy'); const parseError = new vscode.Diagnostic(new vscode.Range(1, 2, 1, 15), 'Some parse error', vscode.DiagnosticSeverity.Error); parseError.source = 'Parser'; - const computedIcons = VerificationGutterStatusView.computeGutterIcons(10, undefined, undefined, [ - parseError, - new vscode.Diagnostic(new vscode.Range(5, 2, 5, 14), 'Outdated: could not prove assertion', vscode.DiagnosticSeverity.Error) - ]); + const outdatedReturnError = new vscode.Diagnostic(new vscode.Range(8, 8, 8, 14), 'Outdated: a postcondition could not be proved on this return path', vscode.DiagnosticSeverity.Warning); + outdatedReturnError.relatedInformation = [ { + location: { uri, range: new vscode.Range(5, 14, 5, 19) }, + message: 'This postcondition might not hold: false' + } ]; const expected = [ LineVerificationStatus.VerifiedObsolete, LineVerificationStatus.ResolutionError, @@ -175,9 +183,23 @@ suite('Verification Gutter', () => { LineVerificationStatus.AssertionFailedObsolete, LineVerificationStatus.VerifiedObsolete, LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.AssertionFailedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, + LineVerificationStatus.VerifiedObsolete, LineVerificationStatus.VerifiedObsolete, LineVerificationStatus.VerifiedObsolete ]; + const computedIcons = VerificationGutterStatusView.computeGutterIcons( + uri, + expected.length, undefined, undefined, [ + parseError, + outdatedReturnError + ] + ); assert.deepStrictEqual(expected, computedIcons); }); @@ -208,25 +230,27 @@ suite('Verification Gutter', () => { assert false; // Error } */ - const computedIcons = VerificationGutterStatusView.computeGutterIcons(24, new Map([ - [ '0,7', new vscode.Range(0, 0, 2, 1) ], - [ '4,7', new vscode.Range(4, 0, 6, 1) ], - [ '8,7', new vscode.Range(8, 0, 10, 1) ], - [ '12,7', new vscode.Range(12, 0, 14, 1) ], - [ '16,7', new vscode.Range(16, 0, 18, 1) ], - [ '20,7', new vscode.Range(20, 0, 23, 1) ] - ]), [ - { nameRange: new vscode.Range(0, 7, 0, 10), status: PublishedVerificationStatus.Stale }, - { nameRange: new vscode.Range(4, 7, 4, 10), status: PublishedVerificationStatus.Stale }, - { nameRange: new vscode.Range(8, 7, 8, 10), status: PublishedVerificationStatus.Queued }, - { nameRange: new vscode.Range(12, 7, 12, 10), status: PublishedVerificationStatus.Running }, - { nameRange: new vscode.Range(16, 7, 16, 10), status: PublishedVerificationStatus.Correct }, - { nameRange: new vscode.Range(20, 7, 20, 10), status: PublishedVerificationStatus.Error } - ], [ - new vscode.Diagnostic(new vscode.Range(5, 2, 5, 14), 'Outdated, could not prove assertion', vscode.DiagnosticSeverity.Error), - new vscode.Diagnostic(new vscode.Range(17, 2, 17, 14), 'some warning', vscode.DiagnosticSeverity.Warning), - new vscode.Diagnostic(new vscode.Range(22, 2, 22, 14), 'could not prove assertion', vscode.DiagnosticSeverity.Error) - ]); + const computedIcons = VerificationGutterStatusView.computeGutterIcons( + vscode.Uri.parse('file:///woops.dfy'), + 24, new Map([ + [ '0,7', new vscode.Range(0, 0, 2, 1) ], + [ '4,7', new vscode.Range(4, 0, 6, 1) ], + [ '8,7', new vscode.Range(8, 0, 10, 1) ], + [ '12,7', new vscode.Range(12, 0, 14, 1) ], + [ '16,7', new vscode.Range(16, 0, 18, 1) ], + [ '20,7', new vscode.Range(20, 0, 23, 1) ] + ]), [ + { nameRange: new vscode.Range(0, 7, 0, 10), status: PublishedVerificationStatus.Stale }, + { nameRange: new vscode.Range(4, 7, 4, 10), status: PublishedVerificationStatus.Stale }, + { nameRange: new vscode.Range(8, 7, 8, 10), status: PublishedVerificationStatus.Queued }, + { nameRange: new vscode.Range(12, 7, 12, 10), status: PublishedVerificationStatus.Running }, + { nameRange: new vscode.Range(16, 7, 16, 10), status: PublishedVerificationStatus.Correct }, + { nameRange: new vscode.Range(20, 7, 20, 10), status: PublishedVerificationStatus.Error } + ], [ + new vscode.Diagnostic(new vscode.Range(5, 2, 5, 14), 'Outdated: could not prove assertion', vscode.DiagnosticSeverity.Warning), + new vscode.Diagnostic(new vscode.Range(17, 2, 17, 14), 'some warning', vscode.DiagnosticSeverity.Warning), + new vscode.Diagnostic(new vscode.Range(22, 2, 22, 14), 'could not prove assertion', vscode.DiagnosticSeverity.Error) + ]); const expected = [ LineVerificationStatus.Nothing, LineVerificationStatus.VerifiedObsolete, diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 7f54460c..79bfac77 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -149,7 +149,7 @@ export default class VerificationGutterStatusView { const document = await workspace.openTextDocument(uri); this.lineCountsPerDocument.set(document.uri, document.lineCount); - const perLineStatus = VerificationGutterStatusView.computeGutterIcons(document.lineCount, nameToSymbolRange, verifiableRanges, diagnostics); + const perLineStatus = VerificationGutterStatusView.computeGutterIcons(uri, document.lineCount, nameToSymbolRange, verifiableRanges, diagnostics); this.updateUsingLineStatus({ uri: uri.toString(), perLineStatus: perLineStatus }); } @@ -165,7 +165,9 @@ export default class VerificationGutterStatusView { return result; } + // eslint-disable-next-line max-params public static computeGutterIcons( + uri: Uri, lineCount: number, nameToSymbolRanges: Map | undefined, statuses: NamedVerifiableStatus[] | undefined, @@ -189,16 +191,14 @@ export default class VerificationGutterStatusView { if(diagnostic.severity !== DiagnosticSeverity.Error && !outdatedError) { continue; } - for(let line = diagnostic.range.start.line; line <= diagnostic.range.end.line; line++) { - lineToErrorSource.set(line, diagnostic.source ?? ''); - const contextRange = lineToSymbolRange.get(line); - if(contextRange === undefined) { - continue; - } - for(let contextLine = contextRange.start.line; contextLine <= contextRange.end.line; contextLine++) { - linesInErrorContext.add(contextLine); + + const source = diagnostic.source ?? ''; + for(const related of diagnostic.relatedInformation ?? []) { + if(related.location.uri === uri) { + processErrorRange(related.location.range, source); } } + processErrorRange(diagnostic.range, source); } if(nameToSymbolRanges === undefined || statuses === undefined) { @@ -219,6 +219,20 @@ export default class VerificationGutterStatusView { } } } + + function processErrorRange(range: Range, source: string | undefined) { + for(let line = range.start.line; line <= range.end.line; line++) { + lineToErrorSource.set(line, source ?? ''); + const contextRange = lineToSymbolRange.get(line); + if(contextRange === undefined) { + continue; + } + for(let contextLine = contextRange.start.line; contextLine <= contextRange.end.line; contextLine++) { + linesInErrorContext.add(contextLine); + } + } + } + for(let line = 0; line < lineCount; line++) { if(linesToSkip.has(line)) { perLineStatus.push(LineVerificationStatus.Nothing); From 8040603fa1784cf58c31f1a988be48175bd00a6b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 11 Sep 2023 13:43:35 +0200 Subject: [PATCH 27/30] Slight UI tweak --- src/ui/compilationStatusView.ts | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/ui/compilationStatusView.ts b/src/ui/compilationStatusView.ts index 3c9a8be4..4c4b3dd8 100644 --- a/src/ui/compilationStatusView.ts +++ b/src/ui/compilationStatusView.ts @@ -216,17 +216,21 @@ export default class CompilationStatusView { } } else { const skipped = statuses.filter(v => v.status === PublishedVerificationStatus.Stale).length; - const errors = statuses.filter(v => v.status === PublishedVerificationStatus.Error).length; - const succeeded = completed - errors; + const errors = statuses.filter(v => v.status === PublishedVerificationStatus.Error); + const errorCount = errors.length; + const succeeded = completed - errorCount; - if(errors === 0) { + if(errorCount === 0) { if(skipped === 0) { message = Messages.CompilationStatus.VerificationSucceeded; } else { message = `Verified ${succeeded} declarations, skipped ${skipped}`; } } else { - message = `${Messages.CompilationStatus.VerificationFailed} ${(errors > 1 ? `${errors} declarations` : 'a declaration')}`; + const object = errorCount > 1 + ? `${errorCount} declarations` + : (document.getText(VerificationSymbolStatusView.convertRange(errors[0].nameRange)) ?? 'a declaration'); + message = `${Messages.CompilationStatus.VerificationFailed} ${object}`; } } this.verifiableRangeMessages.set(uri.toString(), message); From 8fdec69e6f6fe08dcc8e6d1c4b7d43a76eb4e858 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 11 Sep 2023 18:52:20 +0200 Subject: [PATCH 28/30] Add support for foundAllErrors --- src/language/api/verificationSymbolStatusParams.ts | 3 ++- src/ui/compilationStatusView.ts | 3 ++- src/ui/verificationSymbolStatusView.ts | 1 + 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/language/api/verificationSymbolStatusParams.ts b/src/language/api/verificationSymbolStatusParams.ts index fca58cc9..d0fdc2d3 100644 --- a/src/language/api/verificationSymbolStatusParams.ts +++ b/src/language/api/verificationSymbolStatusParams.ts @@ -16,5 +16,6 @@ export enum PublishedVerificationStatus { Queued = 1, // Scheduled to be run but waiting for resources Running = 2, // Currently running Error = 4, // Finished and had errors - Correct = 5 // Finished and was correct + Correct = 5, // Finished and was correct + FoundAllErrors = 6 // Finished, had errors and found them all } \ No newline at end of file diff --git a/src/ui/compilationStatusView.ts b/src/ui/compilationStatusView.ts index 4c4b3dd8..050720cb 100644 --- a/src/ui/compilationStatusView.ts +++ b/src/ui/compilationStatusView.ts @@ -216,7 +216,8 @@ export default class CompilationStatusView { } } else { const skipped = statuses.filter(v => v.status === PublishedVerificationStatus.Stale).length; - const errors = statuses.filter(v => v.status === PublishedVerificationStatus.Error); + const errors = statuses.filter(v => v.status === PublishedVerificationStatus.Error + || v.status === PublishedVerificationStatus.FoundAllErrors); const errorCount = errors.length; const succeeded = completed - errorCount; diff --git a/src/ui/verificationSymbolStatusView.ts b/src/ui/verificationSymbolStatusView.ts index fd05a49b..1e5d2398 100644 --- a/src/ui/verificationSymbolStatusView.ts +++ b/src/ui/verificationSymbolStatusView.ts @@ -228,6 +228,7 @@ export default class VerificationSymbolStatusView { itemFinished(); break; } + case PublishedVerificationStatus.FoundAllErrors: case PublishedVerificationStatus.Error: run.failed(testItem, [], getDuration()); itemFinished(); From 838cb74d8441fe35c423a1000ae3d090ae393008 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 11 Sep 2023 19:11:58 +0200 Subject: [PATCH 29/30] Added support for verified in context --- src/test/suite/extension.test.ts | 27 ++++++++++++++++++++++++++ src/ui/verificationGutterStatusView.ts | 8 +++++++- 2 files changed, 34 insertions(+), 1 deletion(-) diff --git a/src/test/suite/extension.test.ts b/src/test/suite/extension.test.ts index 583b456a..23a880fd 100644 --- a/src/test/suite/extension.test.ts +++ b/src/test/suite/extension.test.ts @@ -203,6 +203,33 @@ suite('Verification Gutter', () => { assert.deepStrictEqual(expected, computedIcons); }); + test('foundAllError', () => { + /* + method Faz() { + assert true; + assert true; + assert false; // Error + } + */ + const computedIcons = VerificationGutterStatusView.computeGutterIcons( + vscode.Uri.parse('file:///woops.dfy'), + 5, new Map([ + [ '0,7', new vscode.Range(0, 0, 4, 1) ] + ]), [ + { nameRange: new vscode.Range(0, 7, 0, 10), status: PublishedVerificationStatus.FoundAllErrors } + ], [ + new vscode.Diagnostic(new vscode.Range(3, 2, 3, 14), 'could not prove assertion', vscode.DiagnosticSeverity.Error) + ]); + const expected = [ + LineVerificationStatus.Nothing, + LineVerificationStatus.AssertionVerifiedInErrorContext, + LineVerificationStatus.AssertionVerifiedInErrorContext, + LineVerificationStatus.AssertionFailed, + LineVerificationStatus.AssertionVerifiedInErrorContext + ]; + assert.deepStrictEqual(expected, computedIcons); + }); + test('computeGutterIconsResolved', () => { /* method Foo() { // Stale diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 79bfac77..421d820d 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -248,7 +248,12 @@ export default class VerificationGutterStatusView { resultStatus = LineVerificationStatus.AssertionFailed; } else { if(linesInErrorContext.has(line)) { - resultStatus = LineVerificationStatus.ErrorContext; + if(statusPerLine.get(line) === PublishedVerificationStatus.FoundAllErrors) { + // if we found all errors then a line with no error must be correct. + resultStatus = LineVerificationStatus.AssertionVerifiedInErrorContext; + } else { + resultStatus = LineVerificationStatus.ErrorContext; + } } else { resultStatus = LineVerificationStatus.Verified; } @@ -263,6 +268,7 @@ export default class VerificationGutterStatusView { progressStatus = GutterIconProgress.Running; break; case PublishedVerificationStatus.Error: + case PublishedVerificationStatus.FoundAllErrors: case PublishedVerificationStatus.Correct: case undefined: progressStatus = GutterIconProgress.Done; From fc9988a2e480d4ccfe6223097055ec594b7e7ebf Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 20 Sep 2023 16:08:47 +0200 Subject: [PATCH 30/30] Support for assertions in computed gutter icons --- .../api/verificationSymbolStatusParams.ts | 6 +- src/language/dafnyLanguageClient.ts | 2 + src/test/suite/extension.test.ts | 167 ++++++++++++------ src/ui/compilationStatusView.ts | 4 +- src/ui/verificationGutterStatusView.ts | 34 ++-- src/ui/verificationSymbolStatusView.ts | 3 +- 6 files changed, 147 insertions(+), 69 deletions(-) diff --git a/src/language/api/verificationSymbolStatusParams.ts b/src/language/api/verificationSymbolStatusParams.ts index d0fdc2d3..4f6f0c0c 100644 --- a/src/language/api/verificationSymbolStatusParams.ts +++ b/src/language/api/verificationSymbolStatusParams.ts @@ -15,7 +15,7 @@ export enum PublishedVerificationStatus { Stale = 0, // Not scheduled to be run Queued = 1, // Scheduled to be run but waiting for resources Running = 2, // Currently running - Error = 4, // Finished and had errors - Correct = 5, // Finished and was correct - FoundAllErrors = 6 // Finished, had errors and found them all + FoundSomeErrors = 4, // Finished and had errors + FoundAllErrors = 5, + Correct = 6 // Finished and was correct } \ No newline at end of file diff --git a/src/language/dafnyLanguageClient.ts b/src/language/dafnyLanguageClient.ts index d5e0635f..cc3c3383 100644 --- a/src/language/dafnyLanguageClient.ts +++ b/src/language/dafnyLanguageClient.ts @@ -28,6 +28,7 @@ function getLanguageServerLaunchArgsNew(): string[] { const specifiedCores = parseInt(Configuration.get(ConfigurationConstants.LanguageServer.VerificationVirtualCores)); // This is a temporary fix to prevent 0 cores from being used, since the languages server currently does not handle 0 cores correctly: https://github.com/dafny-lang/dafny/pull/3276 const cores = isNaN(specifiedCores) || specifiedCores === 0 ? Math.ceil((os.cpus().length + 1) / 2) : Math.max(1, specifiedCores); + const displayGutterIcons = Configuration.get(ConfigurationConstants.LanguageServer.DisplayGutterStatus); return [ `--verify-on:${verifyOn}`, `--verification-time-limit:${Configuration.get(ConfigurationConstants.LanguageServer.VerificationTimeLimit)}`, @@ -35,6 +36,7 @@ function getLanguageServerLaunchArgsNew(): string[] { `--cores:${cores}`, `--notify-ghostness:${Configuration.get(ConfigurationConstants.LanguageServer.MarkGhostStatements)}`, '--notify-line-verification-status:false', + `--show-assertions:${displayGutterIcons ? 'All' : 'Implicit'}`, ...getDafnyPluginsArgument(), ...launchArgs ]; diff --git a/src/test/suite/extension.test.ts b/src/test/suite/extension.test.ts index 23a880fd..8c073388 100644 --- a/src/test/suite/extension.test.ts +++ b/src/test/suite/extension.test.ts @@ -147,25 +147,24 @@ suite('Verification Gutter', () => { }); test('computeGutterIconsParseError', () => { - /* - method Foo() { - parse(;)Error - } + const source = ` +method Foo() { + parse(;)Error +} - method Bat() - ensures false - { - if (true) { - return; - } else { - return; - } - } +method Bat() + ensures false +{ + if (true) { + return; + } else { + return; + } +} - method Fom() { - assert true; - } - */ +method Fom() { + assert true; +}`.trimStart(); const uri = vscode.Uri.parse('file:///woops.dfy'); const parseError = new vscode.Diagnostic(new vscode.Range(1, 2, 1, 15), 'Some parse error', vscode.DiagnosticSeverity.Error); parseError.source = 'Parser'; @@ -194,8 +193,8 @@ suite('Verification Gutter', () => { LineVerificationStatus.VerifiedObsolete ]; const computedIcons = VerificationGutterStatusView.computeGutterIcons( - uri, - expected.length, undefined, undefined, [ + virtualDocument(uri, source), + false, undefined, undefined, [ parseError, outdatedReturnError ] @@ -203,17 +202,27 @@ suite('Verification Gutter', () => { assert.deepStrictEqual(expected, computedIcons); }); + function virtualDocument(uri: vscode.Uri, source: string): vscode.TextDocument { + const lines = source.split('\n'); + return { + uri: uri, + getText: (range: vscode.Range) => { + return lines[range.start.line]; + }, + lineCount: lines.length + } as vscode.TextDocument; + } + test('foundAllError', () => { - /* - method Faz() { - assert true; - assert true; - assert false; // Error - } - */ + const source = ` +method Faz() { + assert true; + assert true; + assert false; // Error +}`.trimStart(); const computedIcons = VerificationGutterStatusView.computeGutterIcons( - vscode.Uri.parse('file:///woops.dfy'), - 5, new Map([ + virtualDocument(vscode.Uri.parse('file:///woops.dfy'), source), + false, new Map([ [ '0,7', new vscode.Range(0, 0, 4, 1) ] ]), [ { nameRange: new vscode.Range(0, 7, 0, 10), status: PublishedVerificationStatus.FoundAllErrors } @@ -231,35 +240,34 @@ suite('Verification Gutter', () => { }); test('computeGutterIconsResolved', () => { - /* - method Foo() { // Stale - assert false; // No error - } + const source = ` +method Foo() { // Stale + assert false; // No error +} - method Bat() { // Stale - assert false; // Outdated error - } +method Bat() { // Stale + assert false; // Outdated error +} - method Bar() { // Queued - assert false; - } +method Bar() { // Queued + assert false; +} - method Baz() { // Running - assert false; - } +method Baz() { // Running + assert false; +} - method Fom() { // Correct - assert true; - } +method Fom() { // Correct + assert true; +} - method Faz() { // Error - assert true; - assert false; // Error - } - */ +method Faz() { // Error + assert true; + assert false; // Error +}`.trimStart(); const computedIcons = VerificationGutterStatusView.computeGutterIcons( - vscode.Uri.parse('file:///woops.dfy'), - 24, new Map([ + virtualDocument(vscode.Uri.parse('file:///woops.dfy'), source), + false, new Map([ [ '0,7', new vscode.Range(0, 0, 2, 1) ], [ '4,7', new vscode.Range(4, 0, 6, 1) ], [ '8,7', new vscode.Range(8, 0, 10, 1) ], @@ -272,7 +280,7 @@ suite('Verification Gutter', () => { { nameRange: new vscode.Range(8, 7, 8, 10), status: PublishedVerificationStatus.Queued }, { nameRange: new vscode.Range(12, 7, 12, 10), status: PublishedVerificationStatus.Running }, { nameRange: new vscode.Range(16, 7, 16, 10), status: PublishedVerificationStatus.Correct }, - { nameRange: new vscode.Range(20, 7, 20, 10), status: PublishedVerificationStatus.Error } + { nameRange: new vscode.Range(20, 7, 20, 10), status: PublishedVerificationStatus.FoundSomeErrors } ], [ new vscode.Diagnostic(new vscode.Range(5, 2, 5, 14), 'Outdated: could not prove assertion', vscode.DiagnosticSeverity.Warning), new vscode.Diagnostic(new vscode.Range(17, 2, 17, 14), 'some warning', vscode.DiagnosticSeverity.Warning), @@ -306,6 +314,61 @@ suite('Verification Gutter', () => { ]; assert.deepStrictEqual(expected, computedIcons); }); + + + test('foundSomeErrorsTrackAssertions', () => { + const source = ` +method FoundSomeErrors() { + if (*) { + assert false; + } else { + var x := 3 / 2; + } + assert false; +} +method FoundAllErrors() { + if (*) { + assert false; + } else { + var x := 3 / 2; + } + assert true; +}`.trimStart(); + const computedIcons = VerificationGutterStatusView.computeGutterIcons( + virtualDocument(vscode.Uri.parse('file:///woops.dfy'), source), + true, new Map([ + [ '0,7', new vscode.Range(0, 0, 7, 1) ], + [ '8,7', new vscode.Range(8, 0, 15, 1) ] + ]), [ + { nameRange: new vscode.Range(0, 7, 0, 22), status: PublishedVerificationStatus.FoundSomeErrors }, + { nameRange: new vscode.Range(8, 7, 8, 21), status: PublishedVerificationStatus.FoundAllErrors } + ], [ + new vscode.Diagnostic(new vscode.Range(2, 4, 2, 16), 'could not prove assertion', vscode.DiagnosticSeverity.Error), + new vscode.Diagnostic(new vscode.Range(4, 4, 4, 16), 'Assertion: division', vscode.DiagnosticSeverity.Hint), + new vscode.Diagnostic(new vscode.Range(6, 4, 6, 18), 'could not prove assertion', vscode.DiagnosticSeverity.Error), + new vscode.Diagnostic(new vscode.Range(10, 4, 10, 16), 'could not prove assertion', vscode.DiagnosticSeverity.Error), + new vscode.Diagnostic(new vscode.Range(12, 4, 12, 18), 'Assertion: division', vscode.DiagnosticSeverity.Hint) + ]); + const expected = [ + LineVerificationStatus.Nothing, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.AssertionFailed, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.AssertionFailed, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.Nothing, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.AssertionFailed, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.AssertionVerifiedInErrorContext, + LineVerificationStatus.ErrorContext, + LineVerificationStatus.AssertionVerifiedInErrorContext, + LineVerificationStatus.ErrorContext + ]; + assert.deepStrictEqual(expected, computedIcons); + }); }); suite('commands', () => { diff --git a/src/ui/compilationStatusView.ts b/src/ui/compilationStatusView.ts index 050720cb..10f49217 100644 --- a/src/ui/compilationStatusView.ts +++ b/src/ui/compilationStatusView.ts @@ -201,7 +201,7 @@ export default class CompilationStatusView { const document = await workspace.openTextDocument(uri); const statuses = params.namedVerifiables; - const completed = statuses.filter(v => v.status >= PublishedVerificationStatus.Error).length; + const completed = statuses.filter(v => v.status >= PublishedVerificationStatus.FoundSomeErrors).length; const queued = statuses.filter(v => v.status === PublishedVerificationStatus.Queued); const running = statuses.filter(v => v.status === PublishedVerificationStatus.Running); const total = statuses.length; @@ -216,7 +216,7 @@ export default class CompilationStatusView { } } else { const skipped = statuses.filter(v => v.status === PublishedVerificationStatus.Stale).length; - const errors = statuses.filter(v => v.status === PublishedVerificationStatus.Error + const errors = statuses.filter(v => v.status === PublishedVerificationStatus.FoundSomeErrors || v.status === PublishedVerificationStatus.FoundAllErrors); const errorCount = errors.length; const succeeded = completed - errorCount; diff --git a/src/ui/verificationGutterStatusView.ts b/src/ui/verificationGutterStatusView.ts index 421d820d..3894d6a4 100644 --- a/src/ui/verificationGutterStatusView.ts +++ b/src/ui/verificationGutterStatusView.ts @@ -1,5 +1,5 @@ /* eslint-disable max-depth */ -import { Range, window, ExtensionContext, workspace, TextEditor, TextEditorDecorationType, Uri, Position, DocumentSymbol, Diagnostic, DiagnosticSeverity, commands, languages } from 'vscode'; +import { Range, TextDocument, window, ExtensionContext, workspace, TextEditor, TextEditorDecorationType, Uri, Position, DocumentSymbol, Diagnostic, DiagnosticSeverity, commands, languages } from 'vscode'; import { Disposable } from 'vscode-languageclient'; import { IVerificationGutterStatusParams, @@ -149,7 +149,7 @@ export default class VerificationGutterStatusView { const document = await workspace.openTextDocument(uri); this.lineCountsPerDocument.set(document.uri, document.lineCount); - const perLineStatus = VerificationGutterStatusView.computeGutterIcons(uri, document.lineCount, nameToSymbolRange, verifiableRanges, diagnostics); + const perLineStatus = VerificationGutterStatusView.computeGutterIcons(document, true, nameToSymbolRange, verifiableRanges, diagnostics); this.updateUsingLineStatus({ uri: uri.toString(), perLineStatus: perLineStatus }); } @@ -167,8 +167,8 @@ export default class VerificationGutterStatusView { // eslint-disable-next-line max-params public static computeGutterIcons( - uri: Uri, - lineCount: number, + document: TextDocument, + assertionTracking: boolean, nameToSymbolRanges: Map | undefined, statuses: NamedVerifiableStatus[] | undefined, diagnostics: Diagnostic[]): LineVerificationStatus[] { @@ -177,6 +177,7 @@ export default class VerificationGutterStatusView { const lineToSymbolRange = new Map(); const linesInErrorContext = new Set(); const linesToSkip = new Set(); + const implicitAssertionLines = new Set(); if(nameToSymbolRanges !== undefined) { for(const range of nameToSymbolRanges.values()) { @@ -187,6 +188,13 @@ export default class VerificationGutterStatusView { } const perLineStatus: LineVerificationStatus[] = []; for(const diagnostic of diagnostics) { + const assertionMarker = diagnostic.message.startsWith('Assertion: ') + && diagnostic.severity === DiagnosticSeverity.Hint; + if(assertionMarker) { + // Just the first line of the assertion is sufficient. + implicitAssertionLines.add(diagnostic.range.start.line); + } + const outdatedError = diagnostic.message.startsWith('Outdated: '); if(diagnostic.severity !== DiagnosticSeverity.Error && !outdatedError) { continue; @@ -194,7 +202,7 @@ export default class VerificationGutterStatusView { const source = diagnostic.source ?? ''; for(const related of diagnostic.relatedInformation ?? []) { - if(related.location.uri === uri) { + if(related.location.uri === document.uri) { processErrorRange(related.location.range, source); } } @@ -202,7 +210,7 @@ export default class VerificationGutterStatusView { } if(nameToSymbolRanges === undefined || statuses === undefined) { - for(let line = 0; line < lineCount; line++) { + for(let line = 0; line < document.lineCount; line++) { statusPerLine.set(line, PublishedVerificationStatus.Stale); } } else { @@ -233,12 +241,15 @@ export default class VerificationGutterStatusView { } } - for(let line = 0; line < lineCount; line++) { + for(let line = 0; line < document.lineCount; line++) { if(linesToSkip.has(line)) { perLineStatus.push(LineVerificationStatus.Nothing); continue; } + const lineText = document.getText(new Range(line, 0, line + 1, 0)); + const isExplicitAssertion = lineText.trimStart().startsWith('assert'); + const error = lineToErrorSource.get(line); if(error === 'Parser' || error === 'Resolver') { perLineStatus.push(LineVerificationStatus.ResolutionError); @@ -248,8 +259,11 @@ export default class VerificationGutterStatusView { resultStatus = LineVerificationStatus.AssertionFailed; } else { if(linesInErrorContext.has(line)) { - if(statusPerLine.get(line) === PublishedVerificationStatus.FoundAllErrors) { - // if we found all errors then a line with no error must be correct. + const considerLineAsHavingAssertions + = !assertionTracking || implicitAssertionLines.has(line) || isExplicitAssertion; + if(statusPerLine.get(line) === PublishedVerificationStatus.FoundAllErrors + && considerLineAsHavingAssertions) { + // If we found all errors then an assertion with no error must be correct. resultStatus = LineVerificationStatus.AssertionVerifiedInErrorContext; } else { resultStatus = LineVerificationStatus.ErrorContext; @@ -267,7 +281,7 @@ export default class VerificationGutterStatusView { case PublishedVerificationStatus.Running: progressStatus = GutterIconProgress.Running; break; - case PublishedVerificationStatus.Error: + case PublishedVerificationStatus.FoundSomeErrors: case PublishedVerificationStatus.FoundAllErrors: case PublishedVerificationStatus.Correct: case undefined: diff --git a/src/ui/verificationSymbolStatusView.ts b/src/ui/verificationSymbolStatusView.ts index 1e5d2398..37a09d43 100644 --- a/src/ui/verificationSymbolStatusView.ts +++ b/src/ui/verificationSymbolStatusView.ts @@ -229,7 +229,7 @@ export default class VerificationSymbolStatusView { break; } case PublishedVerificationStatus.FoundAllErrors: - case PublishedVerificationStatus.Error: + case PublishedVerificationStatus.FoundSomeErrors: run.failed(testItem, [], getDuration()); itemFinished(); break; @@ -317,7 +317,6 @@ export default class VerificationSymbolStatusView { return item; } - public static convertRange(range: lspRange): Range { return new Range( VerificationSymbolStatusView.convertPosition(range.start),