Comments (3)
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.
from dafny.
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.
from dafny.
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?
from dafny.
Related Issues (20)
- Issue with multi-backend-testing
- Verification hang apparently caused by Std import HOT 3
- Costless by clause in `assert .. by { }` when using --isolate-assertions HOT 3
- Unstable CLI test `git-issues/git-issue-697j.dfy`, related to Rust backend HOT 5
- can't label forall-ensuring statement
- can't label assumptions
- textDocument/codeAction failed
- Named ensure clause
- Flaky test: DafnyTestGeneration HOT 3
- Flaky test Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization.ProjectManagerDatabaseTest.ChangeAndUndoProjectWithMultipleFile HOT 1
- Flaky test: Unspecified
- JavaScript and Go backend: Incorrect map cardinality HOT 1
- Helpers.unsignedLongToBigInteger removed from Java runtime
- C# backend: Multiset size overflow
- Dafny generated code not necessarily backwards compatible with code generated by older Dafny versions HOT 4
- Potential enhancement: array initialisation that is incompatible with declared size
- C#Β and Go Backends: Incorrect finite map semantics HOT 1
- Make the Rust compiler run on nightly once it passes all tests
- Dafny-to-Rust code generator
- [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-cryptographic-material-providers-library HOT 15
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
π Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. πππ
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google β€οΈ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from dafny.