Stream: VsCoq devs & users

Topic: Change in XML protocol


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Jun 11 2021 at 10:26):

Is there a fix incoming? VSCoq is unusable with master now.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Jun 19 2021 at 13:55):

Yes, please!


Last updated: Jan 30 2023 at 18:04 UTC