Seeing "Resolving..." indefinitely even though verification is otherwise working

[ethanbb]

Failing code

Seems to happen with pretty much any code, but this is an example:

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
    requires y > 0
    ensures less < x
    ensures x < more
{
    more := x + y;
    less := x - y;
}

Steps to reproduce the issue

• Dafny version: 4.10.0.0
• Dafny VSCode extension version: 3.4.4
• .NET 9
• Windows 11 24H2
• Open VS Code or restart Dafny with a file with the above code open, status bar says "Verification Succeeded"
• Delete a brace or something, status bar says "Parsing Failed"
• Undo

Expected behavior

• Status bar continues to update rather than getting stuck at "Resolving..."

Actual behavior

• Status bar says "Resolving..." forever (sometimes on 2nd or 3rd time).
• Does not say Verification Succeeded again until Dafny is retarted
• Gutter and tests tab show checkmarks, hover tooltips look correct, etc. Also verification succeeds at the command line.
• Dafny Language Server output: "[Error - 11:32:10 PM] Server process exited with code 0." (when verbose logging is turned on, it seems correct and continues to respond.)

[ethanbb]

So as I continued to work through the tutorial, at some point the file got long enough and/or conditions complex enough that verification was taking several seconds, and at that point the status bar started working normally. At the same time, I started to see the squiggly "working" feedback in the gutter, which I'm guessing did not appear before just because verification completed so quickly.

So it seems like this only occurs with simple files that verify very quickly (so maybe not a high priority)

[keyboardDrummer]

I couldn't reproduce this with the file you pasted. Removing the brace and then undoing lets the status bar go back to "Verified .."

So it seems like this only occurs with simple files that verify very quickly (so maybe not a high priority)

Maybe there's a concurrency issue where the "Resolving..." status message is received by the client after the "Verified ..." status message. Could you follow these steps to gather more data:

1. Run the VSCode command "Open User Settings (JSON)" and then paste "dafny-vscode.trace.server": "verbose", into the file
2. Reproduce the issue
3. Go to the output tab and the "Dafny Language Server" channel.
4. Paste the contents into a file and attach that to this ticket

Thanks a lot!

[ethanbb]

No problem, here's what came out (attached).

dafny_language_server_resolving.txt