Open mitchellholt opened 4 months ago
I can confirm this issue does not occur when using VSCode. dafny server
has code to kill z3
processes when it exits, but I'm not sure if this only runs when you shutdown the language server through its shutdown and exit APIs, or also when you send a sigterm. Do you know how neovim kills its LSP servers? Maybe you could do a little experiment with killing the LSP server yourself to see if it then cleans up the Z3 processes. If you can confirm there's a Dafny LSP server issue that would help prioritize this.
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:
$ ps -ef | grep dafny
mitchell 534157 505209 0 08:44 pts/3 00:00:00 grep --color=auto dafny
--- Open oops.dfy in neovim in a different tmux pane ---
$ ps -ef | grep dafny
mitchell 537144 537140 0 08:48 ? 00:00:00 bash /home/mitchell/bin/dafny server
mitchell 537152 537144 44 08:48 ? 00:00:03 /usr/bin/dotnet /home/mitchell/Documents/CSSE3100/dafny/Scripts/../Binaries/Dafny.dll server
mitchell 537238 537152 79 08:48 ? 00:00:03 /home/mitchell/Documents/CSSE3100/dafny/Binaries/z3/bin/z3-4.12.1 -smt2 -in
mitchell 537239 537152 0 08:49 ? 00:00:00 /home/mitchell/Documents/CSSE3100/dafny/Binaries/z3/bin/z3-4.12.1 -smt2 -in
mitchell 537288 536871 0 08:49 pts/4 00:00:00 grep --color=auto dafny
$ kill -SIGTERM 537144
$ ps -ef | grep dafny
mitchell 537152 1444 7 08:48 ? 00:00:03 /usr/bin/dotnet /home/mitchell/Documents/CSSE3100/dafny/Scripts/../Binaries/Dafny.dll server
mitchell 537238 537152 97 08:48 ? 00:00:43 /home/mitchell/Documents/CSSE3100/dafny/Binaries/z3/bin/z3-4.12.1 -smt2 -in
mitchell 537239 537152 0 08:49 ? 00:00:00 /home/mitchell/Documents/CSSE3100/dafny/Binaries/z3/bin/z3-4.12.1 -smt2 -in
mitchell 537663 536871 0 08:49 pts/4 00:00:00 grep --color=auto dafny
I hope this helps, let me know if there is anything else I can do or if I have misunderstood you.
but this doesn't clean up all of the instances of z3 or dotnet
When I have a dafny server
process and I kill it with SIGTERM, I see that it and the Z3 processes under it terminate. I'm not sure what you mean by the dotnet
instances are not cleaned up. Isn't that the process you're terminating? What process is being terminated by your SIGTERM then?
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