-
Notifications
You must be signed in to change notification settings - Fork 254
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Dafny language server does not clean up z3 child processes #5376
Comments
I can confirm this issue does not occur when using VSCode. |
I'm not sure how neovim kills LSP servers. I tried killing the server with SIGTERM, but this doesn't clean up all of the instances of z3 or dotnet:
I hope this helps, let me know if there is anything else I can do or if I have misunderstood you. |
When I have a |
Dafny version
4.4.0
Code to produce this issue
Command to run and resulting output
For whatever reason, dafny takes a long time to verify this code via z3 (my code is probably pretty terrible). I haven't actually waited around for long enough before to see if z3 terminates. When I run
dafny verify
and send an interrupt signal, dafny will clean up the z3 child process:However, when I open the file in my editor, wait for the language server to start sending some alerts, and then close my editor, there is still an instance of z3 running:
The only other instance of neovim running on my machine was inside a separate tmux session, and it was not running anything dafny-related. I concluded that the language server probably just isn't cleaning up the child z3 process, whereas verify does.
What happened?
I expected that the dafny server would clean up its child processes (although maybe this is a neovim thing?)
What type of operating system are you experiencing the problem on?
Linux
The text was updated successfully, but these errors were encountered: