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

Using {:only} to focus verification #4432

Closed
seebees opened this issue Jul 31, 2023 · 0 comments · Fixed by #4433
Closed

Using {:only} to focus verification #4432

seebees opened this issue Jul 31, 2023 · 0 comments · Fixed by #4433
Assignees
Labels
part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) release-blocker Must be resolved before the next release

Comments

@seebees
Copy link

seebees commented Jul 31, 2023

This is a great feature.
However, everything that is not {:only} will also be tagged green.

They really should be grey/or black.
Since they are not verified.

Also, there should be a color for things changed outside {:only}.

Take the following situation.
I am working on method A and have tagged it {:only}
so that I can focus my verification.

I realize that function B is involved.
If I add an extra ensures to function B
then I can make progress on method A.
However, since I have only marked method A {:only}
this change is not verified.

Ideally the IDE should either mark function B {:only}
or update the gutter so that it is clear that this is not verified...

Update by @MikaelMayer:

method NotVerified() { // Should not be highlighted in green
  assert 1 == 0;
}
method {:only} Verified() { // Verified
  assert true;
}
method NotVerified2() { // Should not be highlighted in green
  assert 1 == 0;
}
@MikaelMayer MikaelMayer self-assigned this Aug 8, 2023
@MikaelMayer MikaelMayer transferred this issue from dafny-lang/ide-vscode Aug 17, 2023
@MikaelMayer MikaelMayer added the part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) label Aug 17, 2023
MikaelMayer added a commit that referenced this issue Aug 17, 2023
@MikaelMayer MikaelMayer added the release-blocker Must be resolved before the next release label Aug 29, 2023
MikaelMayer added a commit that referenced this issue Sep 19, 2023
…displayed as verified in the gutter icons (#4433)

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 |
|--------------------------|---------------|
|
![image](https://github.com/dafny-lang/dafny/assets/3601079/9b8e98c2-00a7-4e44-b31a-ba8c5c668a2c)
|
![image](https://github.com/dafny-lang/dafny/assets/3601079/5e44226e-5897-4f1e-8223-c7d37b64ab68)
|
|--------------------------|--------------|
|
![image](https://github.com/dafny-lang/dafny/assets/3601079/bbbb2658-ac9d-441d-9edb-fcc3c489f44c)
|
![image](https://github.com/dafny-lang/dafny/assets/3601079/a6abf19b-d2c8-41d7-939c-fb846d7d4681)
|
|--------------------------|--------------|

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
keyboardDrummer pushed a commit that referenced this issue Sep 26, 2023
…displayed as verified in the gutter icons (#4433)

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 |
|--------------------------|---------------|
|
![image](https://github.com/dafny-lang/dafny/assets/3601079/9b8e98c2-00a7-4e44-b31a-ba8c5c668a2c)
|
![image](https://github.com/dafny-lang/dafny/assets/3601079/5e44226e-5897-4f1e-8223-c7d37b64ab68)
|
|--------------------------|--------------|
|
![image](https://github.com/dafny-lang/dafny/assets/3601079/bbbb2658-ac9d-441d-9edb-fcc3c489f44c)
|
![image](https://github.com/dafny-lang/dafny/assets/3601079/a6abf19b-d2c8-41d7-939c-fb846d7d4681)
|
|--------------------------|--------------|

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) release-blocker Must be resolved before the next release
Projects
None yet
2 participants