Coqtail: Seeing Coqtop error messages

Since this seems to be a pretty uncommon edge case and possibly due to a Vim bug, I’ll close it as wontfix for now. If more people run into this problem then I’ll revisit it.

Cool, I’m able to reproduce it now. :CoqStart fails on a tracked file with a huge diff but succeeds on an untracked file with the same content. I’ll try to dig into the log some more and see what’s going on.

The handler (start in this case) returns None when there are no errors. This gets bundled in a dictionary, converted to JSON and written to the socket with wfile.write, which then gets received by Vim and decoded back into a dictionary. So the only way I can see the Vim side getting a string instead is if something goes wrong with ch_evalexpr and it returns an empty string by default or something like that.

You can use string() to convert dictionaries into strings that can be :echomed.