Stream: User interfaces devs & users

Topic: Killing stuck Coq proof worker


view this post on Zulip 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 )

view this post on Zulip Paolo Giarrusso (Nov 02 2020 at 19:58):

Is there a proper way to terminate coqidetop and proof workers?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Nov 03 2020 at 09:39):

I guess one should kill the process group, assuming coqidetop sets this right.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Nov 03 2020 at 09:41):

coqidetop and the worker are connected by a pipie/socket

view this post on Zulip Enrico Tassi (Nov 03 2020 at 09:41):

and signals in ocaml are not triggered "everywhere"

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 03 2020 at 09:43):

so if you never reach that "read"... you never notice master is dead

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 09:45):

I mentioned process groups on the issue, but I always found them intimidating


Last updated: Aug 11 2022 at 02:03 UTC