VSCode extension shows forever "verifying" - how to diagnose?

[hmijail]

Dafny 3.1.0.30421 - commit 98e24a6
VSCode 1.55.2
Dafny extension 1.5.0, using LS from external Dafny

My .dfy file opened in VSCode causes it to forever show a "Verifying" message (with circling arrow) in the status bar. There is no Z3 running in the OS Activity Monitor (nor any other process that might look like some work is happening), so looks like this will never change by itself.

Edits in the file might cause the message to stabilize into a "Verified" message, or make it go into "verifying" again. It's a big file, and I didn't manage to extract some snippet that would keep the weird behavior.

Is there any easy way in which I can get some visibility into what's going on, so maybe I can isolate a proper bug report?

[camrein]

Thanks for the report. I just recently received a similar report. The problem you're describing makes me feel that there is some synchronization issue with the UI rather than a problem with the language server.
If I understand you right: The "Verifying..." indicator is showing, and you can still edit and verify other documents in the meantime? This suggests that the verifier is not stuck as it seems to be (other documents may not verify concurrently, they have to wait for the verifier to be "free").

The LS can write log files. You can enable it by replacing the most likely empty nlog.config of your extension install-dir (something like ~/.vscode/extensions/correctnesslab.dafny-vscode-1.5.0/out/resources/dafny) with the one available here. Maybe you'll see some errors in the created log.txt log file.

Nevertheless, I have the feeling that there might be errors happening during the verification. You may already see them in the VSCode output when switching to the Dafny Language Server view, without having to enable the log explicitly:

If everything works fine, it simply should show some JSON communication between the VSCode and LS. If there are errors, you should see some exceptions appear.
In case that there are really errors happening, I'd be grateful if you can share these. Furthermore, I have prepared a branch with a change that ensures that the verification is always updated.

[hmijail]

If I understand you right: The "Verifying..." indicator is showing, and you can still edit and verify other documents in the meantime?

No, once the "Verifying" indicator is showing, other documents don't get verified when I edit them.
They do if I restart the Dafny server.

Looking at the Dafny Language Server view, when I open the affected document, an entry appears like this:

