-
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
Fixes gutter when cache is enabled #2312
Conversation
await VerifyTrace(@" | ||
. S [S][ ][I][S][S][ ]:method test() { | ||
. S [O][O][o][Q][O][O]: assert true; | ||
. S [=][=][-][~][=][=]: assert false; |
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.
Before the fix, the last [O] and [=] would have been replaced by [ ] because the result of individual cached splits were not reported the second time.
await VerifyTrace(@" | ||
. S S | I $ | :method test() { | ||
. S | | I $ | : assert true; | ||
. S S | I $ | : //Next: |
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.
Before the fix, this text would not terminate because it would never get back to the | icon
@@ -20,5 +20,6 @@ public interface IVerificationProgressReporter { | |||
void ReportEndVerifyImplementation(Implementation implToken, Boogie.VerificationResult verificationResult); | |||
void ReportImplementationsBeforeVerification(Implementation[] implementations); | |||
void ReportAssertionBatchResult(AssertionBatchResult batchResult); | |||
void ReportAssertionBatchResult(Implementation implementation, VCResult batchResult); |
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 find having two methods ReportAssertionBatchResult
to be confusing. What do you think?
Seems like you could also change AssertionBatchResult
so it contains only an Implementation
and a VCResult
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 first signature makes something nice, it's possible assign AssertionBatchResult
s to their correct implementation in a threaded way:
dafny/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
Lines 136 to 137 in 07d614f
var subscription = verifier.BatchCompletions.Where(c => | |
implementations.Contains(c.Split.Implementation)).Subscribe(progressReporter.ReportAssertionBatchResult); |
The second signature is the one I need because I don't have the split available, only the implementation and the result from the cache.
I just pushed something I'm satisfied with: I removed the split from AssertionBatchResult
and just included the Implementation
because we are not using other properties of the split anyway.
Fixes dafny-lang/ide-vscode#187
The issue was that caching would prevent reports of implementations being finished to verify for the gutter reporting mechanism. I added it, and a test that I verified would not work in the absence of the fix.
Changes
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.