Karl Palmskog (Dec 09 2021 at 22:04): Karl Palmskog (Dec 09 2021 at 22:04):unfortunately CoqIDE is the only IDE that gets automatic testing in the Coq Platform and so on. Would be useful to add for VsCode, but probably takes quite a bit of CI engineering
Paolo Giarrusso (Dec 09 2021 at 22:05):As a lower-tech fix, anything that needs coqide changes needs vscoq changes
Paolo Giarrusso (Dec 09 2021 at 22:06):This rule could be checked in a checklist or automatically (insert usual SwEng tradeoffs).
Paolo Giarrusso (Dec 09 2021 at 22:07):Of course, that assumes that the protocol changes broke coqide and that ci notices; neither is obvious. Does CI even test using coqide? That's not easy I guess...
Karl Palmskog (Dec 09 2021 at 22:08):yeah, I think at a high level of abstraction the XML protocol is considered legacy/deprecated
Karl Palmskog (Dec 09 2021 at 22:09):we would like to have proper language server, but this going to be WIP for the foreseeable future
Paolo Giarrusso (Dec 09 2021 at 22:14):okay, but doesn't that round that up to "state of the art and fully supported"? I hope it's better supported than the coqtop protocol...
Théo Zimmermann (Dec 10 2021 at 08:40):Karl Palmskog said:
unfortunately CoqIDE is the only IDE that gets automatic testing in the Coq Platform and so on. Would be useful to add for VsCode, but probably takes quite a bit of CI engineering
Not true. Coqtail (which also uses the XML protocol) is also in Coq's CI. And VsCoq has an unreleased branch (the document manager) in it as well.
Karl Palmskog (Dec 10 2021 at 08:45):OK, so some testing in Coq's CI, but not in the Platform CI I think?
Michael Soegtrop (Dec 10 2021 at 09:01):I don't think one can run VSCode on headless CI servers, so how should VsCoq be tested? Also testing UI software is in general a quite involved business, unless you just want to test if it starts at all.
Théo Zimmermann (Dec 10 2021 at 09:05):One could look at what CoqIDE and Coqtail testing look like and try to be on par with them (even if this probably does not mean actual UI testing).
Paolo Giarrusso (Dec 10 2021 at 09:29):of course there’s more, but a head for headless servers is an apt-get install away with xvfb (untested link: http://elementalselenium.com/tips/38-headless)
Michael Soegtrop (Dec 10 2021 at 10:08):I am definitely open for PRs on this, but I don't have the bandwidth for this right now.
Paolo Giarrusso (Dec 10 2021 at 10:33):Until somebody does, maybe just ban changes to the protocol until testing is in place.
Paolo Giarrusso (Dec 10 2021 at 10:34):Including the "backward-compatible" changes that have been attempted — the last one I saw had to be reverted.
Paolo Giarrusso (Dec 10 2021 at 10:40):cognitive bias warning: I'd probably miss any successful changes!
Huỳnh Trần Khanh (Nov 17 2022 at 14:26)::eyes: hello, I made a few changes to VsCoq but I probably can't make more changes unless there are tests. I really need tests to detect issues quickly. I plan to add some headless browser tests. but could I ask... I want to run my tests on CI, would it be ok if I switch the CI to using GitHub Actions?
Karl Palmskog (Nov 17 2022 at 14:31):Sounds reasonable to me, I don't think we can trust Travis much anyway.
Karl Palmskog (Nov 17 2022 at 14:33):I don't think @Maxime Dénès has anything against swapping out Travis for VsCoq CI either?
Maxime Dénès (Nov 17 2022 at 16:03):Adding tests is actually something we do want for VsCoq 2, so adding the necessary infrastructure would be very welcome! Ideally, if we could setup something reasonably standard for testing vscode extensions, it would help reusing it. And of course, I'm in favor of switching from Travis to GitHub Actions.
Karl Palmskog (Nov 17 2022 at 17:09):from another similar discussion: https://github.com/redhat-developer/vscode-extension-tester
Huỳnh Trần Khanh (Nov 18 2022 at 00:46):Also the existing unit tests are broken right? I can't run them. Normally unit tests are very easy to run.
Huỳnh Trần Khanh (Nov 18 2022 at 09:38):Bumping. I just want to make sure my perception is correct. You can just answer "yes" if this is true.
Karl Palmskog (Nov 18 2022 at 09:47):@Huỳnh Trần Khanh yes, please go ahead and switch to GitHub Actions CI for VsCoq. And adding more automated tests is good.
Théo Zimmermann (Nov 18 2022 at 09:50):I think the bump was about unit tests being broken.
Karl Palmskog (Nov 18 2022 at 09:52):OK, then we'll have to ping @Maxime Dénès to check on the "VsCoq unit tests are currently broken" point
Maxime Dénès (Nov 18 2022 at 10:03):It could well be. At this point, as I wrote, our energy is focused on VsCoq 2, and resolving the blockers on the Coq side. So I haven't checked for a while the status of unit tests in the current branch.
Last updated: Jun 04 2023 at 23:30 UTC