{:only} issues

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

// file1.dfy
module X {
  method {:only} VerifyMe() {
    assert true;
  }
}

// file2.dfy
include "file1.dfy"
module Y {
  import X
  method VerifyMeToo() {
    assert false;        // Gutter icons in VSCode show that this method is verified
  }
}

Command to run and resulting output

$ dafny verify --filter-symbol "VerifyMeToo" file2.dfy
file1.dfy(2,9): Warning: Members with {:only} temporarily disable the verification of other members in the entire file
  |
2 |   method {:only} VerifyMe() {
  |          ^^^^^^^


Dafny program verifier finished with 0 verified, 0 errors
Compilation failed because warnings were found and --allow-warnings is false

What happened?

Four issues there:

• The warning about the {:only} is not mentioned in VSCode, only on the command-line.
• The gutter icons are green. If we inlined the included file, it would fix this and the previous issue.
• The method itself has no warning indicating it's not verified.
• The documentation states that it deactivate verification of other methods in the same file but that extends beyond the file in which {:only} was written.

What type of operating system are you experiencing the problem on?

Windows

[keyboardDrummer]

We now have some IDE (play icon) and CLI options (--filter-symbol/--filter-position) to verify specific things. What's still missing from the IDE is an option to verify individual assertions.

However, once we have that, is there still a use-case for {:only}? To me the act of making source changes to help development does not seem like a good UX, and can even be unsafe when those changes are accidentally committed.

[MikaelMayer]

{:only} is more useful as assume false; nowadays. What is unsafe is to ignore warnings.

On my side, I'm not using the IDE UX that requires clicking on buttons to verify my code. I prefer that everything happens automatically whenever I type something. If you can trigger verification on change with your mode, while making it possible to restrict verification to some methods, then I personally won't use {:only}.

[keyboardDrummer]

{:only} is more useful as assume false; nowadays. What is unsafe is to ignore warnings.

On my side, I'm not using the IDE UX that requires clicking on buttons to verify my code. I prefer that everything happens automatically whenever I type something. If you can trigger verification on change with your mode, while making it possible to restrict verification to some methods, then I personally won't use {:only}.

Fair