[Trace - 2:54:44 PM] Sending notification 'textDocument/didOpen'.
Params: {
    "textDocument": {
        "uri":...

... which seems to follow the format of previous didOpen entries. But nothing more appears after that, even if I activate other documents.

Relatedly: if VSCode opens with the affected document active, the Dafny Language Server view does not even appear in the popup list. This kept me confused for a while.

I also tried changing the empty nlog.config in that directory you mentioned for the one you provided. I couldn't find any log.txt file being created even after restarting the whole VSCode. When / where should it appear?

[hmijail]

I just tried the stabilize-verification-status branch, but the behavior seems to be the same.

[camrein]

Thanks for your tests. This effectively sounds like the language server gets stuck during verification (or some pre-/post-processing related to it). I already got an earlier report with some code snippet - with the observation that the error did not occur on extension 1.4.0 and its DafnyLS 3.0.0. However, I cannot reproduce the error on my devices and I do not own a Mac/OSX. Would you mind sharing a minimal example? Maybe I have better luck with another example to reproduce the error you're describing.

You should see the logs after adding the contents to nlog.config and restarting VSCode. Although, I don't think there will be any helpful error messages in the log since resources should be freed upon error; thus, the DafnyLS shouldn't get stuck.

[hmijail]

If I manage to isolate a shareable snippet that triggers the problem I'll report back...

As for the logs, nlog.config is already set as suggested but I just don't see any log.txt file being generated. Should it appear in the same directory as nlog.config?

[camrein]

Thanks a lot.

Yes, the log file should be generated within the same dir. But I forgot to mention: Since you have probably configured a custom language server that's not located in the default install dir, you have to place the nlog.config within the dir of your server installation. The log file should appear within the same dir as you have installed the server.

[hmijail]

Aha, thank you, that was it - now I have a log.txt file.
It contains hundreds of lines like

2021-05-06 22:44:59.1884|WARN|Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver|encountered unknown top level declaration Address of type Microsoft.Dafny.OpaqueTypeDecl 
...
2021-05-06 22:44:59.2050|WARN|Microsoft.Dafny.LanguageServer.Language.Symbols.SymbolTableFactory|encountered unknown syntax node of type Microsoft.Dafny.AliasModuleDecl in XXX.dfy@(6,19) 
...
2021-05-06 22:44:59.2050|WARN|Microsoft.Dafny.LanguageServer.Language.Symbols.SymbolTableFactory|could not resolve the symbol of designator named nat in XXX.dfy@(12,36) 
...

... where XXX.dfy is the file that gets stuck in "Verifying".
However I see that even files that don't get stuck seem to generate lots of similar lines, so I guess this is not very meaningful.

[hmijail]

A coarse observation: by looking at macOS' Activity Monitor, I see that verifying a small Dafny file that doesn't exhibit the bug causes some spikes of CPU activity by processes named dotnet and z3.
In comparison, verifying the "bad" Dafny file seems to cause a smaller spike of dotnet and no z3 - in spite of being a much larger file.
So I'd guess that the LS fails before reaching that point.

[camrein]

Thanks a lot for sharing your observations. These warnings are not problematic (I should lower their severity by now) since they only depict language features that are currently not supported by the language server (they'll miss code navigation and similar features). Are there any errors/exceptions within the log?
These spikes are really interesting. You could be right that Z3 is never invoked and the language server gets right before it. Just to make sure: I suppose your "problematic" file compiles and verifies without any issues.

[hmijail]

I just re-checked the executables that are triggered by the editing of code in VSCode, using execsnoop, a DTrace script included with macOS that lists every executable started by the OS - so this is should be the best view one can get, as opposed to the coarse view given by Activity Monitor. And I can confirm now that editing even whitespace in a "correctly-working file" causes the execution of rg and z3. But once the "Verifying" message gets stuck, z3 never runs again on any file, only rg does, until I restart the LS. The "bad" file itself does the same.

In summary: the "bad" file runs rg, never runs z3, gets the "Verifying" message stuck, and from then on z3 never ever runs, only rg.

Are there any errors/exceptions within the log?

No, it is all WARN lines.

I suppose your "problematic" file compiles and verifies without any issues.

No, that file has a few errors of the to be compilable, the value of a let-such-that expression must be uniquely determined kind.
However, as I move those snippets to separate smaller files to fix them, VSCode keeps the verifier working on them without trouble...

[camrein]

I am sorry that my response took so long; I couldn't get access to an OSX device to debug the issue.
Fortunately, I now have a MacBook and did some investigations. The error with the example code I had has immediately resulted in a StackOverflowError in the language server. Strangely enough that this only appears to be a problem on OSX. However, it's not the usual "infinite recursion" programming error; it's just that the language server requires such a large stack. So there is not much we can do on the program side. Although, a solution is the (undocumented) COMPlus_DefaultStackSize environment variable. Setting it to a sufficiently large number resolves the issue. For example, you can run the following command prior to opening VSCode from the shell:

# Increase the stack size
export COMPlus_DefaultStackSize=100000

# Launch VSCode
code

[hmijail]

I can confirm that my big file does finish its verification if I set the COMPlus_DefaultStackSize environment variable.
Do you know if there is any way to get the same result from within VSCode?
And, is there any reason to not set that variable permanently?

[camrein]

Thank you very much for your quick response and confirmation.
If you launch VSCode from a terminal where you set the environment variable, all processes (including the language server) should inherit this setting. Therefore, you should be able to successfully verify your big file from within VSCode.
I can't really tell. It may result in situations where stack-overflows from infinite recursions could take longer to surface. What I personally don't like about this, is the fact that it's undocumented (at least I couldn't find something in a reasonable time). Moreover, according to this issue, it's only implemented for Unix systems, i.e., not for Windows.

[hmijail]

I just found something remarkable. If I add export COMPlus_DefaultStackSize=100000 to ~/.profile , VSCode picks that up on its next restart from the GUI. No reboot needed, just like that.

VSCode must be doing some magic on its own restart to import environment variables... which is great, because looks like macOS Big Sur 11.4 has no way to permanently add environment variables to the GUI process. The methods that worked in earlier versions seem to be gone now.

[camrein]

Thank you for your follow-up. I am glad that you managed to create a (hopefully) satisfactory solution. Moreover, thank you for sharing it.
How was your experience so far? Did you have any forever Verifying situations thereafter? Otherwise, we could close this issue for the time being.

[hmijail]

Yes, sorry, I didn't think to close it.
I've moved on to other parts of the project, so I have had limited experience with the fix. But for now, seems to work OK.
Thank you!