Verification does not recover from parsing failure

[tchajed]

In the default onchange setting for Automatic Verification, after a parsing failure Dafny does not recover and start reporting verification successes. This basically makes it unusable, except by frequently reloading the VS Code window.

Here's a video of me doing something basic where the status gets stuck on "Parsing...": Dafny VS Code bug.

I'm using Dafny 4.2.0 and v3.1.2 of the VS Code extension. I'm on an Apple Silicon Mac.

[keyboardDrummer]

Hey, sorry to hear you're running into this! This is awful.

Could you try to set your VSCode Dafny to use "latest nightly" ? Go to VSCode's preferences, filter on Dafny, and at the bottom of the options list you can find the version selector. We've resolved several performance related issues after 4.2, and it seems you're running into them. I'm planning to release a new version soon but currently doing more testing.

[tchajed]

The latest nightly does seem to fix the issue, thanks for pointing that out! I hope you can release 4.3 soon.