Seems VsCoq and CoqIDE can't do it (see https://github.com/coq/coq/issues/13292 by @Fabian Kunze )
Is there a proper way to terminate coqidetop and proof workers?
If the proof worker is in a loop, it won't notice the pipe is broken.
Coqidetop sends a kill -9 to terminate workers (on unix).
There is still maybe a bug, I don't recall if it kills all workers on abortion (eg the pipe to coqidetop gets broken).
On windows, it may be hard to fix properly. On unix it may be possible by adding an at_exit in stm.ml.
Note that in CoqIDE you have a dedicated panel with the workers, and you can kill them by doubleclick
But (according to the issue) CoqIDE sends SIGKILL to coqidetop, so coqidetop can't send SIGKILL to children
having the IDE send SIGKILL to the children might also work I guess, if they're not leaked?
I guess one should kill the process group, assuming coqidetop sets this right.
My understanding is that most of the time things work because coqidetop dies and the worker gets a sigpipe. But if it is in a busy loop it may never see that.
coqidetop and the worker are connected by a pipie/socket
and signals in ocaml are not triggered "everywhere"
maybe it's not even a sigpipe, it's just a End_of_file while reading from the pipe
so if you never reach that "read"... you never notice master is dead
I mentioned process groups on the issue, but I always found them intimidating
Last updated: Aug 11 2022 at 02:03 UTC