fix: "Stuck on Verifying..." (#1771)

RELEASE_NOTES.md

@@ -3,6 +3,7 @@
 - feat: `continue` statements. Like Dafny's `break` statements, these come in two forms: one that uses a label to name the continue target and one that specifies the continue target by nesting level. See section [19.2](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-break-continue) of the Reference Manual. (https://github.com/dafny-lang/dafny/pull/1839)
 - feat: The keyword syntax for functions will change in Dafny version 4. The new command-line option `/functionSyntax` (see `/help`) allows early adoption of the new syntax. (https://github.com/dafny-lang/dafny/pull/1832)
 - fix: No warning "File contains no code" if a file only contains a submodule (https://github.com/dafny-lang/dafny/pull/1840)
+- fix: Stuck in verifying in VSCode - support for verification cancellation (https://github.com/dafny-lang/dafny/pull/1771)
 - fix: export-reveals of function-by-method now allows the function body to be ghost (https://github.com/dafny-lang/dafny/pull/1855)
 - fix: Regain C# 7.3 compatibility of the compiled code. (https://github.com/dafny-lang/dafny/pull/1877)
 - fix: The error "assertion violation" is replaced by the better wording "assertion might not hold". This indicates better that the verifier is unable to prove the assertion. (https://github.com/dafny-lang/dafny/pull/1862)

Source/DafnyLanguageServer.Test/Various/CancelVerification.cs

@@ -0,0 +1,72 @@
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+using OmniSharp.Extensions.LanguageServer.Protocol.Client;
+using System.IO;
+using System.Threading;
+using System.Threading.Tasks;
+using OmniSharp.Extensions.LanguageServer.Protocol.Document;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various {
+  [TestClass]
+  public class CancelVerificationTest : DafnyLanguageServerTestBase {
+    private ILanguageClient client;
+
+    [TestInitialize]
+    public async Task SetUp() {
+      client = await InitializeClient();
+    }
+
+    // https://github.com/dafny-lang/language-server-csharp/issues/40
+    [TestMethod]
+    public async Task CancelingVerificationStopsTheProver() {
+      var source = @"
+function method {:unroll 100} Ack(m: nat, n: nat): nat
+  decreases m, n
+{
+  if m == 0 then
+    n + 1
+  else if n == 0 then
+    Ack(m - 1, 1)
+  else
+    Ack(m - 1, Ack(m, n - 1))
+}
+
+method test() {
+  assert Ack(5, 5) == 0;
+}".TrimStart();
+      var documentItem = CreateTestDocument(source);
+      client.OpenDocument(documentItem);
+      await Task.Delay(5_000);
+      // This cancels the previous request.
+      client.DidChangeTextDocument(new DidChangeTextDocumentParams {
+        TextDocument = new OptionalVersionedTextDocumentIdentifier {
+          Uri = documentItem.Uri,
+          Version = documentItem.Version + 1
+        },
+        ContentChanges = new[] {new TextDocumentContentChangeEvent {
+          Range = new Range((12, 9), (12, 23)),
+          Text = "true"
+        }}
+      });
+      await client.WaitForNotificationCompletionAsync(documentItem.Uri, CancellationToken);
+      var document = await Documents.GetDocumentAsync(documentItem.Uri);
+      Assert.IsNotNull(document);
+      Assert.IsTrue(!document.Errors.HasErrors);
+      client.DidChangeTextDocument(new DidChangeTextDocumentParams {
+        TextDocument = new OptionalVersionedTextDocumentIdentifier {
+          Uri = documentItem.Uri,
+          Version = documentItem.Version + 2
+        },
+        ContentChanges = new[] {new TextDocumentContentChangeEvent {
+          Range = new Range((12, 9), (12, 13)),
+          Text = "/" // A parse error
+        }}
+      });
+      await client.WaitForNotificationCompletionAsync(documentItem.Uri, CancellationToken);
+      document = await Documents.GetDocumentAsync(documentItem.Uri);
+      Assert.IsNotNull(document);
+      Assert.IsTrue(document.Errors.HasErrors);
+    }
+  }
+}

Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs

@@ -103,10 +103,6 @@ private bool VerifyWithBoogie(ExecutionEngine engine, Boogie.Program program, Ca
       engine.CoalesceBlocks(program);
       engine.Inline(program);
 
-      // TODO The requestId is used to cancel a verification.
-      //      However, the cancelling a verification is currently not possible since it blocks a text document
-      //      synchronization event which are serialized. Thus, no event is processed until the pending
-      //      synchronization is completed.
       var uniqueRequestId = Guid.NewGuid().ToString();
       using (cancellationToken.Register(() => CancelVerification(uniqueRequestId))) {
         try {