Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Squigly lines don't disappear for Veryfication Caching Policy = basic or advanced #187

Closed
xtrm0 opened this issue Jun 28, 2022 · 1 comment · Fixed by dafny-lang/dafny#2312
Closed

Squigly lines don't disappear for Veryfication Caching Policy = basic or advanced #187

xtrm0 opened this issue Jun 28, 2022 · 1 comment · Fixed by dafny-lang/dafny#2312
Assignees
@MikaelMayer

Comments

@xtrm0
Copy link

xtrm0 commented Jun 28, 2022

If:

  1. option dafny.verificationCachingPolicy is set to anything other than none
  2. a file has been verified once
  3. some change happens on the file triggering verification again

Then the green squigly lines (meaning that the verification for those lines is running again and hasn't finished) is not disapearing. This is a bit confusing.

Example (First few lines are both squiggly and opaque light green because they were both cached (so the squigly lines failed to disapear) and verified, last few lines are opaque light green because they were verified just now, and so the squigly lines disapeared)
image

Is this intended behavior, if so, what is the meaning of the light green squigly lines?
MikaelMayer added a commit to dafny-lang/dafny that referenced this issue Jun 28, 2022
@MikaelMayer
Fixes dafny-lang/ide-vscode#187
1065420
@MikaelMayer MikaelMayer mentioned this issue Jun 28, 2022
Merged
@MikaelMayer
Copy link
Member

Thank you very much for spotting it ! It is not intended behavior. It's a bug. I just fixed it.

keyboardDrummer pushed a commit to dafny-lang/dafny that referenced this issue Jul 1, 2022
@MikaelMayer
Fixes gutter when cache is enabled (#2312)
9dab9d7 
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
* It also report all the results that were cached as if they were resolved immediately.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@MikaelMayer MikaelMayer

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fixes gutter when cache is enabled dafny-lang/dafny
2 participants
@xtrm0 @MikaelMayer