-
Notifications
You must be signed in to change notification settings - Fork 256
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
Resolution errors do not get migrated / do not disappear when there are parse errors #5428
Comments
Merged
keyboardDrummer
added a commit
that referenced
this issue
May 14, 2024
Fixes #5428 ### Description - Revert part of #5243 because this caused complication and it needs better consideration before being done. ### How has this been tested? - Added `ResolutionErrorMigration` to verify #5428 is fixed - Update `CorrectParseDiagnosticsDoNotOverridePreviousResolutionOnes` to account for resolution diagnostics no longer being migrated <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
How to reproduce
Parse the following code:
Then, place the caret just before the "m" of module and then paste the following code (including the final newline)
The problem is, resolution errors are not migrated, and second, resolution errors should be marked as obsolete if parse error occur, just in case, so that users know to focus on parse error instead of resolution errors. Or resolution error should disappear if parse errors occur. But I think that if we could do the same that we do for verification, leave them there
The text was updated successfully, but these errors were encountered: