Move compilation status updates to notification publisher (#4454)

Fixes #4451

### Changes
- symbolStatus notifications are resent after any document change is
made.
- "Parsing" is no longer sent when opening a file because it's the
default state for a file. This requires an update on the client to
return to the old behavior, but in the meantime it's OK for the client
to have this tiny regression.
- "Preparing Verification" no longer exists as a notification. Because
one verifiable can be preparing verification while another is verifying,
there is no longer a global "Preparing verification" state so this
notification lost its meaning. We can bring something like this back but
on a more granular level.
- "Resolution Succeeded (not verified)" (UI name) / CompilationSucceeded
(server name) no longer exists as a notification. This sat between
ResolutionStarted and symbolStatus notifications that indicated which
symbols could be verified, but in practice was never shown because
immediately after it symbolStatus notifications would be sent that
trigger a status like "Verified X declarations, skipped Y"
- `CompilationManager` no longer sends any status updates to the IDE
client, bringing it closer to being able to be moved to `DafnyCore` and
used by the CLI.

### Testing
- Updated automating tests

<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/DeclarationLocationMigrationTest.cs

@@ -126,7 +126,7 @@ await ApplyChangeAndWaitCompletionAsync(
         Assert.Equal(new Range((10, 6), (10, 7)), location.Name);
         Assert.Equal(new Range((10, 0), (11, 0)), location.Declaration);
       } catch (AssertActualExpectedException) {
-        await output.WriteLineAsync($"state version is {state.Version}, diagnostics: {state.GetDiagnostics().Values.Stringify()}");
+        await output.WriteLineAsync($"state version is {state.Version}, diagnostics: {state.GetAllDiagnostics().Stringify()}");
         var programString = new StringWriter();
         var printer = new Printer(programString, DafnyOptions.Default);
         printer.PrintProgram((Program)state.Program, true);

Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs

@@ -28,7 +28,7 @@ method Test() {
     await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
     var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
     Assert.NotNull(document);
-    Assert.All(document.GetDiagnostics(), a => Assert.Empty(a.Value));
+    Assert.Empty(document.GetAllDiagnostics());
   }
 
   // https://github.com/dafny-lang/language-server-csharp/issues/40

Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs

@@ -148,7 +148,7 @@ await ApplyChangeAndWaitCompletionAsync(
         Assert.True(state.SignatureAndCompletionTable.TryGetSymbolAt((22, 10), out var symbol));
         Assert.Equal("y", symbol.Name);
       } catch (AssertActualExpectedException) {
-        await output.WriteLineAsync($"state version is {state.Version}, diagnostics: {state.GetDiagnostics().Values.Stringify()}");
+        await output.WriteLineAsync($"state version is {state.Version}, diagnostics: {state.GetAllDiagnostics().Stringify()}");
         var programString = new StringWriter();
         var printer = new Printer(programString, DafnyOptions.Default);
         printer.PrintProgram((Program)state.Program, true);

Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs

@@ -23,7 +23,7 @@ public Task DisposeAsync() {
     }
 
     private async Task SetUp(Action<DafnyOptions> modifyOptions) {
-      (client, Server) = await Initialize(options => { }, modifyOptions);
+      (client, Server) = await Initialize(_ => { }, modifyOptions);
     }
 
     [Fact]
@@ -34,9 +34,9 @@ function GetConstant(): int {
 }".Trim();
       var documentItem = CreateTestDocument(source, "CorrectDocumentCanBeParsedResolvedAndVerifiedWithoutErrors.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
-      Assert.NotNull(document);
-      Assert.True(document.GetDiagnostics().Values.All(x => !x.Any()));
+      var state = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
+      Assert.NotNull(state);
+      Assert.Empty(state.GetAllDiagnostics());
     }
 
     [Fact]
@@ -49,8 +49,8 @@ function GetConstant() int {
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
       var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
-      Assert.Single(document.GetDiagnostics());
-      var message = document.GetDiagnostics()[documentItem.Uri.ToUri()].ElementAt(0);
+      Assert.Single(document.GetDiagnosticUris());
+      var message = document.GetDiagnosticsForUri(documentItem.Uri.ToUri()).ElementAt(0);
       Assert.Equal(MessageSource.Parser.ToString(), message.Source);
     }
 
@@ -64,8 +64,8 @@ function GetConstant(): int {
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
       var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
-      Assert.Single(document.GetDiagnostics());
-      var message = document.GetDiagnostics()[documentItem.Uri.ToUri()].ElementAt(0);
+      Assert.Single(document.GetDiagnosticUris());
+      var message = document.GetDiagnosticsForUri(documentItem.Uri.ToUri()).ElementAt(0);
       Assert.Equal(MessageSource.Resolver.ToString(), message.Source);
     }
 
@@ -105,7 +105,7 @@ method Recurse(x: int) returns (r: int) {
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
       var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
-      Assert.True(document.GetDiagnostics()[documentItem.Uri.ToUri()].All(d => d.Severity != DiagnosticSeverity.Error));
+      Assert.True(document.GetDiagnosticsForUri(documentItem.Uri.ToUri()).All(d => d.Severity != DiagnosticSeverity.Error));
     }
 
     [Fact]
@@ -116,8 +116,7 @@ public async Task EmptyDocumentCanBeOpened() {
       var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
       // Empty files currently yield only a warning.
-      var diagnostics = document.GetDiagnostics();
-      Assert.True(diagnostics[documentItem.Uri.ToUri()].All(d => d.Severity != DiagnosticSeverity.Error));
+      Assert.True(document.GetDiagnosticsForUri(documentItem.Uri.ToUri()).All(d => d.Severity != DiagnosticSeverity.Error));
     }
 
     [Fact]
@@ -127,7 +126,7 @@ public async Task DocumentWithNoValidTokensCanBeOpened() {
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
       var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
-      Assert.True(document.GetDiagnostics()[documentItem.Uri.ToUri()].All(d => d.Severity != DiagnosticSeverity.Error));
+      Assert.True(document.GetDiagnosticsForUri(documentItem.Uri.ToUri()).All(d => d.Severity != DiagnosticSeverity.Error));
     }
 
     [Fact]
@@ -137,7 +136,7 @@ public async Task EmptyDocumentCanBeIncluded() {
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
       var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
-      Assert.False(document.GetDiagnostics().ContainsKey(documentItem.Uri.ToUri()));
+      Assert.DoesNotContain(documentItem.Uri.ToUri(), document.GetDiagnosticUris());
     }
 
     public OpenDocumentTest(ITestOutputHelper output) : base(output) {

Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs

@@ -343,6 +343,8 @@ await SetUp(options => {
     });
     var documentItem = CreateTestDocument(source, "WhenUsingOnSaveMethodStaysStaleUntilSave.dfy");
     await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+    var stale1 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
+    Assert.Equal(PublishedVerificationStatus.Stale, stale1.NamedVerifiables[0].Status);
 
     // Send a change to enable getting a new status notification.
     ApplyChange(ref documentItem, new Range(new Position(1, 0), new Position(1, 0)), "\n");

Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs

@@ -15,9 +15,7 @@ public async Task CancelUnstartedCompilationLeadsToCancelledTasks() {
     var dafnyOptions = DafnyOptions.Create(TextWriter.Null, TextReader.Null);
     var compilationManager = new CompilationManager(new Mock<ILogger<CompilationManager>>().Object,
       new Mock<ITextDocumentLoader>().Object,
-      new Mock<INotificationPublisher>().Object,
       new Mock<IProgramVerifier>().Object,
-      new Mock<ICompilationStatusNotificationPublisher>().Object,
       new Mock<IVerificationProgressReporter>().Object,
       dafnyOptions,
       null, new Compilation(0, new DafnyProject() { Uri = new Uri(Directory.GetCurrentDirectory()) }, new Uri[] { }), null);

Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs

@@ -23,27 +23,22 @@ public class TextDocumentLoaderTest {
     private Mock<ISymbolResolver> symbolResolver;
     private Mock<ISymbolTableFactory> symbolTableFactory;
     private Mock<IGhostStateDiagnosticCollector> ghostStateDiagnosticCollector;
-    private Mock<ICompilationStatusNotificationPublisher> notificationPublisher;
     private TextDocumentLoader textDocumentLoader;
     private Mock<ILogger<ITextDocumentLoader>> logger;
-    private Mock<INotificationPublisher> diagnosticPublisher;
 
     public TextDocumentLoaderTest(ITestOutputHelper output) {
       this.output = new WriterFromOutputHelper(output);
       parser = new();
       symbolResolver = new();
       symbolTableFactory = new();
       ghostStateDiagnosticCollector = new();
-      notificationPublisher = new();
       fileSystem = new();
       logger = new Mock<ILogger<ITextDocumentLoader>>();
-      diagnosticPublisher = new Mock<INotificationPublisher>();
       textDocumentLoader = TextDocumentLoader.Create(
         parser.Object,
         symbolResolver.Object,
         symbolTableFactory.Object,
         ghostStateDiagnosticCollector.Object,
-        notificationPublisher.Object,
         logger.Object
       );
     }

Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs

@@ -94,12 +94,12 @@ private void AssertMatchRegex(string expected, string value) {
     }
   }
 
-  public async Task<NamedVerifiableStatus> WaitForStatus(Range nameRange, PublishedVerificationStatus statusToFind,
+  public async Task<NamedVerifiableStatus> WaitForStatus([CanBeNull] Range nameRange, PublishedVerificationStatus statusToFind,
     CancellationToken cancellationToken, [CanBeNull] TextDocumentIdentifier documentIdentifier = null) {
     while (true) {
       try {
         var foundStatus = await verificationStatusReceiver.AwaitNextNotificationAsync(cancellationToken);
-        var namedVerifiableStatus = foundStatus.NamedVerifiables.FirstOrDefault(n => n.NameRange == nameRange);
+        var namedVerifiableStatus = foundStatus.NamedVerifiables.FirstOrDefault(n => nameRange == null || n.NameRange == nameRange);
         if (namedVerifiableStatus?.Status == statusToFind) {
           if (documentIdentifier != null) {
             Assert.Equal(documentIdentifier.Uri, foundStatus.Uri);
@@ -313,9 +313,8 @@ public async Task AssertNoDiagnosticsAreComing(CancellationToken cancellationTok
   }
 
   protected async Task AssertNoResolutionErrors(TextDocumentItem documentItem) {
-    var fullDiagnostics = (await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem))!.GetDiagnostics();
+    var resolutionDiagnostics = (await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem))!.GetDiagnosticsForUri(documentItem.Uri.ToUri()).ToList();
     // A document without diagnostics may be absent, even if resolved successfully
-    var resolutionDiagnostics = fullDiagnostics.GetValueOrDefault(documentItem.Uri.ToUri(), ImmutableList<Diagnostic>.Empty);
     var resolutionErrors = resolutionDiagnostics.Count(d => d.Severity == DiagnosticSeverity.Error);
     if (0 != resolutionErrors) {
       await Console.Out.WriteAsync(string.Join("\n", resolutionDiagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).Select(d => d.ToString())));

Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs

@@ -21,7 +21,7 @@ public class CompilationStatusNotificationTest : ClientBasedLanguageServerTest {
     [Fact]
     public async Task MultipleDocuments() {
       var source = @"
-method Foo() returns (x: int) ensures x / 2 == 1; {
+method Foo() returns (x: int) {
   return 2;
 }".TrimStart();
       var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
@@ -32,8 +32,7 @@ public async Task MultipleDocuments() {
       var documentItem1 = await CreateAndOpenTestDocument(source, Path.Combine(directory, "RunWithMultipleDocuments1.dfy"));
 
       var expectedStatuses = new[] {
-        CompilationStatus.Parsing, CompilationStatus.ResolutionStarted, CompilationStatus.CompilationSucceeded,
-        CompilationStatus.PreparingVerification
+        CompilationStatus.ResolutionStarted
       };
       var documents = new[] { documentItem1.Uri, DocumentUri.File(secondFilePath) };
       foreach (var expectedStatus in expectedStatuses) {
@@ -47,6 +46,9 @@ public async Task MultipleDocuments() {
           Assert.Equal(expectedStatus, status.Status);
         }
       }
+      foreach (var _ in documents) {
+        await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken);
+      }
     }
 
     [Fact(Timeout = MaxTestExecutionTimeMs)]
@@ -60,13 +62,11 @@ method Abs(x: int) returns (y: int)
 ".TrimStart();
       var documentItem = CreateTestDocument(source, "DocumentWithParserErrorsSendsParsingFailedStatus.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ParsingFailed);
 
       // We re-send the same erroneous document again to check that we don't have a CompilationSucceeded event queued.
       var otherDoc = CreateTestDocument(source, "Test2.dfy");
       client.OpenDocument(otherDoc);
-      await AssertProgress(otherDoc, CompilationStatus.Parsing);
       await AssertProgress(otherDoc, CompilationStatus.ParsingFailed);
     }
 
@@ -81,14 +81,12 @@ method Abs(x: int) returns (y: int)
 ".TrimStart();
       var documentItem = CreateTestDocument(source, "DocumentWithResolverErrorsSendsResolutionFailedStatus.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ResolutionStarted);
       await AssertProgress(documentItem, CompilationStatus.ResolutionFailed);
 
       // We re-send the same erroneous document again to check that we don't have a CompilationSucceeded event queued.
       var otherDoc = CreateTestDocument(source, "Test2.dfy");
       client.OpenDocument(otherDoc);
-      await AssertProgress(otherDoc, CompilationStatus.Parsing);
       await AssertProgress(otherDoc, CompilationStatus.ResolutionStarted);
       await AssertProgress(otherDoc, CompilationStatus.ResolutionFailed);
     }
@@ -107,9 +105,8 @@ method Abs(x: int) returns (y: int)
 ".TrimStart();
       var documentItem = CreateTestDocument(source, "DocumentWithoutErrorsSendsCompilationSucceededVerificationStartedAndVerificationSucceededStatuses.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ResolutionStarted);
-      await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded);
+      await WaitForStatus(null, PublishedVerificationStatus.Correct, CancellationToken, documentItem);
     }
     private async Task AssertProgress(TextDocumentItem documentItem, CompilationStatus expectedStatus, [CanBeNull] string expectedMessage = null) {
       var lastResult = await compilationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
@@ -132,28 +129,25 @@ method Abs(x: int) returns (y: int)
 ".TrimStart();
       var documentItem = CreateTestDocument(source, "DocumentWithOnlyVerifierErrorsSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ResolutionStarted);
-      await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded);
+      await WaitForStatus(null, PublishedVerificationStatus.Error, CancellationToken, documentItem);
     }
 
     [Fact(Timeout = MaxTestExecutionTimeMs)]
     public async Task DocumentWithOnlyCodedVerifierTimeoutSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses() {
       var documentItem = CreateTestDocument(SlowToVerify, "DocumentWithOnlyCodedVerifierTimeoutSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ResolutionStarted);
-      await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded);
+      await WaitForStatus(null, PublishedVerificationStatus.Error, CancellationToken, documentItem);
     }
 
     [Fact(Timeout = MaxTestExecutionTimeMs)]
     public async Task DocumentWithOnlyConfiguredVerifierTimeoutSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses() {
       await SetUp(options => options.Set(BoogieOptionBag.VerificationTimeLimit, 3U));
       var documentItem = CreateTestDocument(SlowToVerify, "DocumentWithOnlyConfiguredVerifierTimeoutSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ResolutionStarted);
-      await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded);
+      await WaitForStatus(null, PublishedVerificationStatus.Error, CancellationToken, documentItem);
     }
 
     [Fact(Timeout = MaxTestExecutionTimeMs)]
@@ -171,14 +165,12 @@ method Abs(x: int) returns (y: int)
       // compilation status twice without any verification status inbetween.
       var documentItem1 = CreateTestDocument(source, "test_1.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem1, CancellationToken);
-      await AssertProgress(documentItem1, CompilationStatus.Parsing);
       await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted);
-      await AssertProgress(documentItem1, CompilationStatus.CompilationSucceeded);
+      await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem1);
       var documentItem2 = CreateTestDocument(source, "test_2dfy");
       await client.OpenDocumentAndWaitAsync(documentItem2, CancellationToken);
-      await AssertProgress(documentItem2, CompilationStatus.Parsing);
       await AssertProgress(documentItem2, CompilationStatus.ResolutionStarted);
-      await AssertProgress(documentItem2, CompilationStatus.CompilationSucceeded);
+      await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem2);
     }
 
     [Fact(Timeout = MaxTestExecutionTimeMs)]
@@ -197,15 +189,13 @@ method Abs(x: int) returns (y: int)
       var documentItem1 = CreateTestDocument(source, "test_1.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem1, CancellationToken);
       await client.SaveDocumentAndWaitAsync(documentItem1, CancellationToken);
-      await AssertProgress(documentItem1, CompilationStatus.Parsing);
       await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted);
-      await AssertProgress(documentItem1, CompilationStatus.CompilationSucceeded);
+      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.Parsing);
       await AssertProgress(documentItem2, CompilationStatus.ResolutionStarted);
-      await AssertProgress(documentItem2, CompilationStatus.CompilationSucceeded);
+      await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem2);
     }
 
     [Fact(Timeout = MaxTestExecutionTimeMs)]
@@ -219,7 +209,6 @@ lemma Something(i: int)
     }";
       var documentItem = CreateTestDocument(source, "MultisetShouldNotCrashParser.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ParsingFailed);
     }