-
Notifications
You must be signed in to change notification settings - Fork 257
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
Fixed verification ordering priority and speedup #2352
Conversation
…fyImplementationRunning
Niiice! I did make a few changes, hope that's OK. I've changed the verification ordering tests so they test against the API instead of internals, and I made two refactorings. |
…-lang/dafny into fix-verification-ordering-priority
…-lang/dafny into fix-verification-ordering-priority
…-lang/dafny into fix-verification-ordering-priority
}); | ||
} | ||
|
||
private Position GetPositionOf(string code, string symbol) { |
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.
Funny would be if we could use LSP's workspace symbol feature to ask for the positions ^^
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 wish too.
… not done at about the same time
Fixes #2347
Also fixes the number of cores to the engine option which was never set, so it defaulted to 1.
Before this PR, on an 8-core machine with vscore set to 8 in VSCode:
After this PR, same machine, same options
Note the small grey bar where it should be green. This is a video encoding issue.
Can you spot the 4 differences?
I did not write tests for verifying ordering as I found such tests used to be unstable and randomly crash the CI. I only did unit testing to verify that the priority is correctly assigned, but that PR fixes the fact that priority setting was done after verification was launched, which was useless.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.