it will probably break the "true" vscoq also, won't it?
(the one we have in CI is just testing a curated set of random and half-borken APIs, not sure why we keep it)
Right I also wondered this
you should probably ping them in the PR to check whether there will be a problem
(not sure the real vscoq actually uses this stuff)
Do you know if VSCoq is version independent?
If its tied to the coq version, then the full thing should really be in CI no?
AFAIR there is a little shim atop of the XML protocol, and vscoq just relies on that
the one thing I'm sure about is that when the XML protocol changes it breaks vscoq
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
Looks like they are relying solely on the xml protocol
All of it is written in typescript
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
This isn't https://github.com/coq/coq/issues/15687 right?
Whoops yesterday's clipboard issues.
Last updated: Feb 06 2023 at 19:03 UTC