Scroll + CoqToCursor kills+hangs Coquille if previous head is offscreen
Environment
- Coq version: 8.10.2
- Neovim version:
v0.5.0-nightly-355-g4139678f9
(edit: also repros with the default v0.4.3 build from Homebrew) - Coquille commit (run
git log -1
in coquille's directory if unsure):81cea3080
- I have run
:UpdateRemotePlugins
in neovim but it didn't help: yep
Description
If you go bit by bit through a file, comment by comment, proof by proof, then you can check all of it. However, you generally want to do large swaths at a time, to catch up. Coquille cannot do this at the moment. It can't do large leaps; it silently fails, stops accepting commands, and then hangs on exit.
Steps to Reproduce
- Find a long .v file. nahas_tutorial.v works for this. Observe you can check a few lines at a time.
- Scroll down. Takes about a screenful and a half for me.
- CoqToCursor
- Nothing happens
- Go back to the end of the checked part to try a smaller region
- Observe that you can no longer interact with Coquille at all
- Attempt to start fresh:
call CoqStop()
hangs. So does exiting the buffer, due to the autocommand. - Kill the neovim process externally, because it is no longer accepting input.
((8) shouldn't really ever be a problem with a python plugin -- pynvim has perfectly good facilities for asynchronous functions that don't block the entire editor even if the downstream program is blocking, which coqtop appears to be doing a lot recently.)
Debug Output (Optional)
Unable to get CoqDebug output because it also hangs.
Edited by Cache Cache