Initialisation hangs when using coqtop
There is a race condition when launching a Coq toplevel during :CoqStart
. It manifests probably only with older Coq, i.e. when coqtop
(v. 8.6) is needed instead of coqidetop
(v. 8.9). I suspect it happens like this:
- A job with
coqidetop
is created. - (I tried to call
job_status()
here, which checks the running/dead status of a job, but since the job probably only managed tofork
and not yetexecv
, it still appears fine.) - The initialisation script continues, reaching the point where an “About” call is made to the
coqidetop
job. - (Sometimes, with debug options set, it fails here, as the channel being written to is already closed, but more often this does not happen on my machine.)
- The call's XML is written to the channel, which still appears fine.
- The job finally gets to
execv
coqidetop
, which I do not have. - The job exits, calling the callback which in turn launches a job with the older
coqtop
. - The
coqtop
job starts correctly, but the “About” call is trapped in the first job's channel (or perhaps even consumed and buffered by the now-dead job, I am not sure if that is possible). As it never reachescoqtop
, the script never receives a response and the initialisation does not continue.
I spent several hours trying to fix this issue in an elegant way, but to no avail. For now, I just wait 100ms after the first job is launched, which is of course a dirty work-around and not at all an actual solution. Using the same channel for both jobs might be worth looking into, although I do not know, whether the first job would not consume any input before exiting. Another variant might be checking whether coqidetop
exists beforehand and launching the correct toplevel right away.
Introduced by: 1ff3c89b