Synchronous commands are not interruptible

[tomtomjhj]

Synchronous commands (e.g. CoqGotoDef, CoqStop, ..) cannot be interrupted. This is usually not a problem, but can be frustrating in some cases. For example, if I run CoqToLine to the bottom of a big file and then run CoqGotoDef while CoqToLine is still processing, the UI completely freezes until CoqToLine finishes (which may take very long time).

This is because the synchronous commands use s:evalexpr(), which blocks the UI until the response arrives or the timeout expires (set to 5000ms with chanopts for Vim). The problem of s:evalexpr() is that

1. ch_evalexpr() can't be interrupted by CoqInterrupt and even by <C-c>, and
2. the timeout somehow takes much longer than the specified 5000ms if Coqtail is busy.

I suggest fixing 1 since it subsumes the benefit of fixing 2 and fixing 2 seems to be quite difficult.

The direct solution is:

1. s:evalexpr() should avoid ch_evalexpr() and instead take the polling approach as the nvim compatibility layer does;
2. CoqInterrupt should set a global interrupt flag which is checked in the poll loop.

There are some indirect solutions (PG does something similar to these):

• give higher priority to synchronous commands (+ query commands) by putting them at the front of the reqs queue;
  • this does not fix the issue because to_line handler itself takes long
• do not allow synchronous commands when Coqtail is busy.

Even if we implement the indirect solutions, I think making the commands interruptible is useful in general.

[whonore]

Thanks for the report and the suggestions. I agree this situation should be improved. Your proposed solution seems like it should work and probably shouldn't be too difficult to implement, although it's hard to say with async code like this.

I think another useful improvement would be to let commands that are "read only" like CoqGotoDef, or CoqJumpToEnd, or the query commands execute even while CoqToLine is running. I think this could be done by intercepting these commands in CoqtailHandler.parse_msgs and putting them in a separate queue or executing them immediately, similar to how interrupt is currently handled. This is probably a big enough change that it should go in a separate PR though.

Are you interested in working on either of these changes? I have some time in the next couple weeks, but it's a bit sporadic so it might take a little while for me to implement. But if you're interested I'd be happy to answer questions about the code and discuss possible implementations.

[tomtomjhj]

Hi, I'm a bit busy recently, but I think I can take some time on weekends to implement it.

Regarding immediate processing of read-only commands, I agree that this should be a separate PR. It would also make sense to make CoqtailHandler.handler loop never block with a job queue interface for Coqtop. I guess this might be helpful for full async support, though I haven't thought about it deeply yet.

[tomtomjhj]

Sorry, I have used up this weekend's free time dealing with another irritating vim bug.

[whonore]

That's fine, there's no rush.

[tomtomjhj]

Setting an interrupt flag in CoqInterrupt and checking the flag in the evalexpr loop does not work because vim doesn't process the user input while the script is running. I guess the only way to interrupt the vimscript loop with the user input is the built-in CTRL-C.

[whonore]

Yea that's a lot of why the implementation is so convoluted to begin with. Another possibility is to not worry about making evalexpr interruptible, and instead try to use sendexpr and callbacks as much as possible. Then we might be able to just make everything asynchronous, and if anything still needs to be blocking we could just give it a short timeout.

[tomtomjhj]

Side note: In NeoVim, <C-c> does not interrupt vimscript if it's mapped (https://github.com/neovim/neovim/issues/15258). The correct behavior is to ignore the mapping and interrupt the script (:h map_CTRL-C).

update: fixed in nvim 0.7.1

[whonore]

Interesting, it seems the same is at least supposed to be true in regular Vim, but I've been using <C-c> for interrupt for a while now and it almost always works. But, occasionally I see something strange like Coqtail going out of sync with coqtop, so maybe this explains that.

I guess the default mapping should eventually be changed to something else, but I'll have to think about what that should be. In the meantime I think we can do a sort of soft deprecation by putting a note in the documentation and printing a warning for anyone that isn't already remapping it.