Publish empty verification list (dafny-lang#2552)

Fixes "Verification completed" not showing for Dafny files that don't have any verifiable tasks.
robin-aws · Aug 5, 2022 · 228193c · 228193c
1 parent 052b9e2
commit 228193c
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 10 deletions.
diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs
@@ -13,6 +13,20 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization;
 [TestClass]
 public class VerificationStatusTest : ClientBasedLanguageServerTest {
 
+  [TestMethod]
+  public async Task EmptyVerificationTaskListIsPublishedOnOpenAndChange() {
+    var source = "method m1() {}";
+    var documentItem = CreateTestDocument(source);
+    await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+
+    var status1 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
+    Assert.AreEqual(0, status1.NamedVerifiables.Count);
+
+    ApplyChange(ref documentItem, new Range(0, 0, 0, 0), "\n");
+
+    var status2 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
+    Assert.AreEqual(0, status2.NamedVerifiables.Count);
+  }
 
   [TestMethod]
   public async Task NoVerificationStatusPublishedForUnparsedDocument() {
@@ -100,12 +114,9 @@ await SetUp(new Dictionary<string, string> {
     var translatedStatusBefore = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
     Assert.AreEqual(1, translatedStatusBefore.NamedVerifiables.Count);
 
-    // Delete the end of the Foo range
+    // Delete the end of the Foo range, so Foo() becomes F()
     ApplyChange(ref documentItem, new Range(0, 8, 0, 12), "()");
 
-    var resolutionStatusAfter = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
-    Assert.AreEqual(0, resolutionStatusAfter.NamedVerifiables.Count);
-
     var translatedStatusAfter = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
     Assert.AreEqual(1, translatedStatusAfter.NamedVerifiables.Count);
   }
@@ -249,6 +260,7 @@ await SetUp(new Dictionary<string, string>() {
 
     await client.SaveDocumentAndWaitAsync(documentItem, CancellationToken);
 
+    var stale2 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
     var running = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken);
     Assert.AreEqual(PublishedVerificationStatus.Running, running.NamedVerifiables[0].Status);
 

diff --git a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs
@@ -28,23 +28,27 @@ public void PublishNotifications(DafnyDocument previous, DafnyDocument document)
     }
 
     private void PublishVerificationStatus(DafnyDocument previousDocument, DafnyDocument document) {
-      if (!document.WasResolved) {
+      var notification = GetFileVerificationStatus(document);
+      if (notification == null) {
+        // Do not publish verification status while resolving
         return;
       }
 
-      var notification = GetFileVerificationStatus(document);
       var previous = GetFileVerificationStatus(previousDocument);
-      if (previous.Version > notification.Version ||
-          previous.NamedVerifiables.SequenceEqual(notification.NamedVerifiables)) {
+      if (previous != null && (previous.Version > notification.Version ||
+          previous.NamedVerifiables.SequenceEqual(notification.NamedVerifiables))) {
         return;
       }
 
       languageServer.TextDocument.SendNotification(DafnyRequestNames.VerificationSymbolStatus, notification);
     }
 
-    private static FileVerificationStatus GetFileVerificationStatus(DafnyDocument document) {
+    private static FileVerificationStatus? GetFileVerificationStatus(DafnyDocument document) {
+      if (document.ImplementationIdToView == null || document.VerificationTasks == null) {
+        return null;
+      }
       return new FileVerificationStatus(document.Uri, document.Version,
-        GetNamedVerifiableStatuses(document.ImplementationIdToView ?? (IReadOnlyDictionary<ImplementationId, ImplementationView>)new Dictionary<ImplementationId, ImplementationView>()));
+        GetNamedVerifiableStatuses(document.ImplementationIdToView));
     }
 
     private static List<NamedVerifiableStatus> GetNamedVerifiableStatuses(IReadOnlyDictionary<ImplementationId, ImplementationView> implementationViews) {