Parsing issues with MetaCoq

[thomas-lamiaux]

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]

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]

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

[terencode]

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

vscoq 2.2.1, coq 8.19.2

[thomas-lamiaux]

see https://coq.zulipchat.com/#narrow/channel/237662-VsCoq-devs-.26-users/topic/VsCoq.20randomly.20crashes.20when.20opening.20a.20file/near/481334265 for a minimal example.
Basically it happens as soon as there is a file doing

From MetaCoq Require Import Template.All

[SkySkimmer]

can you try with coq/coq#19864 ?

[SkySkimmer]

This looks like a metacoq issue, they do something with an option which can modify another option
https://github.com/MetaCoq/metacoq/blob/65aa1112dc73b853e5e55b77be12aaed7c6bce15/template-coq/src/tm_util.ml#L18-L54
this is not really supported by the API

[SkySkimmer]

It doesn't even work, set_option_value ~stage:Interp (fun _ v -> v) key i sets the option to the current value
ie Set MetaCoq Template Monad Debug. does nothing

[gares]

Thanks for investigating @SkySkimmer . Should we open an issue in metacoq?

[SkySkimmer]

MetaCoq/metacoq#1123