diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index f87900213f4..ce5475d8c59 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,6 +1,7 @@ # Upcoming -- feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of waiting for all methods to be verified. (https://github.com/dafny-lang/dafny/pull/1944) +- feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of after all methods are verified. +- fix: No more display of previous obsolete verification diagnostics if newer are available. (https://github.com/dafny-lang/dafny/pull/2142) - feat: Live verification diagnostics for the language server (https://github.com/dafny-lang/dafny/pull/1942) - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080) diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs new file mode 100644 index 00000000000..9febb0fef52 --- /dev/null +++ b/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs @@ -0,0 +1,65 @@ +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.Workspace.Notifications; +using Microsoft.VisualStudio.TestTools.UnitTesting; +using OmniSharp.Extensions.JsonRpc; +using OmniSharp.Extensions.LanguageServer.Protocol.Document; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; +using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; + +namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; + +[TestClass] +public class ConcurrentLinearVerificationGutterStatusTester : LinearVerificationGutterStatusTester { + private const int MaxSimultaneousVerificationTasks = 3; + + protected TestNotificationReceiver[] verificationStatusGutterReceivers = + new TestNotificationReceiver[MaxSimultaneousVerificationTasks]; + + private void NotifyAllVerificationGutterStatusReceivers(VerificationStatusGutter request) { + foreach (var receiver in verificationStatusGutterReceivers) { + receiver.NotificationReceived(request); + } + } + + [TestInitialize] + public override async Task SetUp() { + for (var i = 0; i < verificationStatusGutterReceivers.Length; i++) { + verificationStatusGutterReceivers[i] = new(); + } + verificationStatusGutterReceiver = new(); + client = await InitializeClient(options => + options + .AddHandler(DafnyRequestNames.VerificationStatusGutter, + NotificationHandler.For(NotifyAllVerificationGutterStatusReceivers)) + ); + } + + [TestMethod] + public async Task EnsuresManyDocumentsCanBeVerifiedAtOnce() { + var result = new List(); + for (var i = 0; i < MaxSimultaneousVerificationTasks; i++) { + result.Add(VerifyTrace(@" + . | | | I | | :predicate F(i: int) { + . | | | I | | : false // Should not be highlighted in gutter. + . | | | I | | :} + | | | I | | : + . S [S][ ][I][S][ ]:method H() + . S [=][=][-][~][O]: ensures F(1) + . S [=][=][-][~][=]:{//Next: { assert false; + . S [S][ ][I][S][ ]:}", $"testfile{i}.dfy", true, verificationStatusGutterReceivers[i])); + } + + for (var i = 0; i < MaxSimultaneousVerificationTasks; i++) { + await result[i]; + } + + //await Task.WhenAll(result.ToArray()); + } + +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/LinearRenderingTest.cs b/Source/DafnyLanguageServer.Test/GutterStatus/LinearRenderingTest.cs similarity index 100% rename from Source/DafnyLanguageServer.Test/Diagnostics/LinearRenderingTest.cs rename to Source/DafnyLanguageServer.Test/GutterStatus/LinearRenderingTest.cs diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/LinearVerificationDiagnosticTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs similarity index 83% rename from Source/DafnyLanguageServer.Test/Diagnostics/LinearVerificationDiagnosticTester.cs rename to Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs index 8e840e75e0e..97d0e0b3096 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/LinearVerificationDiagnosticTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs @@ -16,17 +16,15 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; -public abstract class LinearVerificationDiagnosticTester : ClientBasedLanguageServerTest { - protected TestNotificationReceiver VerificationDiagnosticReceiver; +public abstract class LinearVerificationGutterStatusTester : ClientBasedLanguageServerTest { + protected TestNotificationReceiver verificationStatusGutterReceiver; [TestInitialize] public override async Task SetUp() { - diagnosticReceiver = new(); - VerificationDiagnosticReceiver = new(); + verificationStatusGutterReceiver = new(); client = await InitializeClient(options => options - .OnPublishDiagnostics(diagnosticReceiver.NotificationReceived) .AddHandler(DafnyRequestNames.VerificationStatusGutter, - NotificationHandler.For(VerificationDiagnosticReceiver.NotificationReceived)) + NotificationHandler.For(verificationStatusGutterReceiver.NotificationReceived)) ); } @@ -108,27 +106,29 @@ public static string ExtractCode(string tracesAndCode) { protected List previousTraces = null; - protected async Task> GetAllLineVerificationDiagnostics(TextDocumentItem documentItem) { + protected async Task> GetAllLineVerificationStatuses( + TextDocumentItem documentItem, + TestNotificationReceiver verificationStatusGutterReceiver + ) { var traces = new List(); var maximumNumberOfTraces = 50; var previousPerLineDiagnostics = previousTraces == null || previousTraces.Count == 0 ? null : previousTraces[^1].ToList(); - var nextDiagnostic = await diagnosticReceiver.AwaitNextNotificationAsync(CancellationToken); for (; maximumNumberOfTraces > 0; maximumNumberOfTraces--) { - var verificationDiagnosticReport = await VerificationDiagnosticReceiver.AwaitNextNotificationAsync(CancellationToken); - if (documentItem.Uri != verificationDiagnosticReport.Uri || documentItem.Version != verificationDiagnosticReport.Version) { + var verificationStatusGutter = await verificationStatusGutterReceiver.AwaitNextNotificationAsync(CancellationToken); + if (documentItem.Uri != verificationStatusGutter.Uri || documentItem.Version != verificationStatusGutter.Version) { continue; } - var newPerLineDiagnostics = verificationDiagnosticReport.PerLineStatus.ToList(); + var newPerLineDiagnostics = verificationStatusGutter.PerLineStatus.ToList(); if ((previousPerLineDiagnostics != null && previousPerLineDiagnostics.SequenceEqual(newPerLineDiagnostics)) || newPerLineDiagnostics.All(status => status == LineVerificationStatus.Nothing)) { continue; } - traces.Add(verificationDiagnosticReport.PerLineStatus); - if (NoMoreNotificationsToAwaitFrom(verificationDiagnosticReport)) { + traces.Add(verificationStatusGutter.PerLineStatus); + if (NoMoreNotificationsToAwaitFrom(verificationStatusGutter)) { break; } @@ -139,10 +139,10 @@ var previousPerLineDiagnostics return traces; } - private static bool NoMoreNotificationsToAwaitFrom(VerificationStatusGutter verificationDiagnosticReport) { - return verificationDiagnosticReport.PerLineStatus.Contains(LineVerificationStatus.ResolutionError) || - verificationDiagnosticReport.PerLineStatus.All(IsNotIndicatingProgress) || - verificationDiagnosticReport.PerLineStatus.All(status => status == LineVerificationStatus.Nothing); + private static bool NoMoreNotificationsToAwaitFrom(VerificationStatusGutter verificationGutterStatus) { + return verificationGutterStatus.PerLineStatus.Contains(LineVerificationStatus.ResolutionError) || + verificationGutterStatus.PerLineStatus.All(IsNotIndicatingProgress) || + verificationGutterStatus.PerLineStatus.All(status => status == LineVerificationStatus.Nothing); } /// @@ -218,19 +218,24 @@ Position IndexToPosition(int index) { } // If testTrace is false, codeAndTree should not contain a trace to test. - public async Task VerifyTrace(string codeAndTrace, bool testTrace = true) { + public async Task VerifyTrace(string codeAndTrace, string fileName = null, bool testTrace = true, + TestNotificationReceiver verificationStatusGutterReceiver = null + ) { + if (verificationStatusGutterReceiver == null) { + verificationStatusGutterReceiver = this.verificationStatusGutterReceiver; + } codeAndTrace = codeAndTrace[0] == '\n' ? codeAndTrace.Substring(1) : codeAndTrace.Substring(0, 2) == "\r\n" ? codeAndTrace.Substring(2) : codeAndTrace; var codeAndChanges = testTrace ? ExtractCode(codeAndTrace) : codeAndTrace; var (code, changes) = ExtractCodeAndChanges(codeAndChanges); - var documentItem = CreateTestDocument(code); - await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var documentItem = CreateTestDocument(code, fileName); + client.OpenDocument(documentItem); var traces = new List(); - traces.AddRange(await GetAllLineVerificationDiagnostics(documentItem)); + traces.AddRange(await GetAllLineVerificationStatuses(documentItem, verificationStatusGutterReceiver)); foreach (var (range, inserted) in changes) { ApplyChange(ref documentItem, range, inserted); - traces.AddRange(await GetAllLineVerificationDiagnostics(documentItem)); + traces.AddRange(await GetAllLineVerificationStatuses(documentItem, verificationStatusGutterReceiver)); } if (testTrace) { diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/ListeningTextDocumentLoader.cs b/Source/DafnyLanguageServer.Test/GutterStatus/ListeningTextDocumentLoader.cs similarity index 100% rename from Source/DafnyLanguageServer.Test/Diagnostics/ListeningTextDocumentLoader.cs rename to Source/DafnyLanguageServer.Test/GutterStatus/ListeningTextDocumentLoader.cs diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/ReorderingVerificationDiagnosticTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs similarity index 93% rename from Source/DafnyLanguageServer.Test/Diagnostics/ReorderingVerificationDiagnosticTester.cs rename to Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs index 10ed32b568e..301b0afe07e 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/ReorderingVerificationDiagnosticTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs @@ -21,20 +21,18 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; /// methods priorities for verification being set automatically. /// [TestClass] -public class ReorderingVerificationDiagnosticTester : LinearVerificationDiagnosticTester { +public class ReorderingVerificationGutterStatusTester : LinearVerificationGutterStatusTester { private ListeningTextDocumentLoader textDocumentLoader; private const int MaxTestExecutionTimeMs = 10000; [TestInitialize] public override async Task SetUp() { DafnyOptions.Install(DafnyOptions.Create("-proverOpt:SOLVER=noop")); - diagnosticReceiver = new(); - VerificationDiagnosticReceiver = new(); + verificationStatusGutterReceiver = new(); client = await InitializeClient(options => options - .OnPublishDiagnostics(diagnosticReceiver.NotificationReceived) .AddHandler(DafnyRequestNames.VerificationStatusGutter, - NotificationHandler.For(VerificationDiagnosticReceiver.NotificationReceived)) + NotificationHandler.For(verificationStatusGutterReceiver.NotificationReceived)) , serverOptions => { serverOptions.Services.AddSingleton(serviceProvider => { textDocumentLoader = new ListeningTextDocumentLoader( diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/SimpleLinearVerificationDiagnosticTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs similarity index 95% rename from Source/DafnyLanguageServer.Test/Diagnostics/SimpleLinearVerificationDiagnosticTester.cs rename to Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs index 663b821cdbc..a94f9b7f6f6 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/SimpleLinearVerificationDiagnosticTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs @@ -13,7 +13,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; [TestClass] -public class SimpleLinearVerificationDiagnosticTester : LinearVerificationDiagnosticTester { +public class SimpleLinearVerificationGutterStatusTester : LinearVerificationGutterStatusTester { private const int MaxTestExecutionTimeMs = 10000; // To add a new test, just call VerifyTrace on a given program, @@ -21,7 +21,7 @@ public class SimpleLinearVerificationDiagnosticTester : LinearVerificationDiagno // Add '//Next:' to edit a line multiple times [TestMethod, Timeout(MaxTestExecutionTimeMs)] - public async Task EnsureVerificationDiagnosticsAreWorking() { + public async Task EnsureVerificationGutterStatusIsWorking() { await VerifyTrace(@" . | | | I I | | :predicate Ok() { . | | | I I | | : true diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs index ba4056d1a3e..9e592fd4c7a 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs @@ -69,7 +69,7 @@ decreases y }".TrimStart(); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var diagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, diagnostics.Length); Assert.AreEqual("Parser", diagnostics[0].Source); Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity); @@ -93,7 +93,7 @@ decreases y }".TrimStart(); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var diagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, diagnostics.Length); Assert.AreEqual("Resolver", diagnostics[0].Source); Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity); @@ -117,7 +117,7 @@ decreases y }".TrimStart(); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var diagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(2, diagnostics.Length); Assert.AreEqual("Resolver", diagnostics[0].Source); Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity); @@ -170,7 +170,7 @@ await SetUp(new Dictionary() { }); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var diagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(0, diagnostics.Length); await AssertNoDiagnosticsAreComing(); } @@ -237,7 +237,7 @@ decreases y } }); - var diagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, diagnostics.Length); Assert.AreEqual("Parser", diagnostics[0].Source); Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity); @@ -264,7 +264,7 @@ await SetUp(new Dictionary() { }); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var diagnosticsAfterOpening = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnosticsAfterOpening = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(0, diagnosticsAfterOpening.Length); client.DidChangeTextDocument(new DidChangeTextDocumentParams { @@ -280,7 +280,7 @@ await SetUp(new Dictionary() { } }); - var diagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, diagnostics.Length); Assert.AreEqual("Parser", diagnostics[0].Source); Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity); @@ -347,7 +347,7 @@ await SetUp(new Dictionary() { }); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var diagnosticsAfterOpening = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnosticsAfterOpening = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(0, diagnosticsAfterOpening.Length); client.DidChangeTextDocument(new DidChangeTextDocumentParams { @@ -363,7 +363,7 @@ await SetUp(new Dictionary() { } }); - var diagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(0, diagnostics.Length); await AssertNoDiagnosticsAreComing(); } @@ -434,9 +434,9 @@ decreases y }".TrimStart(); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); client.DidCloseTextDocument(new DidCloseTextDocumentParams { TextDocument = documentItem }); - var diagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(0, diagnostics.Length); await AssertNoDiagnosticsAreComing(); } @@ -446,7 +446,7 @@ public async Task OpeningDocumentThatIncludesNonExistentDocumentReportsParserErr var source = "include \"doesNotExist.dfy\""; var documentItem = CreateTestDocument(source, Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles/test.dfy")); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var diagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, diagnostics.Length); Assert.AreEqual("Parser", diagnostics[0].Source); Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity); @@ -459,7 +459,7 @@ public async Task OpeningDocumentThatIncludesDocumentWithSyntaxErrorsReportsPars var source = "include \"syntaxError.dfy\""; var documentItem = CreateTestDocument(source, Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles/test.dfy")); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var diagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, diagnostics.Length); Assert.AreEqual("Parser", diagnostics[0].Source); Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity); @@ -472,7 +472,7 @@ public async Task OpeningDocumentThatIncludesDocumentWithSemanticErrorsReportsRe var source = "include \"syntaxError.dfy\""; var documentItem = CreateTestDocument(source, Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles/test.dfy")); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var diagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, diagnostics.Length); Assert.AreEqual("Parser", diagnostics[0].Source); Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity); @@ -485,7 +485,7 @@ public async Task OpeningDocumentWithSemanticErrorsInIncludeReportsResolverError var source = "include \"semanticError.dfy\""; var documentItem = CreateTestDocument(source, Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles/test.dfy")); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var diagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, diagnostics.Length); Assert.AreEqual("Resolver", diagnostics[0].Source); Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity); @@ -539,10 +539,10 @@ await SetUp(new Dictionary() { }); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var changeDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var changeDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(0, changeDiagnostics.Length); client.SaveDocument(documentItem); - var saveDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var saveDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, saveDiagnostics.Length); Assert.AreEqual(MessageSource.Verifier.ToString(), saveDiagnostics[0].Source); Assert.AreEqual(DiagnosticSeverity.Error, saveDiagnostics[0].Severity); @@ -718,10 +718,10 @@ method test() { ".TrimStart(); var documentItem = CreateTestDocument(source); client.OpenDocument(documentItem); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); Assert.AreEqual(0, resolutionDiagnostics.Length); - var firstVerificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); - var secondVerificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); + var firstVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); + var secondVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); Assert.AreEqual(1, firstVerificationDiagnostics.Length); // Second diagnostic is a timeout exception from SlowToVerify @@ -742,10 +742,10 @@ await SetUp(new Dictionary() { }); var documentItem = CreateTestDocument(source); client.OpenDocument(documentItem); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); Assert.AreEqual(0, resolutionDiagnostics.Length); - var firstVerificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); - var secondVerificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); + var firstVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); + var secondVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); Assert.AreEqual(1, firstVerificationDiagnostics.Length); Assert.AreEqual(2, secondVerificationDiagnostics.Length); @@ -766,9 +766,9 @@ await SetUp(new Dictionary() { }); var documentItem = CreateTestDocument(source); client.OpenDocument(documentItem); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); Assert.AreEqual(0, resolutionDiagnostics.Length); - var firstVerificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); + var firstVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken.None, documentItem); Assert.AreEqual(2, firstVerificationDiagnostics.Length); await AssertNoDiagnosticsAreComing(); @@ -789,29 +789,29 @@ await SetUp(new Dictionary() { }); var documentItem = CreateTestDocument(source); client.OpenDocument(documentItem); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); Assert.AreEqual(0, resolutionDiagnostics.Length); - var firstVerificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); - var secondVerificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var firstVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var secondVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); Assert.AreEqual(1, firstVerificationDiagnostics.Length); Assert.AreEqual(2, secondVerificationDiagnostics.Length); ApplyChange(ref documentItem, new Range((1, 9), (1, 14)), "true"); ; - var resolutionDiagnostics2 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var resolutionDiagnostics2 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); AssertDiagnosticListsAreEqualBesidesMigration(secondVerificationDiagnostics, resolutionDiagnostics2); - var firstVerificationDiagnostics2 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); - var secondVerificationDiagnostics2 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var firstVerificationDiagnostics2 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var secondVerificationDiagnostics2 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); //Reordering means the assert false could be solved first //Assert.AreEqual(1, firstVerificationDiagnostics2.Length); // Still contains second failing method Assert.AreEqual(1, secondVerificationDiagnostics2.Length); ApplyChange(ref documentItem, new Range((4, 9), (4, 14)), "true"); - var resolutionDiagnostics3 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var resolutionDiagnostics3 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); AssertDiagnosticListsAreEqualBesidesMigration(secondVerificationDiagnostics2, resolutionDiagnostics3); - var firstVerificationDiagnostics3 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); - var secondVerificationDiagnostics3 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var firstVerificationDiagnostics3 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var secondVerificationDiagnostics3 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); //Reordering means the error could be solved first //Assert.AreEqual(1, firstVerificationDiagnostics3.Length); // Still contains second failing method Assert.AreEqual(0, secondVerificationDiagnostics3.Length); @@ -832,16 +832,16 @@ await SetUp(new Dictionary() { }); var documentItem = CreateTestDocument(source); client.OpenDocument(documentItem); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); Assert.AreEqual(0, resolutionDiagnostics.Length); - var firstVerificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var firstVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); Assert.AreEqual(1, firstVerificationDiagnostics.Length); ApplyChange(ref documentItem, new Range((1, 9), (1, 14)), "true"); - var resolutionDiagnostics2 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var resolutionDiagnostics2 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); AssertDiagnosticListsAreEqualBesidesMigration(firstVerificationDiagnostics, resolutionDiagnostics2); - var firstVerificationDiagnostics2 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); - var secondVerificationDiagnostics2 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var firstVerificationDiagnostics2 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var secondVerificationDiagnostics2 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); Assert.AreEqual(0, firstVerificationDiagnostics2.Length); // Still contains second failing method Assert.AreEqual(1, secondVerificationDiagnostics2.Length); @@ -864,10 +864,10 @@ await SetUp(new Dictionary() { }); var documentItem = CreateTestDocument(source); client.OpenDocument(documentItem); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); Assert.AreEqual(0, resolutionDiagnostics.Length); - var firstVerificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); - var secondVerificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var firstVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var secondVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); Assert.AreEqual(1, firstVerificationDiagnostics.Length); Assert.AreEqual(2, secondVerificationDiagnostics.Length); @@ -880,11 +880,11 @@ await SetUp(new Dictionary() { */ ApplyChange(ref documentItem, new Range((2, 0), (4, 0)), ""); - var resolutionDiagnostics2 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var resolutionDiagnostics2 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); // Resolution diagnostics still contain those of the deleted method. AssertDiagnosticListsAreEqualBesidesMigration(secondVerificationDiagnostics, resolutionDiagnostics2); - var firstVerificationDiagnostics2 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var firstVerificationDiagnostics2 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); // The second assert doesn't create a separate error since it's hidden by the first one. // The diagnostics of test2 has not been migrated since test2 no longer exists. Assert.AreEqual(1, firstVerificationDiagnostics2.Length); @@ -929,9 +929,9 @@ method Foo() { var preChangeDiagnostics = await GetLastVerificationDiagnostics(documentItem, CancellationToken); await AssertNoDiagnosticsAreComing(); ApplyChange(ref documentItem, new Range(0, 7, 0, 10), "Bar"); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); Assert.AreEqual(preChangeDiagnostics[0], resolutionDiagnostics[0]); - var finalDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var finalDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(resolutionDiagnostics[0], finalDiagnostics[0]); } @@ -949,9 +949,9 @@ method Bar() { var preChangeDiagnostics = await GetLastVerificationDiagnostics(documentItem, CancellationToken); await AssertNoDiagnosticsAreComing(); ApplyChange(ref documentItem, new Range(0, 7, 0, 10), "Zap"); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); Assert.AreEqual(preChangeDiagnostics[0], resolutionDiagnostics[0]); - var finalDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var finalDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(resolutionDiagnostics[0], finalDiagnostics[0]); } } diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs index d96c0fb6fad..ef6ac27c163 100644 --- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs @@ -18,16 +18,16 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Util; public class ClientBasedLanguageServerTest : DafnyLanguageServerTestBase { protected ILanguageClient client; - protected DiagnosticsReceiver diagnosticReceiver; + protected DiagnosticsReceiver diagnosticsReceiver; public async Task GetLastVerificationDiagnostics(TextDocumentItem documentItem, CancellationToken cancellationToken = default, int? expectedNumber = null) { await client.WaitForNotificationCompletionAsync(documentItem.Uri, cancellationToken); var document = await Documents.GetVerifiedDocumentAsync(documentItem); - await diagnosticReceiver.AwaitNextDiagnosticsAsync(cancellationToken); // Get resolution diagnostics + await diagnosticsReceiver.AwaitNextDiagnosticsAsync(cancellationToken); // Get resolution diagnostics var remainingDiagnostics = expectedNumber ?? Int32.MaxValue; Diagnostic[] result; do { - result = await diagnosticReceiver.AwaitNextDiagnosticsAsync(cancellationToken); + result = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(cancellationToken); remainingDiagnostics--; } while (!document!.Diagnostics.SequenceEqual(result) && remainingDiagnostics > 0); @@ -37,9 +37,9 @@ public async Task GetLastVerificationDiagnostics(TextDocumentItem [TestInitialize] public virtual async Task SetUp() { - diagnosticReceiver = new(); + diagnosticsReceiver = new(); client = await InitializeClient(options => { - options.OnPublishDiagnostics(diagnosticReceiver.NotificationReceived); + options.OnPublishDiagnostics(diagnosticsReceiver.NotificationReceived); }, serverOptions => { serverOptions.Services.AddSingleton(serviceProvider => new SlowVerifier( serviceProvider.GetRequiredService>(), @@ -74,12 +74,12 @@ public async Task AssertNoDiagnosticsAreComing() { } var verificationDocumentItem = CreateTestDocument("class X {does not parse", $"verification{fileIndex++}.dfy"); await client.OpenDocumentAndWaitAsync(verificationDocumentItem, CancellationToken.None); - var resolutionReport = await diagnosticReceiver.AwaitNextNotificationAsync(CancellationToken.None); + var resolutionReport = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken.None); Assert.AreEqual(verificationDocumentItem.Uri, resolutionReport.Uri); client.DidCloseTextDocument(new DidCloseTextDocumentParams { TextDocument = verificationDocumentItem }); - var hideReport = await diagnosticReceiver.AwaitNextNotificationAsync(CancellationToken.None); + var hideReport = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken.None); Assert.AreEqual(verificationDocumentItem.Uri, hideReport.Uri); } } \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs b/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs index 805661a81b3..a80c9b71948 100644 --- a/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs @@ -132,7 +132,7 @@ public async Task ChangeDocumentCancelsPreviousOpenAndChangeVerification() { var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationTokenWithHighTimeout); // The original document contains a syntactic error. - var initialLoadDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationTokenWithHighTimeout, documentItem); + var initialLoadDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationTokenWithHighTimeout, documentItem); await AssertNoDiagnosticsAreComing(); Assert.AreEqual(1, initialLoadDiagnostics.Length); @@ -140,16 +140,16 @@ public async Task ChangeDocumentCancelsPreviousOpenAndChangeVerification() { // Wait for resolution diagnostics now, so they don't get cancelled. // After this we still have never completing verification diagnostics in the queue. - var parseErrorFixedDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationTokenWithHighTimeout, documentItem); + var parseErrorFixedDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationTokenWithHighTimeout, documentItem); Assert.AreEqual(0, parseErrorFixedDiagnostics.Length); // Cancel the slow verification and start a fast verification ApplyChange(ref documentItem, new Range((0, 0), (3, 1)), "function GetConstant(): int ensures false { 1 }"); - var parseErrorStillFixedDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationTokenWithHighTimeout, documentItem); + var parseErrorStillFixedDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationTokenWithHighTimeout, documentItem); Assert.AreEqual(0, parseErrorStillFixedDiagnostics.Length); - var verificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationTokenWithHighTimeout, documentItem); + var verificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationTokenWithHighTimeout, documentItem); Assert.AreEqual(1, verificationDiagnostics.Length); await AssertNoDiagnosticsAreComing(); @@ -173,10 +173,10 @@ public async Task ChangeDocumentCancelsPreviousResolution() { // Fix resolution error, cancel previous diagnostics ApplyChange(ref documentItem, new Range((0, 30), (0, 31)), "1"); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); Assert.AreEqual(0, resolutionDiagnostics.Length); - var verificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); + var verificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem); Assert.AreEqual(0, verificationDiagnostics.Length); await AssertNoDiagnosticsAreComing(); diff --git a/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs b/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs index e30791310a7..fcc84b972d6 100644 --- a/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs @@ -22,7 +22,7 @@ public async Task ResolutionDiagnosticsContainPreviousVerificationResultsWhenCod var verificationDiagnostics = await GetLastVerificationDiagnostics(documentItem, CancellationToken); Assert.AreEqual(1, verificationDiagnostics.Length); ApplyChange(ref documentItem, new Range(0, 47, 0, 47), "\n\n" + NeverVerifies); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(verificationDiagnostics[0], resolutionDiagnostics[0]); } @@ -33,7 +33,7 @@ public async Task ResolutionDiagnosticsContainPreviousVerificationResultsWhenCod var verificationDiagnostics = await GetLastVerificationDiagnostics(documentItem, CancellationToken); Assert.AreEqual(1, verificationDiagnostics.Length); ApplyChange(ref documentItem, new Range(0, 0, 0, 0), NeverVerifies + "\n\n"); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, resolutionDiagnostics.Length); // Verification diagnostic should have been moved. Assert.AreEqual(5, resolutionDiagnostics[0].Range.Start.Line); @@ -48,7 +48,7 @@ public async Task ResolutionDiagnosticsAreRemovedWhenRangeIsDeleted() { var verificationDiagnostics = await GetLastVerificationDiagnostics(documentItem, CancellationToken); Assert.AreEqual(1, verificationDiagnostics.Length); ApplyChange(ref documentItem, new Range(0, 0, 1, 0), ""); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(0, resolutionDiagnostics.Length); } @@ -92,7 +92,7 @@ public async Task ResolutionDiagnosticsAreKeptWhenNonEdgeCrossingChangesAreMade( } }); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(verificationDiagnostics.Length, resolutionDiagnostics.Length); Assert.AreEqual(verificationDiagnostics[0].Message, resolutionDiagnostics[0].Message); Assert.AreEqual(verificationDiagnostics[0].RelatedInformation, resolutionDiagnostics[0].RelatedInformation); @@ -104,17 +104,17 @@ public async Task PassingANullChangeRangeClearsDiagnostics() { var documentItem = CreateTestDocument("method t() { var x: bool := 0; }"); client.OpenDocument(documentItem); - var resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, resolutionDiagnostics.Length); ApplyChange(ref documentItem, null, "method u() ensures true; { var x: bool := true; }"); - resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); - var verificationDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var verificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(0, resolutionDiagnostics.Length); Assert.AreEqual(0, verificationDiagnostics.Length); ApplyChange(ref documentItem, new Range(0, 42, 0, 46), "1"); - resolutionDiagnostics = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + resolutionDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, resolutionDiagnostics.Length); } @@ -131,9 +131,9 @@ public async Task VerificationDiagnosticsCanBeMigratedAcrossMultipleResolutions( Assert.AreEqual(1, verificationDiagnostics.Length); ApplyChange(ref documentItem, new Range(0, 7, 0, 7), "{:neverVerify}"); - var resolutionDiagnostics1 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var resolutionDiagnostics1 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); ApplyChange(ref documentItem, new Range(3, 9, 3, 10), "2"); - var resolutionDiagnostics2 = await diagnosticReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + var resolutionDiagnostics2 = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.AreEqual(1, resolutionDiagnostics1.Length); Assert.AreEqual(1, resolutionDiagnostics2.Length); diff --git a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs index 0c1ce098867..cef997a068c 100644 --- a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs +++ b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs @@ -91,8 +91,10 @@ public IReadOnlyList Verify(DafnyDocument document, DafnyOptions.O.TimeLimit = options.TimeLimit; DafnyOptions.O.VcsCores = GetConfiguredCoreCount(options); DafnyOptions.O.Printer = printer; + var engineOptions = new DafnyOptions(DafnyOptions.O); + engineOptions.Printer = printer; - var executionEngine = new ExecutionEngine(DafnyOptions.O, cache); + var executionEngine = new ExecutionEngine(engineOptions, cache); #pragma warning disable VSTHRD002 var translated = Task.Factory.StartNew(() => Translator.Translate(program, errorReporter, new Translator.TranslatorFlags { InsertChecksums = true,