non-non-non-optional semicolons give horrible error messages - LOW SEVERITY

[kjx]

Dafny version

4.6.0

Code to produce this issue

method Main() { assert 3 == 3 by { true; }; }

Command to run and resulting output

bluebook:~ kjx$ "/usr/local/share/dotnet/dotnet" "/Users/kjx/.vscode/extensions/dafny-lang.ide-vscode-3.3.0/out/resources/nightly-2024-05-05-55d1c40/github/dafny/Dafny.dll" "run" "--no-verify" "/Users/kjx/work/dafny/wont-2.dfy"
work/dafny/wont-2.dfy(1,49): Error: rbrace expected
  |
1 | method Main() { assert 3 == 3 by { assert true; }; }
  |                                                  ^

1 parse errors detected in wont-2.dfy

What happened?

I spent ten minutes staring at this.

most "statements" in method bodies need closing semicolons. assert 3 == 3; //does assert 3 == 3 by { assert true; } //does not

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

Mac

[keyboardDrummer]

I think the pattern is that statements ending in }, such as loops and conditionals, and statements with a by clause, do not need an ; after the }.

What change are you suggesting?

I trust you when you say the current behavior is confusing, but it would help to have an idea of how to improve it.

[keyboardDrummer]

Marking as enhancement not bug, since this is documented behavior.

[kjx]

• what to change - permitting "empty" statements - sequences of semicolons - may be the easiest fix. makes this less sensitive

• I'm not that bothered by Python-style omitted semicolons, so I'm not the best person to ask.

• I think we did a good job in Grace, or at least one I personally liked (semicolons are optional, layout is used to do secondary grouping. I thought it was philosophically the worst of both worlds, but it seemed to work quite nicely!

• but with Dafny now sometimes looking at layout to give hints, etc, and general inconsistency, perhaps we've been piped at the post?

• OK, I can list such things as enhanements in future