Fixes gutter when cache is enabled (#2312)

Fixes dafny-lang/ide-vscode#187

The issue was that caching would prevent reports of implementations being finished to verify for the gutter reporting mechanism. I added it, and a test that I verified would not work in the absence of the fix.

Changes
* It also report all the results that were cached as if they were resolved immediately.

RELEASE_NOTES.md

@@ -2,6 +2,7 @@
 
 - fix: Fix bug in translation of two-state predicates with heap labels. (https://github.com/dafny-lang/dafny/pull/2300)
 - fix: Check that arguments of 'unchanged' satisfy enclosing reads clause. (https://github.com/dafny-lang/dafny/pull/2302)
+- fix: Caching in the language server does not prevent gutter icons from being updated correctly. (https://github.com/dafny-lang/dafny/pull/2312)
 - fix: Correctly infer type of numeric arguments, where the type is a subset type of a newtype. (https://github.com/dafny-lang/dafny/pull/2314)
 
 # 3.7.1

Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs

@@ -0,0 +1,51 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text.RegularExpressions;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.Dafny.LanguageServer.Language;
+using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics;
+
+[TestClass]
+public class CachedLinearVerificationGutterStatusTester : LinearVerificationGutterStatusTester {
+ private const int MaxTestExecutionTimeMs = 10000;
+
+
+
+ // To add a new test, just call VerifyTrace on a given program,
+ // the test will fail and give the correct output that can be use for the test
+ // Add '//Next<n>:' to edit a line multiple times
+
+ [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+ public async Task EnsureCachingDoesNotMakeSquigglyLinesToRemain() {
+ await SetUp(new Dictionary<string, string>() {
+ { $"{VerifierOptions.Section}:{nameof(VerifierOptions.VerifySnapshots)}", "1" }
+ });
+ await VerifyTrace(@"
+ . S S | I $ | :method test() {
+ . S | | I $ | : assert true;
+ . S S | I $ | : //Next: 
+ . S S | I $ | :}");
+ }
+
+ [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+ public async Task EnsureCachingDoesNotHideErrors() {
+ await SetUp(new Dictionary<string, string>() {
+ { $"{VerifierOptions.Section}:{nameof(VerifierOptions.VerifySnapshots)}", "1" }
+ });
+ await VerifyTrace(@"
+ . S [S][ ][I][S][S][ ]:method test() {
+ . S [O][O][o][Q][O][O]: assert true;
+ . S [=][=][-][~][=][=]: assert false;
+ . S [S][ ][I][S][S][ ]: //Next: 
+ . S [S][ ][I][S][S][ ]:}");
+ }
+}

Source/DafnyLanguageServer/Language/AssertionBatchCompletedObserver.cs

@@ -55,7 +55,7 @@ public void ReportEndVerifyImplementation(Implementation implementation, Boogie.
 
  public void ReportSplitResult(Split split, VCResult vcResult) {
  if (reportVerificationDiagnostics) {
- completedBatches.OnNext(new AssertionBatchResult(split, vcResult));
+ completedBatches.OnNext(new AssertionBatchResult(split.Implementation, vcResult));
  }
  }
 

Source/DafnyLanguageServer/Language/IProgramVerifier.cs

@@ -7,7 +7,7 @@
 using VC;
 
 namespace Microsoft.Dafny.LanguageServer.Language {
- public record AssertionBatchResult(Split Split, VCResult Result);
+ public record AssertionBatchResult(Implementation Implementation, VCResult Result);
 
  public record ProgramVerificationTasks(IReadOnlyList<IImplementationTask> Tasks);
 

Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs

@@ -134,7 +134,7 @@ public async Task<DafnyDocument> PrepareVerificationTasksAsync(DafnyDocument loa
  }
  var implementations = verificationTasks.Select(t => t.Implementation).ToHashSet();
  var subscription = verifier.BatchCompletions.Where(c =>
- implementations.Contains(c.Split.Implementation)).Subscribe(progressReporter.ReportAssertionBatchResult);
+ implementations.Contains(c.Implementation)).Subscribe(progressReporter.ReportAssertionBatchResult);
  cancellationToken.Register(() => subscription.Dispose());
  result.GutterProgressReporter = progressReporter;
  return result;
@@ -245,6 +245,12 @@ public IObservable<DafnyDocument> Verify(DafnyDocument dafnyDocument, IImplement
 
  var statusUpdates = implementationTask.TryRun();
  if (statusUpdates == null) {
+ if (VerifierOptions.GutterStatus && implementationTask.CacheStatus is Completed completedCache) {
+ foreach (var result in completedCache.Result.VCResults) {
+ dafnyDocument.GutterProgressReporter!.ReportAssertionBatchResult(new AssertionBatchResult(implementationTask.Implementation, result));
+ }
+ dafnyDocument.GutterProgressReporter!.ReportEndVerifyImplementation(implementationTask.Implementation, completedCache.Result);
+ }
  return Observable.Empty<DafnyDocument>();
  }
 

Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs

@@ -358,9 +358,8 @@ public void ReportAssertionBatchResult(AssertionBatchResult batchResult) {
  return;
  }
  lock (LockProcessing) {
- var split = batchResult.Split;
+ var implementation = batchResult.Implementation;
  var result = batchResult.Result;
- var implementation = split.Implementation;
  // While there is no error, just add successful nodes.
  var targetMethodNode = GetTargetMethodTree(implementation, out var implementationNode);
  if (targetMethodNode == null) {