request for a brutal visual symbol for ":only" mode

[kjx]

Failing code

lemma {:only} OBrien()
//If the Leader says of such and such an event, "It never happened"— well, it never happened.

lemma WinstonSmith()
// If he says that "two and two are five"—well, two and two are five.
 ensures 2 + 2 == 5
 {}

Steps to reproduce the issue

• Dafny version: 4.9.2.0
• Dafny VSCode extension version: 3.4.3
• paste in the above code
• for extra points, use --filter from the CLI to the same effect

Actual behaviour

• IDE reports "verification successful" or "Dafny program verifier finished with 15 verified, 0 errors"
• IDE can lead green gutter markers which may not be correct

Expected behavior

• be good to do something in all these cases to say "verification partially successful" or 15 verified, 0 errors, 103 ignored.

[MikaelMayer]

Is it still the case? I think this one was fixed

[kjx]

Hi Mikael - seems this is fixed in the IDE (so the green gutter bar goes away) - which is great - but the command line reports (in green)

Dafny program verifier finished with 2 verified, 0 errors

without saying something like

Dafny program verifier finished with 2 verified, 0 errors, 247 ignored

and yes, there is a yellow warning about "only" mixed in with every other warning

[kjx]

so the catch is it's not just {:only}

{:verify false} is even more evil, innit?