the-lambda-church / coquille

Interactive theorem proving with Coq in vim.
ISC License
186 stars 68 forks source link

Decode the input before building XML commands. #57

Open xunam opened 7 years ago

xunam commented 7 years ago

As spotted in issue #53, Coquille chokes on non-ASCII input because of encoding problems and Python throwing UnicodeDecodeError exceptions. This is a simple fix for the issue, it consists in

My first tests work fine but it surely deserves to be checked.

dadoomer commented 7 years ago

Indeed, this seems to solve the problem for me.

dustnnbones commented 1 year ago

@xunam do you have an example of how you fixed the issue?

xunam commented 1 year ago

Hi, I'm not sure what you mean by "example" here, but if I remember well, I fixed the issue by patching the code as in the present PR, which has no conflict according to Github. But it seems that this repository has been unmaintained for 6 years now.

Actually, I ended up writing my own Coq plugin from scratch to support later versions of Coq instead of forking coquille, because the way Coq interacts has changed completely : https://framagit.org/manu/coq-au-vim It has a few open issues but it works reasonably well for me. Feel free to try it !