Fix: Declarations with {:only} ensure that other declarations aren't displayed as verified in the gutter icons

[MikaelMayer]

This PR fixes #4432
I added the corresponding test.

Because the Skipped gutter icon is not supported yet in VSCode, it's just rendered as no icon, which is suitable for now at least to indicate that a method is not verified.

Before, without this PR	With this PR
--------------------------	--------------
--------------------------	--------------

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[keyboardDrummer]

I'm doubtful that it's a good idea to keep the current gutter icon notification API. If possible, and it seems so, I think we should compute gutter icons on the client, since computing on the client prevents equivalent pieces of information that are out-of-sync from reaching the client, and reduces bandwidth usage.

The API change in this PR makes it so that the client no longer has enough information to recompute the same icons without the gutter notifications.

If we want to compute the icons on the client, we should use a different API to tell the client which locations have been skipped from verification. One that comes to my mind is the diagnostics one, since it has a range field. You could emit a warning with a specific code, and the client could either:

• display this as a regular warning
• recognize the specific error code, remove the diagnostic from its list and instead display it as different icons in the gutter.

---

Also, are there other APIs that need to take {:only} into account? What about dafny/textDocument/symbolStatus ? What does the status bar display if you verify a method that's excluded from verification because of {:only} on another method?

[MikaelMayer]

I'm doubtful that it's a good idea to keep the current gutter icon notification API. If possible, and it seems so, I think we should compute gutter icons on the client, since computing on the client prevents equivalent pieces of information that are out-of-sync from reaching the client, and reduces bandwidth usage.

Thanks for sharing your concern.
That's ok and that's another discussion to have, this PR is about fixing current things with the current API, which is faster than designing, reviewing and implementing a new way to compute gutter icons, even if it's better. So please separate the concern of the need of reducing bandwidth and the confusion the gutter icons currently provide in the case of {:only}

The API change in this PR makes it so that the client no longer has enough information to recompute the same icons without the gutter notifications.

Fixing that is a no-brainer. Just add the same information in the tree that you have.

If we want to compute the icons on the client, we should use a different API to tell the client which locations have been skipped from verification. One that comes to my mind is the diagnostics one, since it has a range field. You could emit a warning with a specific code, and the client could either:

• display this as a regular warning
• recognize the specific error code, remove the diagnostic from its list and instead display it as different icons in the gutter.

Also, are there other APIs that need to take {:only} into account? What about dafny/textDocument/symbolStatus ? What does the status bar display if you verify a method that's excluded from verification because of {:only} on another method?

Symbol status says "verified". You could also file an issue for that and I'd be happy to look at it if time permits..

[keyboardDrummer]

That's ok and that's another discussion to have, this PR is about fixing current things with the current API, which is faster than designing, reviewing and implementing a new way to compute gutter icons, even if it's better.

That's true.

But this PR is also a feature enhancement that makes it harder to replace this feature with a more performant one.

Fixing that is a no-brainer. Just add the same information in the tree that you have.

I don't think it's a no-brainer to make API changes. I'm inclined to use warning diagnostics for it since they don't require API changes.

[MikaelMayer]

That's ok and that's another discussion to have, this PR is about fixing current things with the current API, which is faster than designing, reviewing and implementing a new way to compute gutter icons, even if it's better.

That's true.

But this PR is also a feature enhancement that makes it harder to replace this feature with a more performant one.

Removing the green gutter icon on non-verified functions was part of the design of the {:only} feature, it's just I postponed it to a separate PR until recently.

What you suggest does make sense, adding a warning range on non-verified code can makes things easier to spot and to compute on the client side.

Fixing that is a no-brainer. Just add the same information in the tree that you have.

I don't think it's a no-brainer to make API changes. I'm inclined to use warning diagnostics for it since they don't require API changes.

What you call an API change was an actual expected backward-compatible and forward-compatible API change. Gutter icons had "holes" in their numbering, allowing to create other icons as needed.

[keyboardDrummer]

Can you add a test that verifies the symbolStatus API returns Stale as a status for methods/functions that are skipped because of {:only} ? I would like to keep the symbolStatus API and the gutter icon API in sync (I'm always done with a PR that switches away from using the gutter icons, so we'll need the updated symbolStatus API)

[MikaelMayer]

Since @keyboardDrummer requests more nontrivial work to ensure the verification symbols are also not displayed as verified, but I can't do that right now, I'll go back to this PR on October 10th or before.

[MikaelMayer]

I created another issue for your issue @keyboardDrummer
#4544
so that we can merge this fix while I find the time to work on the other one.