No duplicate symbol status (#4523)

### Changes

- No longer resend the same symbolStatus notification
- No longer migrate verification results from a file that was not
changed

### Testing
- Added two unit tests for the above fixes

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs

@@ -15,6 +15,47 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization;
 
 public class VerificationStatusTest : ClientBasedLanguageServerTest {
 
+ [Fact]
+ public async Task DoNotMigrateWrongUri() {
+ var sourceA = @"
+method NotAffectedByChange() {
+ assert false;
+}
+".TrimStart();
+
+ var sourceB = @"
+// 1
+// 2
+// 3
+method ShouldNotBeAffectedByChange() {
+ assert false;
+}
+".TrimStart();
+
+ var directory = Path.GetRandomFileName();
+ await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName));
+ var documentA = await CreateAndOpenTestDocument(sourceA, Path.Combine(directory, "sourceA.dfy"));
+ await WaitUntilAllStatusAreCompleted(documentA);
+ var documentB = await CreateAndOpenTestDocument(sourceB, Path.Combine(directory, "sourceB.dfy"));
+ await WaitUntilAllStatusAreCompleted(documentB);
+ ApplyChange(ref documentA, new Range(3, 0, 3, 0), "// change\n");
+ await AssertNoVerificationStatusIsComing(documentB, CancellationToken);
+ }
+
+ [Fact]
+ public async Task DoNotResendAfterNoopChange() {
+ var source = @"
+method WillVerify() {
+ assert false;
+}
+".TrimStart();
+
+ var document = await CreateAndOpenTestDocument(source);
+ var firstStatus = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
+ ApplyChange(ref document, new Range(3, 0, 3, 0), "//change comment\n");
+ await AssertNoVerificationStatusIsComing(document, CancellationToken);
+ }
+
  [Fact]
  public async Task TryingToVerifyShowsUpAsQueued() {
  var source = @"
@@ -347,12 +388,14 @@ await SetUp(options => {
  var documentItem = CreateTestDocument(SlowToVerify, "ManualRunCancelCancelRunRun.dfy");
  await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
  var stale = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
+ Assert.Equal(documentItem.Uri, stale.Uri);
  Assert.Equal(PublishedVerificationStatus.Stale, stale.NamedVerifiables[0].Status);
  await AssertNoVerificationStatusIsComing(documentItem, CancellationToken);
 
  var methodHeader = new Position(0, 21);
  await client.RunSymbolVerification(new TextDocumentIdentifier(documentItem.Uri), methodHeader, CancellationToken);
  var running0 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
+ Assert.Equal(documentItem.Uri, running0.Uri);
  Assert.Equal(PublishedVerificationStatus.Queued, running0.NamedVerifiables[0].Status);
 
  var running1 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
@@ -432,8 +475,6 @@ await SetUp(options => {
 
  await client.SaveDocumentAndWaitAsync(documentItem, CancellationToken);
 
- var stale2 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
- Assert.Equal(PublishedVerificationStatus.Stale, stale2.NamedVerifiables[0].Status);
  var queued = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
  Assert.Equal(PublishedVerificationStatus.Queued, queued.NamedVerifiables[0].Status);
  var running = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
@@ -468,8 +509,10 @@ await SetUp(options => {
  }
 
  private async Task<FileVerificationStatus> WaitUntilAllStatusAreCompleted(TextDocumentIdentifier documentId) {
- var lastDocument = (CompilationAfterResolution)(await Projects.GetLastDocumentAsync(documentId));
- var symbols = lastDocument!.Verifiables.ToHashSet();
+ var compilationAfterParsing = await Projects.GetLastDocumentAsync(documentId);
+ var lastDocument = (CompilationAfterResolution)compilationAfterParsing;
+ var uri = documentId.Uri.ToUri();
+ var symbols = lastDocument!.Verifiables.Where(v => v.Tok.Uri == uri).ToHashSet();
  FileVerificationStatus beforeChangeStatus;
  do {
  beforeChangeStatus = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);

Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs

@@ -268,6 +268,7 @@ public async Task AssertNoVerificationStatusIsComing(TextDocumentItem documentIt
  client.DidCloseTextDocument(new DidCloseTextDocumentParams {
  TextDocument = verificationDocumentItem
  });
+ var emptyReport = await verificationStatusReceiver.AwaitNextNotificationAsync(cancellationToken);
  }
 
  public async Task AssertNoGhostnessIsComing(CancellationToken cancellationToken) {

Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs

@@ -19,7 +19,38 @@ public class CompilationStatusNotificationTest : ClientBasedLanguageServerTest {
  private const int MaxTestExecutionTimeMs = 10000;
 
  [Fact]
- public async Task MultipleDocuments() {
+ public async Task MultipleDocumentsFailedResolution() {
+ var source = @"
+method Foo() returns (x: int) {
+ return 2;
+}".TrimStart();
+ var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
+ Directory.CreateDirectory(directory);
+ await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName));
+ var secondFilePath = Path.Combine(directory, "RunWithMultipleDocuments2.dfy");
+ await File.WriteAllTextAsync(secondFilePath, source.Replace("Foo", "Bar").Replace("2", "true"));
+ var documentItem1 = await CreateAndOpenTestDocument(source, Path.Combine(directory, "RunWithMultipleDocuments1.dfy"));
+
+ var expectedStatuses = new[] {
+ CompilationStatus.ResolutionStarted,
+ CompilationStatus.ResolutionFailed
+ };
+ var documents = new[] { documentItem1.Uri, DocumentUri.File(secondFilePath) };
+ foreach (var expectedStatus in expectedStatuses) {
+ var statuses = new Dictionary<DocumentUri, CompilationStatusParams>();
+ foreach (var _ in documents) {
+ var statusParams = await compilationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
+ statuses.Add(statusParams.Uri, statusParams);
+ }
+ foreach (var document in documents) {
+ var status = statuses[document];
+ Assert.Equal(expectedStatus, status.Status);
+ }
+ }
+ }
+
+ [Fact]
+ public async Task MultipleDocumentsSuccessfulResolution() {
  var source = @"
 method Foo() returns (x: int) {
  return 2;
@@ -32,7 +63,8 @@ method Foo() returns (x: int) {
  var documentItem1 = await CreateAndOpenTestDocument(source, Path.Combine(directory, "RunWithMultipleDocuments1.dfy"));
 
  var expectedStatuses = new[] {
- CompilationStatus.ResolutionStarted
+ CompilationStatus.ResolutionStarted,
+ CompilationStatus.ResolutionSucceeded
  };
  var documents = new[] { documentItem1.Uri, DocumentUri.File(secondFilePath) };
  foreach (var expectedStatus in expectedStatuses) {
@@ -166,10 +198,12 @@ method Abs(x: int) returns (y: int)
  var documentItem1 = CreateTestDocument(source, "test_1.dfy");
  await client.OpenDocumentAndWaitAsync(documentItem1, CancellationToken);
  await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted);
+ await AssertProgress(documentItem1, CompilationStatus.ResolutionSucceeded);
  await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem1);
  var documentItem2 = CreateTestDocument(source, "test_2dfy");
  await client.OpenDocumentAndWaitAsync(documentItem2, CancellationToken);
  await AssertProgress(documentItem2, CompilationStatus.ResolutionStarted);
+ await AssertProgress(documentItem2, CompilationStatus.ResolutionSucceeded);
  await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem2);
  }
 
@@ -190,11 +224,13 @@ method Abs(x: int) returns (y: int)
  await client.OpenDocumentAndWaitAsync(documentItem1, CancellationToken);
  await client.SaveDocumentAndWaitAsync(documentItem1, CancellationToken);
  await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted);
+ await AssertProgress(documentItem1, CompilationStatus.ResolutionSucceeded);
  await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem1);
  var documentItem2 = CreateTestDocument(source, "test_2dfy");
  await client.OpenDocumentAndWaitAsync(documentItem2, CancellationToken);
  await client.SaveDocumentAndWaitAsync(documentItem2, CancellationToken);
  await AssertProgress(documentItem2, CompilationStatus.ResolutionStarted);
+ await AssertProgress(documentItem2, CompilationStatus.ResolutionSucceeded);
  await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem2);
  }
 

Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs

@@ -43,7 +43,7 @@ public IdeState InitialIdeState(Compilation initialCompilation, DafnyOptions opt
  var program = new EmptyNode();
  return ToIdeState(new IdeState(initialCompilation.Version, initialCompilation, program,
  ImmutableDictionary<Uri, IReadOnlyList<Diagnostic>>.Empty,
- SymbolTable.Empty(), LegacySignatureAndCompletionTable.Empty(options, initialCompilation.Project), new(),
+ SymbolTable.Empty(), LegacySignatureAndCompletionTable.Empty(options, initialCompilation.Project), ImmutableDictionary<Uri, Dictionary<Range, IdeVerificationResult>>.Empty,
  Array.Empty<Counterexample>(),
  ImmutableDictionary<Uri, IReadOnlyList<Range>>.Empty,
  initialCompilation.RootUris.ToDictionary(uri => uri, uri => new DocumentVerificationTree(program, uri))

Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs

@@ -125,7 +125,7 @@ IdeVerificationResult MergeVerifiable(ICanVerify canVerify) {
  kv => kv.Key,
  kv => (IReadOnlyList<Diagnostic>)kv.Value.Select(d => d.ToLspDiagnostic()).ToList()),
  VerificationTrees = VerificationTrees.ToDictionary(kv => kv.Key, kv => (DocumentVerificationTree)kv.Value.GetCopyForNotification()),
- VerificationResults = Verifiables.GroupBy(l => l.NameToken.Uri).ToDictionary(k => k.Key,
+ VerificationResults = Verifiables.GroupBy(l => l.NameToken.Uri).ToImmutableDictionary(k => k.Key,
  k => k.GroupBy(l => l.NameToken.GetLspRange()).ToDictionary(
  l => l.Key,
  l => MergeResults(l.Select(MergeVerifiable))))

Source/DafnyLanguageServer/Workspace/IdeState.cs

@@ -31,7 +31,7 @@ public record IdeState(
  IReadOnlyDictionary<Uri, IReadOnlyList<Diagnostic>> ResolutionDiagnostics,
  SymbolTable SymbolTable,
  LegacySignatureAndCompletionTable SignatureAndCompletionTable,
- Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> VerificationResults,
+ ImmutableDictionary<Uri, Dictionary<Range, IdeVerificationResult>> VerificationResults,
  IReadOnlyList<Counterexample> Counterexamples,
  IReadOnlyDictionary<Uri, IReadOnlyList<Range>> GhostRanges,
  IReadOnlyDictionary<Uri, DocumentVerificationTree> VerificationTrees
@@ -50,32 +50,36 @@ public IdeState Migrate(Migrator migrator, int version) {
  };
  }
 
- private Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> MigrateImplementationViews(Migrator migrator,
- Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> oldVerificationDiagnostics) {
- return oldVerificationDiagnostics.ToDictionary(kv => kv.Key, kv => {
- var result = new Dictionary<Range, IdeVerificationResult>();
- foreach (var entry in kv.Value) {
- var newOuterRange = migrator.MigrateRange(entry.Key);
- if (newOuterRange == null) {
- continue;
- }
+ private ImmutableDictionary<Uri, Dictionary<Range, IdeVerificationResult>> MigrateImplementationViews(
+ Migrator migrator,
+ ImmutableDictionary<Uri, Dictionary<Range, IdeVerificationResult>> oldVerificationDiagnostics) {
+ var uri = migrator.MigratedUri;
+ var previous = oldVerificationDiagnostics.GetValueOrDefault(uri);
+ if (previous == null) {
+ return oldVerificationDiagnostics;
+ }
+ var result = new Dictionary<Range, IdeVerificationResult>();
+ foreach (var entry in previous) {
+ var newOuterRange = migrator.MigrateRange(entry.Key);
+ if (newOuterRange == null) {
+ continue;
+ }
 
- var newValue = new Dictionary<string, IdeImplementationView>();
- foreach (var innerEntry in entry.Value.Implementations) {
- var newInnerRange = migrator.MigrateRange(innerEntry.Value.Range);
- if (newInnerRange != null) {
- newValue.Add(innerEntry.Key, innerEntry.Value with {
- Range = newInnerRange,
- Diagnostics = migrator.MigrateDiagnostics(innerEntry.Value.Diagnostics)
- });
- }
+ var newValue = new Dictionary<string, IdeImplementationView>();
+ foreach (var innerEntry in entry.Value.Implementations) {
+ var newInnerRange = migrator.MigrateRange(innerEntry.Value.Range);
+ if (newInnerRange != null) {
+ newValue.Add(innerEntry.Key, innerEntry.Value with {
+ Range = newInnerRange,
+ Diagnostics = migrator.MigrateDiagnostics(innerEntry.Value.Diagnostics)
+ });
  }
-
- result.Add(newOuterRange, entry.Value with { Implementations = newValue });
  }
 
- return result;
- });
+ result.Add(newOuterRange, entry.Value with { Implementations = newValue });
+ }
+
+ return oldVerificationDiagnostics.SetItem(uri, result);
  }
 
  public IReadOnlyDictionary<Range, IdeVerificationResult> GetVerificationResults(Uri uri) {

Source/DafnyLanguageServer/Workspace/Migrator.cs

@@ -1,3 +1,4 @@
+using System;
 using System.Collections.Generic;
 using System.Collections.Immutable;
 using System.Linq;
@@ -8,6 +9,7 @@
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
 namespace Microsoft.Dafny.LanguageServer.Workspace.ChangeProcessors;
 
@@ -22,6 +24,8 @@ public class Migrator {
 
  private readonly Dictionary<TextDocumentContentChangeEvent, Position> getPositionAtEndOfAppliedChangeCache = new();
 
+ public Uri MigratedUri => changeParams.TextDocument.Uri.ToUri();
+
  public Migrator(
  ILogger<Migrator> logger,
  ILogger<LegacySignatureAndCompletionTable> loggerSymbolTable,

Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs

@@ -34,65 +34,78 @@ public async Task PublishNotifications(IdeState previousState, IdeState state) {
  return;
  }
 
- PublishProgressStatus(previousState, state);
+ PublishProgress(previousState, state);
  PublishGhostness(previousState, state);
  await PublishDiagnostics(state);
  }
 
- private void PublishProgressStatus(IdeState previousState, IdeState state) {
- foreach (var uri in state.Compilation.RootUris) {
- // TODO, still have to check for ownedness
+ private void PublishProgress(IdeState previousState, IdeState state) {
+ // Some global progress values, such as ResolutionSucceeded, will trigger the symbol progress to be displayed.
+ // To ensure that the displayed progress is always up-to-date,
+ // we must publish symbol progress before publishing the global one.
+
+ // Better would be to have a single notification API with the schema { globalProgress, symbolProgress }
+ // so this problem can not occur, although that would require the "symbolProgress" part to be able to contain a
+ // "no-update" value to prevent having to send many duplicate symbolProgress updates.
+
+ PublishSymbolProgress(previousState, state);
+ PublishGlobalProgress(previousState, state);
+ }
 
- var current = GetProgressStatus(state, uri);
- var previous = GetProgressStatus(previousState, uri);
+ private void PublishSymbolProgress(IdeState previousState, IdeState state) {
+ foreach (var uri in state.Compilation.RootUris) {
+ var previous = GetFileVerificationStatus(previousState, uri);
+ var current = GetFileVerificationStatus(state, uri);
 
  if (Equals(current, previous)) {
  continue;
  }
 
- switch (current) {
- case ResolutionProgressStatus resolutionProgressStatus:
- languageServer.SendNotification(new CompilationStatusParams {
- Uri = uri,
- Version = filesystem.GetVersion(uri),
- Status = resolutionProgressStatus.CompilationStatus,
- Message = null
- });
- break;
- case VerificationProgressStatus verificationProgressStatus:
- languageServer.TextDocument.SendNotification(DafnyRequestNames.VerificationSymbolStatus, verificationProgressStatus.FileVerificationStatus);
- break;
- }
+ languageServer.TextDocument.SendNotification(DafnyRequestNames.VerificationSymbolStatus, current);
  }
-
  }
 
- private abstract record ProgressStatus;
+ private void PublishGlobalProgress(IdeState previousState, IdeState state) {
+ foreach (var uri in state.Compilation.RootUris) {
+ // TODO, still have to check for ownedness
 
- private sealed record VerificationProgressStatus(FileVerificationStatus FileVerificationStatus) : ProgressStatus;
+ var current = GetGlobalProgress(state);
+ var previous = GetGlobalProgress(previousState);
 
- private sealed record ResolutionProgressStatus(CompilationStatus CompilationStatus) : ProgressStatus;
+ if (Equals(current, previous)) {
+ continue;
+ }
+
+ languageServer.SendNotification(new CompilationStatusParams {
+ Uri = uri,
+ Version = filesystem.GetVersion(uri),
+ Status = current,
+ Message = null
+ });
+ }
+
+ }
 
- private ProgressStatus GetProgressStatus(IdeState state, Uri uri) {
- var hasResolutionDiagnostics = (state.ResolutionDiagnostics.GetValueOrDefault(uri) ?? Enumerable.Empty<Diagnostic>()).
+ private CompilationStatus GetGlobalProgress(IdeState state) {
+ var hasResolutionDiagnostics = state.ResolutionDiagnostics.Values.SelectMany(x => x).
  Any(d => d.Severity == DiagnosticSeverity.Error);
  if (state.Compilation is CompilationAfterResolution) {
  if (hasResolutionDiagnostics) {
- return new ResolutionProgressStatus(CompilationStatus.ResolutionFailed);
+ return CompilationStatus.ResolutionFailed;
  }
 
- return new VerificationProgressStatus(GetFileVerificationStatus(state, uri));
+ return CompilationStatus.ResolutionSucceeded;
  }
 
  if (state.Compilation is CompilationAfterParsing) {
  if (hasResolutionDiagnostics) {
- return new ResolutionProgressStatus(CompilationStatus.ParsingFailed);
+ return CompilationStatus.ParsingFailed;
  }
 
- return new ResolutionProgressStatus(CompilationStatus.ResolutionStarted);
+ return CompilationStatus.ResolutionStarted;
  }
 
- return new ResolutionProgressStatus(CompilationStatus.Parsing);
+ return CompilationStatus.Parsing;
  }
 
  private FileVerificationStatus GetFileVerificationStatus(IdeState state, Uri uri) {

Source/DafnyLanguageServer/Workspace/Notifications/CompilationStatus.cs

@@ -10,6 +10,7 @@ public enum CompilationStatus {
  Parsing,
  ParsingFailed,
  ResolutionStarted,
- ResolutionFailed
+ ResolutionFailed,
+ ResolutionSucceeded
  }
 }