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
- (I tried to call
job_status()here, which checks the running/dead status of a job, but since the job probably only managed to
forkand not yet
execv, it still appears fine.)
- The initialisation script continues, reaching the point where an “About” call is made to the
- (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
coqidetop, which I do not have.
- The job exits, calling the callback which in turn launches a job with the older
coqtopjob 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 reaches
coqtop, 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