Stream: Coq devs & plugin devs

Topic: pr #15645 https://github.com/coq/coq/pull/15645


view this post on Zulip Pierre-Marie Pédrot (Feb 15 2022 at 22:34):

it will probably break the "true" vscoq also, won't it?

view this post on Zulip Pierre-Marie Pédrot (Feb 15 2022 at 22:34):

(the one we have in CI is just testing a curated set of random and half-borken APIs, not sure why we keep it)

view this post on Zulip Ali Caglayan (Feb 15 2022 at 22:40):

Right I also wondered this

view this post on Zulip Pierre-Marie Pédrot (Feb 15 2022 at 22:41):

you should probably ping them in the PR to check whether there will be a problem

view this post on Zulip Pierre-Marie Pédrot (Feb 15 2022 at 22:42):

(not sure the real vscoq actually uses this stuff)

view this post on Zulip Ali Caglayan (Feb 15 2022 at 22:44):

Do you know if VSCoq is version independent?

view this post on Zulip Ali Caglayan (Feb 15 2022 at 22:45):

If its tied to the coq version, then the full thing should really be in CI no?

view this post on Zulip Pierre-Marie Pédrot (Feb 15 2022 at 22:46):

AFAIR there is a little shim atop of the XML protocol, and vscoq just relies on that

view this post on Zulip Pierre-Marie Pédrot (Feb 15 2022 at 22:46):

the one thing I'm sure about is that when the XML protocol changes it breaks vscoq

view this post on Zulip Pierre-Marie Pédrot (Feb 15 2022 at 22:47):

the thing I don't know is the language the shim is written in and if it relies on some OCaml code from the coq implem

view this post on Zulip Ali Caglayan (Feb 15 2022 at 23:02):

Looks like they are relying solely on the xml protocol

view this post on Zulip Ali Caglayan (Feb 15 2022 at 23:02):

All of it is written in typescript

view this post on Zulip Ali Caglayan (Feb 15 2022 at 23:03):

Since I didn't change the protocol I think this will be fine to merge, but let's give the devs till tomorrow to respond

view this post on Zulip Paolo Giarrusso (Feb 16 2022 at 08:33):

This isn't https://github.com/coq/coq/issues/15687 right?

view this post on Zulip Ali Caglayan (Feb 16 2022 at 08:42):

Whoops yesterday's clipboard issues.


Last updated: Feb 06 2023 at 19:03 UTC