-
Notifications
You must be signed in to change notification settings - Fork 260
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: "Stuck on Verifying..." #1771
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.
Only some small inputs, and it appears something's wrong with the tests.
I'm quite impressed that this feature didn't require changes to the language server itself. 😄
This will sure have a huge impact on UX.
}".TrimStart(); | ||
var documentItem = CreateTestDocument(source); | ||
client.OpenDocument(documentItem); | ||
Thread.Sleep(5000); |
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.
Prefer using await Task.Delay(5_000);
here
@@ -100,11 +100,11 @@ public class DafnyProgramVerifier : IProgramVerifier { | |||
// However, the cancelling a verification is currently not possible since it blocks a text document |
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 we can remove this comment now
Just in case you're waiting for the approval: I think you didn't push your latest changes. 😄 |
Indeed, I did not, because there is still a problem in Boogie where counter-examples are not reported correctly anymore. I'll be waiting on Boogie to be compatible with Dafny again to solve this issue. |
This PR adds no new operational code because the fix is in Boogie:
boogie-org/boogie#491
This fix has been merged, and this PR bumps the Boogie version, so the test included should now pass.
This tests asks the verifier to do something hard, and cancels verification by performing a change on the text.
Until this PR, the verifier is stuck verifying, but with the fix above, it will cancel verification, kill zombie processes, and continue smoothly