search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

Parsing issues with MetaCoq #892

Open thomas-lamiaux opened 1 month ago

thomas-lamiaux commented 1 month ago

At the moment, basically all the files in https://github.com/thomas-lamiaux/generating_recursors creates parsing issue. I can not exactly isolate a file as it happens from time to time when I open files.

You can check out the issue by cloning the repo, doing make, and trying to check the files in the folder recursors_api.

I am using coq 8.19.2, the associated version of Equations and MetaCoq and vscoq 2.1.7.

terencode commented 2 weeks ago

Not sure if it is the same, but for my project, the parsing is messed up almost each time I edit something containing utf8 characters like 𝓘 or 𝒯. The only fix is to reopen vscode, which gets annoying very quickly.

gares commented 2 weeks ago

@terencode can you please tell us which version are you on?

terencode commented 2 weeks ago

@terencode can you please tell us which version are you on?

vscoq 2.2.1, coq 8.19.2