Move compilation status updates to notification publisher #4454
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
MikaelMayer
approved these changes
Aug 23, 2023
| @@ -21,7 +21,7 @@ public class CompilationStatusNotificationTest : ClientBasedLanguageServerTest { | |||
| [Fact] | |||
| public async Task MultipleDocuments() { | |||
| var source = @" | |||
| method Foo() returns (x: int) ensures x / 2 == 1; { | |||
| method Foo() returns (x: int) { | |||
There was a problem hiding this comment.
Why did you remove the ensures clause?
There was a problem hiding this comment.
Part of debugging, but it's not needed
| var program = parser.Parse(compilation, errorReporter, cancellationToken); | ||
| var compilationAfterParsing = new CompilationAfterParsing(compilation, program, errorReporter.AllDiagnosticsCopy, | ||
| compilation.RootUris.ToDictionary(uri => uri, | ||
| uri => migratedVerificationTrees.GetValueOrDefault(uri) ?? new DocumentVerificationTree(program, uri))); | ||
| if (errorReporter.HasErrors) { | ||
| _ = statusPublisher.SendStatusNotification(compilation, CompilationStatus.ParsingFailed); |
There was a problem hiding this comment.
Did you ensure that parsing failures are still sent? Normally there should be a test for that but I have not checked.
There was a problem hiding this comment.
There are tests for it yes
keyboardDrummer
added a commit
to keyboardDrummer/dafny
that referenced
this pull request
Sep 15, 2023
…#4454) Fixes dafny-lang#4451 ### Changes - symbolStatus notifications are resent after any document change is made. - "Parsing" is no longer sent when opening a file because it's the default state for a file. This requires an update on the client to return to the old behavior, but in the meantime it's OK for the client to have this tiny regression. - "Preparing Verification" no longer exists as a notification. Because one verifiable can be preparing verification while another is verifying, there is no longer a global "Preparing verification" state so this notification lost its meaning. We can bring something like this back but on a more granular level. - "Resolution Succeeded (not verified)" (UI name) / CompilationSucceeded (server name) no longer exists as a notification. This sat between ResolutionStarted and symbolStatus notifications that indicated which symbols could be verified, but in practice was never shown because immediately after it symbolStatus notifications would be sent that trigger a status like "Verified X declarations, skipped Y" - `CompilationManager` no longer sends any status updates to the IDE client, bringing it closer to being able to be moved to `DafnyCore` and used by the CLI. ### Testing - Updated automating tests <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
keyboardDrummer
added a commit
that referenced
this pull request
Sep 19, 2023
Fixes #4451 ### Changes - symbolStatus notifications are resent after any document change is made. - "Parsing" is no longer sent when opening a file because it's the default state for a file. This requires an update on the client to return to the old behavior, but in the meantime it's OK for the client to have this tiny regression. - "Preparing Verification" no longer exists as a notification. Because one verifiable can be preparing verification while another is verifying, there is no longer a global "Preparing verification" state so this notification lost its meaning. We can bring something like this back but on a more granular level. - "Resolution Succeeded (not verified)" (UI name) / CompilationSucceeded (server name) no longer exists as a notification. This sat between ResolutionStarted and symbolStatus notifications that indicated which symbols could be verified, but in practice was never shown because immediately after it symbolStatus notifications would be sent that trigger a status like "Verified X declarations, skipped Y" - `CompilationManager` no longer sends any status updates to the IDE client, bringing it closer to being able to be moved to `DafnyCore` and used by the CLI. ### Testing - Updated automating tests <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fixes #4451
Changes
CompilationManagerno longer sends any status updates to the IDE client, bringing it closer to being able to be moved toDafnyCoreand used by the CLI.Testing
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.