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.

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

Client side gutter icons #423

Open
wants to merge 33 commits into
base: master
Choose a base branch
from

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented Aug 23, 2023

Changes

  • Compute gutter icons on the client and configure the server so it no longer sends gutter icons to the client.

Here's an example. Left shows client side computed icons, and right shows server side computed icons (using latest nightly):

Client computed Server computed
image image

Left seems more correct, since right indicates errors on line 18 and 20 event though verification found no errors there. Also, left finds proven assertion on line 33 that right does not find.

Testing

  • Manual testing looked good, although I'm sure there are small differences. @MikaelMayer could you also manually test this PR ?
  • Added unit tests for the method computeNewGutterIcons, to check that given the particular symbolStatus, diagnostics and documentSymbol information, the right gutter icons are computed.
  • Did not add an integration test that runs an actual language server and checks that the icons per line evolve according to expectations. Such a test would be difficult to make stable because it depends on having a running language server.

@keyboardDrummer keyboardDrummer enabled auto-merge (squash) August 23, 2023 14:46
@MikaelMayer
Copy link
Member

I just tried this PR with the latest Dafny master. I typed:

method Test() {

}

and got the following result
image
Reloading VSCode on that same file displays nothing in gutter icons.
Even writing "assert true;" inside did not change anything.

The language server was started with these options.

Language server: {"command":"...\\AppData\\Local\\Temp\\vscode-dafny-dlls-W1YBH8\\Dafny.exe","args":["server","--verify-on:Change","--verification-time-limit:30","--cache-verification=0","--cores:4","--notify-ghostness:true","--notify-line-verification-status:false"]}
Dafny is ready

@MikaelMayer
Copy link
Member

Also, what about backward compatibility? We can assume users will always use the most up to date version of VSCode, but not that they will use the most up to date version of Dafny for quite a long time (I've seen migrations lasting 1 year!)
What earliest version of Dafny is your change supporting?

@keyboardDrummer
Copy link
Member Author

keyboardDrummer commented Aug 29, 2023

I'm in a branch that includes my unmerged PRs to Dafny server. Will let you know when those are merged.

Given the code you showed, when opening the file I get:

image

When pressing verification it turns into:
image


Different contents:

With manual verification, on opening file:
image

After clicking verify:
image

image

or with an extra newline:

image

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants