-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fix: Prevent diagnostics to "pass through" #2142
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A few comments to ease the review of this PR.
|
||
var executionEngine = new ExecutionEngine(DafnyOptions.O, cache); | ||
var executionEngine = new ExecutionEngine(engineOptions, cache); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't understand why you create multiple receivers.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should this be removed?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you explain that in a comment in the testing code?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.