Paolo Giarrusso (Nov 02 2020 at 19:24): Paolo Giarrusso (Nov 02 2020 at 19:24):Seems VsCoq and CoqIDE can't do it (see https://github.com/coq/coq/issues/13292 by @Fabian Kunze )
Paolo Giarrusso (Nov 02 2020 at 19:58):Is there a proper way to terminate coqidetop and proof workers?
Enrico Tassi (Nov 03 2020 at 08:21):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).
Enrico Tassi (Nov 03 2020 at 08:22):On windows, it may be hard to fix properly. On unix it may be possible by adding an at_exit in stm.ml.
Enrico Tassi (Nov 03 2020 at 08:23):Note that in CoqIDE you have a dedicated panel with the workers, and you can kill them by doubleclick
Paolo Giarrusso (Nov 03 2020 at 09:30):But (according to the issue) CoqIDE sends SIGKILL to coqidetop, so coqidetop can't send SIGKILL to children
Paolo Giarrusso (Nov 03 2020 at 09:36):having the IDE send SIGKILL to the children might also work I guess, if they're not leaked?
Enrico Tassi (Nov 03 2020 at 09:39):I guess one should kill the process group, assuming coqidetop sets this right.
Enrico Tassi (Nov 03 2020 at 09:40):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.
Enrico Tassi (Nov 03 2020 at 09:41):coqidetop and the worker are connected by a pipie/socket
Enrico Tassi (Nov 03 2020 at 09:41):and signals in ocaml are not triggered "everywhere"
Enrico Tassi (Nov 03 2020 at 09:42):maybe it's not even a sigpipe, it's just a End_of_file while reading from the pipe
Enrico Tassi (Nov 03 2020 at 09:43):so if you never reach that "read"... you never notice master is dead
Paolo Giarrusso (Nov 03 2020 at 09:45):I mentioned process groups on the issue, but I always found them intimidating
Last updated: Oct 13 2024 at 01:02 UTC