Pierre-Marie Pédrot (Feb 15 2022 at 22:34): Pierre-Marie Pédrot (Feb 15 2022 at 22:34):it will probably break the "true" vscoq also, won't it?
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)
Ali Caglayan (Feb 15 2022 at 22:40):Right I also wondered this
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
Pierre-Marie Pédrot (Feb 15 2022 at 22:42):(not sure the real vscoq actually uses this stuff)
Ali Caglayan (Feb 15 2022 at 22:44):Do you know if VSCoq is version independent?
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?
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
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
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
Ali Caglayan (Feb 15 2022 at 23:02):Looks like they are relying solely on the xml protocol
Ali Caglayan (Feb 15 2022 at 23:02):All of it is written in typescript
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
Paolo Giarrusso (Feb 16 2022 at 08:33):This isn't https://github.com/coq/coq/issues/15687 right?
Ali Caglayan (Feb 16 2022 at 08:42):Whoops yesterday's clipboard issues.
Last updated: Oct 12 2024 at 13:01 UTC