Verification Gutter Status (#147)

Features implemented:
- Renders the linear verification statuses in the left gutter with static and animated icons
- That same diagnostics are also rendered in the right scrollbar for a preview of the entire file
- Option to deactivate verification gutter status (on by default)
- Parse errors will gray out the gutter display after 2 seconds the first time, and immediately after every subsequent resolution or parsing errors
- The first "obsolete" line diagnostics is not shown until 2 seconds after it is first set up, so that there is less flickering for the current method being edited

Author: MikaelMayer

images/error-obsolete.png

@@ -155,6 +155,11 @@
           "default": "true",
           "description": "Mark ghost statements in the code (requires restart and Dafny 3.4.0+)"
         },
+        "dafny.displayGutterStatus": {
+          "type": "boolean",
+          "default": "true",
+          "description": "Display verification status in the gutter (requires restart and Dafny 3.7.0+)"
+        },
         "dafny.dafnyPlugins": {
           "type": "array",
           "items": {

images/error-obsolete_gray.png

@@ -24,6 +24,7 @@ export namespace ConfigurationConstants {
     export const VerificationCachingPolicy = 'verificationCachingPolicy';
     export const MarkGhostStatements = 'markGhostStatements';
     export const DafnyPlugins = 'dafnyPlugins';
+    export const DisplayGutterStatus = 'displayGutterStatus';
   }
 
   export namespace Compiler {

images/error-range-end-obsolete.png

@@ -0,0 +1,77 @@
+import { DocumentUri, integer } from 'vscode-languageclient';
+
+export interface IVerificationGutterStatusParams {
+  uri: DocumentUri;
+  version?: integer;
+  perLineStatus: LineVerificationStatus[];
+}
+
+// Except for cosmetics, this enumeration is a copy-paste from Dafny's
+// Source/DafnyLanguageServer/Workspace/Notifications/VerificationDiagnosticsParams.cs
+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,
+  VerifiedObsolete = 201,
+  VerifiedVerifying = 202,
+  // Also applicable for empty spaces if they are not surrounded by errors.
+  Verified = 200,
+ // For trees containing children with errors (e.g. methods)
+  ErrorContextObsolete = 301,
+  ErrorContextVerifying = 302,
+  ErrorContext = 300,
+  // For individual assertions in error ranges
+  AssertionVerifiedInErrorContextObsolete = 351,
+  AssertionVerifiedInErrorContextVerifying = 352,
+  AssertionVerifiedInErrorContext = 350,
+  // For specific lines which have errors on it. They take over verified assertions
+  AssertionFailedObsolete = 401,
+  AssertionFailedVerifying = 402,
+  AssertionFailed = 400,
+  // For lines containing resolution or parse errors
+  ResolutionError = 500,
+  // Cosmetics, not part of server's output
+  ErrorContextStart = 310,
+  ErrorContextStartObsolete = 311,
+  ErrorContextStartVerifying = 312,
+  ErrorContextEnd = 320,
+  ErrorContextEndObsolete = 321,
+  ErrorContextEndVerifying = 322
+}
+
+export enum ScrollColor {
+  Unknown = '#00000000',
+  Error = '#fe536aa0',
+  ErrorActive = '#fe536ad0',
+  ErrorRange = '#fad00080',
+  Verified = '#62b45580'
+}
+
+export const obsoleteLineVerificationStatus: LineVerificationStatus[] = [
+  LineVerificationStatus.AssertionFailedObsolete,
+  LineVerificationStatus.VerifiedObsolete,
+  LineVerificationStatus.ErrorContextObsolete,
+  LineVerificationStatus.ErrorContextStartObsolete,
+  LineVerificationStatus.ErrorContextEndObsolete
+];
+export const verifyingLineVerificationStatus: LineVerificationStatus[] = [
+  LineVerificationStatus.Verifying,
+  LineVerificationStatus.AssertionFailedVerifying,
+  LineVerificationStatus.ErrorContextEndVerifying,
+  LineVerificationStatus.ErrorContextVerifying,
+  LineVerificationStatus.ErrorContextStartVerifying,
+  LineVerificationStatus.VerifiedVerifying,
+  LineVerificationStatus.AssertionVerifiedInErrorContextVerifying
+];
+export const nonErrorLineVerificationStatus: LineVerificationStatus[] = [
+  LineVerificationStatus.Scheduled,
+  LineVerificationStatus.Nothing,
+  LineVerificationStatus.Verified,
+  LineVerificationStatus.VerifiedObsolete,
+  LineVerificationStatus.VerifiedVerifying,
+  LineVerificationStatus.Verifying
+];

images/error-range-end-verifying-2.png

@@ -8,6 +8,7 @@ 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 { getLanguageServerRuntimePath } from './dafnyInstallation';
 
 const LanguageServerId = 'dafny-vscode';
@@ -21,6 +22,7 @@ function getLanguageServerLaunchArgs(): string[] {
     getVerifierCachingPolicy(),
     getVerifierVirtualCoresArgument(),
     getMarkGhostStatementsArgument(),
+    getDisplayGutterStatusArgument(),
     ...getDafnyPluginsArgument(),
     ...launchArgs
   ];
@@ -48,6 +50,10 @@ function getVerifierVirtualCoresArgument(): string {
   return `--verifier:vcscores=${Configuration.get<string>(ConfigurationConstants.LanguageServer.VerificationVirtualCores)}`;
 }
 
+function getDisplayGutterStatusArgument(): string {
+  return `--verifier:gutterStatus=${Configuration.get<string>(ConfigurationConstants.LanguageServer.DisplayGutterStatus)}`;
+}
+
 function getMarkGhostStatementsArgument(): string {
   return `--ghost:markStatements=${Configuration.get<string>(ConfigurationConstants.LanguageServer.MarkGhostStatements)}`;
 }
@@ -101,6 +107,10 @@ 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 onCompilationStatus(callback: (params: ICompilationStatusParams) => void): Disposable {
     return this.onNotification('dafny/compilation/status', callback);
   }

images/error-range-end-verifying.png

@@ -1,5 +1,4 @@
 import { StatusBarAlignment, StatusBarItem, TextDocument, window, workspace, ExtensionContext } from 'vscode';
-
 import { CompilationStatus, ICompilationStatusParams, IVerificationCompletedParams, IVerificationStartedParams } from '../language/api/compilationStatus';
 import { DafnyLanguageClient } from '../language/dafnyLanguageClient';
 import { getVsDocumentPath } from '../tools/vscode';
@@ -23,7 +22,9 @@ function toStatusMessage(status: CompilationStatus, message?: string | null): st
   case CompilationStatus.VerificationSucceeded:
     return Messages.CompilationStatus.VerificationSucceeded;
   case CompilationStatus.VerificationFailed:
-    return Messages.CompilationStatus.VerificationFailed;
+    return message != null
+      ? `${Messages.CompilationStatus.VerificationFailed} ${message}`
+      : `${Messages.CompilationStatus.VerificationFailed}`;
   }
 }
 

images/error-range-end.png

@@ -6,6 +6,7 @@ import CompileCommands from './compileCommands';
 import CounterExamplesView from './counterExamplesView';
 import DafnyVersionView from './dafnyVersionView';
 import GhostDiagnosticsView from './ghostDiagnosticsView';
+import VerificationGutterStatusView from './verificationGutterStatusView';
 
 export default async function createAndRegisterDafnyIntegration(
   context: ExtensionContext,
@@ -14,6 +15,7 @@ export default async function createAndRegisterDafnyIntegration(
 ): Promise<void> {
   CounterExamplesView.createAndRegister(context, languageClient);
   GhostDiagnosticsView.createAndRegister(context, languageClient);
+  VerificationGutterStatusView.createAndRegister(context, languageClient);
   CompileCommands.createAndRegister(context);
   CompilationStatusView.createAndRegister(context, languageClient);
   await DafnyVersionView.createAndRegister(context, languageServerVersion);