whonore / Coqtail

Interactive Coq Proofs in Vim
MIT License
274 stars 35 forks source link

Fix NeoVim Deadlock #361

Closed whonore closed 3 months ago

whonore commented 3 months ago

Calling :CoqJumpToEnd before :CoqStart results in a deadlock on NeoVim. The sequence of events is:

  1. Since !s:running(), :CoqJumpToEnd calls coqtail#start with coqtail#jumpto("endpoint") as a callback.
  2. coqtail#start calls s:call, which calls s:sendexpr and registers coqtail#after_startCB as its callback.
  3. s:chanrecv receives the reply and executes coqtail#after_startCB.
  4. coqtail#after_startCB executes coqtail#jumpto, which calls s:call, which calls s:evalexpr.
  5. s:evalexpr blocks while waiting for a reply, but s:chanrecv is also blocked waiting for coqtail#after_startCB to return.

Commands like :CoqNext don't have this problem because they execute asynchronously, so coqtail#after_startCB calls s:sendexpr instead of s:evalexpr. It also works fine on Vim because it uses the builtin ch_evalexpr, which handles other messages while waiting for a reply.

The ideal solution would be to somehow execute callbacks asynchronously, but I couldn't figure out a way of doing that in vimscript. Perhaps it's possible with Lua. In any case, I realized that the only synchronous commands that could be called before :CoqStart are :CoqJumpToEnd, :CoqJumpToError, and :CoqGotoDef, so I just have these cases busy wait for coqtail#start to complete instead of using callbacks.

Fixes #360.

TairanLee commented 3 months ago

Checked on v0.9.5 and v0.10.0, both work fine now. Thanks a lot !