Stream: VsCoq devs & users

Topic: Automated testing of VsCoq


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

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 22:05):

As a lower-tech fix, anything that needs coqide changes needs vscoq changes

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 22:06):

This rule could be checked in a checklist or automatically (insert usual SwEng tradeoffs).

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

view this post on Zulip Karl Palmskog (Dec 09 2021 at 22:08):

yeah, I think at a high level of abstraction the XML protocol is considered legacy/deprecated

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

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

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

view this post on Zulip Karl Palmskog (Dec 10 2021 at 08:45):

OK, so some testing in Coq's CI, but not in the Platform CI I think?

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

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

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

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

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 10:33):

Until somebody does, maybe just ban changes to the protocol until testing is in place.

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

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 10:40):

cognitive bias warning: I'd probably miss any successful changes!

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

view this post on Zulip Karl Palmskog (Nov 17 2022 at 14:31):

Sounds reasonable to me, I don't think we can trust Travis much anyway.

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

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

view this post on Zulip Karl Palmskog (Nov 17 2022 at 17:09):

from another similar discussion: https://github.com/redhat-developer/vscode-extension-tester

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

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

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

view this post on Zulip Théo Zimmermann (Nov 18 2022 at 09:50):

I think the bump was about unit tests being broken.

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

view this post on Zulip 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: Jan 30 2023 at 17:03 UTC