fix: "Stuck on Verifying..."

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)
 
 

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

@@ -98,12 +98,8 @@ private bool VerifyWithBoogie(Boogie.Program program, CancellationToken cancella
       ExecutionEngine.CollectModSets(program);
       ExecutionEngine.CoalesceBlocks(program);
       ExecutionEngine.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))) {
+      using (cancellationToken.Register(() => CancelVerification(requestId))) {
         try {
           var statistics = new PipelineStatistics();
           var outcome = ExecutionEngine.InferAndVerify(program, statistics, programId, null, uniqueRequestId);

Source/Directory.Build.props

@@ -7,7 +7,7 @@
 
   <!-- Boogie dependency -->
   <ItemGroup>
-    <PackageReference Include="Boogie.ExecutionEngine" Version="2.11.4" />
+    <PackageReference Include="Boogie.ExecutionEngine" Version="2.11.5" />
   </ItemGroup>
 
 </Project>

customBoogie.patch

@@ -138,7 +138,7 @@ index 30e67936..64a5a976 100644
 
    <!-- Boogie dependency -->
    <ItemGroup>
--    <PackageReference Include="Boogie.ExecutionEngine" Version="2.11.4" />
+-    <PackageReference Include="Boogie.ExecutionEngine" Version="2.11.5" />
 +    <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
    </ItemGroup>