Hugo Herbelin (May 31 2021 at 17:11): Hugo Herbelin (May 31 2021 at 17:11):Hi vscoq devs, Coq PR#13663 is adding a new attribute in element goal of the XML protocol, corresponding to a new field goal_name to the type `Interface.goal. What should be done at the vscoq side (if any) in such a case? Thanks for help.
Fabian Kunze (Jun 07 2021 at 15:28):A change that just acknowledges the existance of that new field and fixes parsing, without using the name (yet?), probably involves only shifting the array subscript positions in the goal case of the doDeserialize:
https://github.com/coq-community/vscoq/blob/master/server/src/coqtop/xml-protocol/deserialize.base.ts#L436
Hugo Herbelin (Jun 09 2021 at 12:42):Ah, this means that if the field had been the last one, that would have been transparent for vscoq. I can do that if needed.
Matthieu Sozeau (Jun 11 2021 at 10:26):Is there a fix incoming? VSCoq is unusable with master now.
Matthieu Sozeau (Jun 18 2021 at 12:21):@Hugo Herbelin Can you push your fix for master? I've been unable to make much progress this week due to TYPES and this very annoying bug.
Hugo Herbelin (Jun 18 2021 at 13:15):@Matthieu Sozeau : you mean a fix that moves the new field at the end? That would be trivial.
Matthieu Sozeau (Jun 19 2021 at 13:55):Yes, please!
Last updated: Jun 04 2023 at 23:30 UTC