Fix: Prevent diagnostics to "pass through"

RELEASE_NOTES.md

@@ -1,6 +1,7 @@
 # Upcoming
 
-- feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of waiting for all methods to be verified. (https://github.com/dafny-lang/dafny/pull/1944)
+- feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of after all methods are verified.
+- fix: No more display of previous obsolete verification diagnostics if newer are available. (https://github.com/dafny-lang/dafny/pull/2142)
 - feat: Live verification diagnostics for the language server (https://github.com/dafny-lang/dafny/pull/1942)
 - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080)
 

Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs

@@ -0,0 +1,65 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text.RegularExpressions;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+using OmniSharp.Extensions.JsonRpc;
+using OmniSharp.Extensions.LanguageServer.Protocol.Document;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics;
+
+[TestClass]
+public class ConcurrentLinearVerificationGutterStatusTester : LinearVerificationGutterStatusTester {
+ private const int MaxSimultaneousVerificationTasks = 3;
+
+ protected TestNotificationReceiver<VerificationStatusGutter>[] verificationStatusGutterReceivers =
+ new TestNotificationReceiver<VerificationStatusGutter>[MaxSimultaneousVerificationTasks];
+
+ private void NotifyAllVerificationGutterStatusReceivers(VerificationStatusGutter request) {
+ foreach (var receiver in verificationStatusGutterReceivers) {
+ receiver.NotificationReceived(request);
+ }
+ }
+
+ [TestInitialize]
+ public override async Task SetUp() {
+ for (var i = 0; i < verificationStatusGutterReceivers.Length; i++) {
+ verificationStatusGutterReceivers[i] = new();
+ }
+ verificationStatusGutterReceiver = new();
+ client = await InitializeClient(options =>
+ options
+ .AddHandler(DafnyRequestNames.VerificationStatusGutter,
+ NotificationHandler.For<VerificationStatusGutter>(NotifyAllVerificationGutterStatusReceivers))
+ );
+ }
+
+ [TestMethod]
+ public async Task EnsuresManyDocumentsCanBeVerifiedAtOnce() {
+ var result = new List<Task>();
+ for (var i = 0; i < MaxSimultaneousVerificationTasks; i++) {
+ result.Add(VerifyTrace(@"
+ . | | | I | | :predicate F(i: int) {
+ . | | | I | | : false // Should not be highlighted in gutter.
+ . | | | I | | :}
+ | | | I | | :
+ . S [S][ ][I][S][ ]:method H()
+ . S [=][=][-][~][O]: ensures F(1)
+ . S [=][=][-][~][=]:{//Next: { assert false;
+ . S [S][ ][I][S][ ]:}", $"testfile{i}.dfy", true, verificationStatusGutterReceivers[i]));
+ }
+
+ for (var i = 0; i < MaxSimultaneousVerificationTasks; i++) {
+ await result[i];
+ }
+
+ //await Task.WhenAll(result.ToArray());
+ }
+
+}

Source/DafnyLanguageServer.Test/Diagnostics/LinearVerificationDiagnosticTester.cs → Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs

@@ -16,17 +16,15 @@
 
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics;
 
-public abstract class LinearVerificationDiagnosticTester : ClientBasedLanguageServerTest {
- protected TestNotificationReceiver<VerificationStatusGutter> VerificationDiagnosticReceiver;
+public abstract class LinearVerificationGutterStatusTester : ClientBasedLanguageServerTest {
+ protected TestNotificationReceiver<VerificationStatusGutter> verificationStatusGutterReceiver;
  [TestInitialize]
  public override async Task SetUp() {
- diagnosticReceiver = new();
- VerificationDiagnosticReceiver = new();
+ verificationStatusGutterReceiver = new();
  client = await InitializeClient(options =>
  options
- .OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)
  .AddHandler(DafnyRequestNames.VerificationStatusGutter,
- NotificationHandler.For<VerificationStatusGutter>(VerificationDiagnosticReceiver.NotificationReceived))
+ NotificationHandler.For<VerificationStatusGutter>(verificationStatusGutterReceiver.NotificationReceived))
  );
  }
 
@@ -108,27 +106,29 @@ public static string ExtractCode(string tracesAndCode) {
 
  protected List<LineVerificationStatus[]> previousTraces = null;
 
- protected async Task<List<LineVerificationStatus[]>> GetAllLineVerificationDiagnostics(TextDocumentItem documentItem) {
+ protected async Task<List<LineVerificationStatus[]>> GetAllLineVerificationStatuses(
+ TextDocumentItem documentItem,
+ TestNotificationReceiver<VerificationStatusGutter> verificationStatusGutterReceiver
+ ) {
  var traces = new List<LineVerificationStatus[]>();
  var maximumNumberOfTraces = 50;
  var previousPerLineDiagnostics
  = previousTraces == null || previousTraces.Count == 0 ? null :
  previousTraces[^1].ToList();
- var nextDiagnostic = await diagnosticReceiver.AwaitNextNotificationAsync(CancellationToken);
  for (; maximumNumberOfTraces > 0; maximumNumberOfTraces--) {
- var verificationDiagnosticReport = await VerificationDiagnosticReceiver.AwaitNextNotificationAsync(CancellationToken);
- if (documentItem.Uri != verificationDiagnosticReport.Uri || documentItem.Version != verificationDiagnosticReport.Version) {
+ var verificationStatusGutter = await verificationStatusGutterReceiver.AwaitNextNotificationAsync(CancellationToken);
+ if (documentItem.Uri != verificationStatusGutter.Uri || documentItem.Version != verificationStatusGutter.Version) {
  continue;
  }
- var newPerLineDiagnostics = verificationDiagnosticReport.PerLineStatus.ToList();
+ var newPerLineDiagnostics = verificationStatusGutter.PerLineStatus.ToList();
  if ((previousPerLineDiagnostics != null
  && previousPerLineDiagnostics.SequenceEqual(newPerLineDiagnostics)) ||
  newPerLineDiagnostics.All(status => status == LineVerificationStatus.Nothing)) {
  continue;
  }
 
- traces.Add(verificationDiagnosticReport.PerLineStatus);
- if (NoMoreNotificationsToAwaitFrom(verificationDiagnosticReport)) {
+ traces.Add(verificationStatusGutter.PerLineStatus);
+ if (NoMoreNotificationsToAwaitFrom(verificationStatusGutter)) {
  break;
  }
 
@@ -139,10 +139,10 @@ var previousPerLineDiagnostics
  return traces;
  }
 
- private static bool NoMoreNotificationsToAwaitFrom(VerificationStatusGutter verificationDiagnosticReport) {
- return verificationDiagnosticReport.PerLineStatus.Contains(LineVerificationStatus.ResolutionError) ||
- verificationDiagnosticReport.PerLineStatus.All(IsNotIndicatingProgress) ||
- verificationDiagnosticReport.PerLineStatus.All(status => status == LineVerificationStatus.Nothing);
+ private static bool NoMoreNotificationsToAwaitFrom(VerificationStatusGutter verificationGutterStatus) {
+ return verificationGutterStatus.PerLineStatus.Contains(LineVerificationStatus.ResolutionError) ||
+ verificationGutterStatus.PerLineStatus.All(IsNotIndicatingProgress) ||
+ verificationGutterStatus.PerLineStatus.All(status => status == LineVerificationStatus.Nothing);
  }
 
  /// <summary>
@@ -218,19 +218,24 @@ Position IndexToPosition(int index) {
  }
 
  // If testTrace is false, codeAndTree should not contain a trace to test.
- public async Task VerifyTrace(string codeAndTrace, bool testTrace = true) {
+ public async Task VerifyTrace(string codeAndTrace, string fileName = null, bool testTrace = true,
+ TestNotificationReceiver<VerificationStatusGutter> verificationStatusGutterReceiver = null
+ ) {
+ if (verificationStatusGutterReceiver == null) {
+ verificationStatusGutterReceiver = this.verificationStatusGutterReceiver;
+ }
  codeAndTrace = codeAndTrace[0] == '\n' ? codeAndTrace.Substring(1) :
  codeAndTrace.Substring(0, 2) == "\r\n" ? codeAndTrace.Substring(2) :
  codeAndTrace;
  var codeAndChanges = testTrace ? ExtractCode(codeAndTrace) : codeAndTrace;
  var (code, changes) = ExtractCodeAndChanges(codeAndChanges);
- var documentItem = CreateTestDocument(code);
- await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+ var documentItem = CreateTestDocument(code, fileName);
+ client.OpenDocument(documentItem);
  var traces = new List<LineVerificationStatus[]>();
- traces.AddRange(await GetAllLineVerificationDiagnostics(documentItem));
+ traces.AddRange(await GetAllLineVerificationStatuses(documentItem, verificationStatusGutterReceiver));
  foreach (var (range, inserted) in changes) {
  ApplyChange(ref documentItem, range, inserted);
- traces.AddRange(await GetAllLineVerificationDiagnostics(documentItem));
+ traces.AddRange(await GetAllLineVerificationStatuses(documentItem, verificationStatusGutterReceiver));
  }
 
  if (testTrace) {

Source/DafnyLanguageServer.Test/Diagnostics/ReorderingVerificationDiagnosticTester.cs → Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs

@@ -21,20 +21,18 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics;
 /// methods priorities for verification being set automatically.
 /// </summary>
 [TestClass]
-public class ReorderingVerificationDiagnosticTester : LinearVerificationDiagnosticTester {
+public class ReorderingVerificationGutterStatusTester : LinearVerificationGutterStatusTester {
  private ListeningTextDocumentLoader textDocumentLoader;
  private const int MaxTestExecutionTimeMs = 10000;
 
  [TestInitialize]
  public override async Task SetUp() {
  DafnyOptions.Install(DafnyOptions.Create("-proverOpt:SOLVER=noop"));
- diagnosticReceiver = new();
- VerificationDiagnosticReceiver = new();
+ verificationStatusGutterReceiver = new();
  client = await InitializeClient(options =>
  options
- .OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)
  .AddHandler(DafnyRequestNames.VerificationStatusGutter,
- NotificationHandler.For<VerificationStatusGutter>(VerificationDiagnosticReceiver.NotificationReceived))
+ NotificationHandler.For<VerificationStatusGutter>(verificationStatusGutterReceiver.NotificationReceived))
  , serverOptions => {
  serverOptions.Services.AddSingleton<ITextDocumentLoader>(serviceProvider => {
  textDocumentLoader = new ListeningTextDocumentLoader(

Source/DafnyLanguageServer.Test/Diagnostics/SimpleLinearVerificationDiagnosticTester.cs → Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs

@@ -13,15 +13,15 @@
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics;
 
 [TestClass]
-public class SimpleLinearVerificationDiagnosticTester : LinearVerificationDiagnosticTester {
+public class SimpleLinearVerificationGutterStatusTester : LinearVerificationGutterStatusTester {
  private const int MaxTestExecutionTimeMs = 10000;
 
  // To add a new test, just call VerifyTrace on a given program,
  // the test will fail and give the correct output that can be use for the test
  // Add '//Next<n>:' to edit a line multiple times
 
  [TestMethod, Timeout(MaxTestExecutionTimeMs)]
- public async Task EnsureVerificationDiagnosticsAreWorking() {
+ public async Task EnsureVerificationGutterStatusIsWorking() {
  await VerifyTrace(@"
  . | | | I I | | :predicate Ok() {
  . | | | I I | | : true