Fix: Prevent diagnostics to "pass through" #2142
Conversation
|
|
||
| var executionEngine = new ExecutionEngine(DafnyOptions.O, cache); | ||
| var executionEngine = new ExecutionEngine(engineOptions, cache); |
There was a problem hiding this comment.
This is the actual fix of this entire PR.
| @@ -22,7 +22,7 @@ public class DiagnosticMigrationTest : ClientBasedLanguageServerTest { | |||
| 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); | |||
There was a problem hiding this comment.
The only change in this file is the refactoring diagnosticReceiver => diagnosticsReceiver
| @@ -132,24 +132,24 @@ decreases y | |||
| 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); | |||
There was a problem hiding this comment.
The only change of this file is diagnosticReceiver => disagnosticsReceiver
| @@ -18,16 +18,16 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Util; | |||
|
|
|||
| public class ClientBasedLanguageServerTest : DafnyLanguageServerTestBase { | |||
| protected ILanguageClient client; | |||
| protected DiagnosticsReceiver diagnosticReceiver; | |||
| protected DiagnosticsReceiver diagnosticsReceiver; | |||
There was a problem hiding this comment.
The only change of this file is diagnosticReceiver => disagnosticsReceiver
| @@ -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); | |||
There was a problem hiding this comment.
After this change and up to the last file, everything is only a refactoring from diagnosticReceiver to disagnosticsReceiver
| var documentItem = CreateTestDocument(code); | ||
| await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); | ||
| var documentItem = CreateTestDocument(code, fileName); | ||
| client.OpenDocument(documentItem); |
There was a problem hiding this comment.
It kept throwing obscure Omnisharp errors if I was using OpenDocumentAndWaitAsync in the presence of multiple documents. I don't know why, and OpenDocument was working.
| private const int MaxSimultaneousVerificationTasks = 3; | ||
|
|
||
| protected DiagnosticsReceiver[] diagnosticsReceivers = new DiagnosticsReceiver[MaxSimultaneousVerificationTasks]; | ||
| protected TestNotificationReceiver<VerificationStatusGutter>[] verificationDiagnosticsReceivers = |
There was a problem hiding this comment.
I think verificationDiagnostics is an ambiguous term, since we have LSP diagnostics related to verification, verification status tree notifications, and verification gutter icons notifications. I would prefer for diagnostics to refer only to LSP diagnostics.
| ); | ||
| } | ||
|
|
||
| [TestMethod/*, Timeout(MaxTestExecutionTimeMs)*/] |
There was a problem hiding this comment.
This test still has some commented out code.
| public class ConcurrentLinearVerificationDiagnosticTester : LinearVerificationDiagnosticTester { | ||
| private const int MaxSimultaneousVerificationTasks = 3; | ||
|
|
||
| protected DiagnosticsReceiver[] diagnosticsReceivers = new DiagnosticsReceiver[MaxSimultaneousVerificationTasks]; |
There was a problem hiding this comment.
I don't understand why you create multiple receivers.
There was a problem hiding this comment.
I don't understand why you create multiple receivers.
I removed the diagnostic receivers, I didn't need them anymore
| await result[i]; | ||
| } | ||
|
|
||
| //await Task.WhenAll(result.ToArray()); |
There was a problem hiding this comment.
Should this be removed?
There was a problem hiding this comment.
Yes it can. I'll remove it in another PR.
|
|
||
| private void NotifyAllVerificationGutterStatusReceivers(VerificationStatusGutter request) { | ||
| foreach (var receiver in verificationStatusGutterReceivers) { | ||
| receiver.NotificationReceived(request); |
There was a problem hiding this comment.
I'm confused by this. All verificationStatusGutterReceivers receive the same notifications, which would be the notifications for all the tasks. How does VerifyTrace that gets verificationStatusGutterReceivers[i] not get confused by the bogus notifications?
There was a problem hiding this comment.
It checks that the filename matches and filters out notifications that do not match.
That way, it can rebuild the trace for every file independently.
There was a problem hiding this comment.
Could you explain that in a comment in the testing code?
There was a problem hiding this comment.
Added a commit in #1946 to add a comment regarding this.
This will solve some noisy log messages seen recently in CI / DafnyLanguageServer, and fix potential problems about setting the printer.
I added a test that, if I revert the first commit of this PR, will just fail because of this shared static variable.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.