Stream: Coq devs & plugin devs

Topic: Coq-Ci needs full CI


view this post on Zulip Laurent Théry (Jan 04 2023 at 09:53):

What does it mean when the bot on a PR adds the tag needs full CI?

view this post on Zulip Théo Zimmermann (Jan 04 2023 at 09:56):

It does this for all the PRs. The point is that the full CI (including all tested external projects) is not run anymore by default when opening or pushing to a PR, so this label is a reminder that this full CI should be run before merging the PR.

view this post on Zulip Laurent Théry (Jan 04 2023 at 09:57):

ok so the full CI is automatically run if there is such tag?

view this post on Zulip Théo Zimmermann (Jan 04 2023 at 09:59):

There is a tag that can be used before pushing, but most often it is triggered by writing "@coqbot: run full CI" in the PR.

view this post on Zulip Théo Zimmermann (Jan 04 2023 at 09:59):

See https://github.com/coq/coq/pull/16600#issuecomment-1268971947 for more context and details.

view this post on Zulip Théo Zimmermann (Jan 04 2023 at 10:00):

I should also update the contributing guide to include this info.

view this post on Zulip Laurent Théry (Jan 04 2023 at 10:00):

@Théo Zimmermann merci!

view this post on Zulip Notification Bot (Jan 04 2023 at 10:00):

Laurent Théry has marked this topic as resolved.

view this post on Zulip Ali Caglayan (Jan 04 2023 at 14:58):

Isn't it @coqbot run full ci without the colon?

view this post on Zulip Théo Zimmermann (Jan 04 2023 at 16:09):

The colon is optional.

view this post on Zulip Notification Bot (Jan 04 2023 at 16:50):

Laurent Théry has marked this topic as unresolved.

view this post on Zulip Laurent Théry (Jan 04 2023 at 16:54):

full CI is taking lots of time, coqbot suggests me to minimize here, but it didn't work about a story of process, where can I find some doc on how to do this minimization ?

view this post on Zulip Karl Palmskog (Jan 05 2023 at 08:02):

this is the script repo the minimizer uses, maybe try to run manually? https://github.com/JasonGross/coq-tools#usage

view this post on Zulip Laurent Théry (Jan 05 2023 at 08:37):

ok I misunderstood the minimize usage, The full CI of coq takes a lots of time. I had a PR that was breaking only a couple of external stuffs. I was hopng that minimize will set to the CI to only those that are broken. Then, when these are fixed, I could go back to full CI.

view this post on Zulip Théo Zimmermann (Jan 05 2023 at 08:57):

No, indeed, we do not yet have support for reducing the full CI to a selection of external projects, but that would indeed be useful to add. Minimization is about extracting a reduced test case to reproduce a breakage.

view this post on Zulip Karl Palmskog (Jan 05 2023 at 09:04):

if you want CI project selection to be safe, that would require quite a lot of dependency tracking (plugins are the hardest)

view this post on Zulip Laurent Théry (Jan 05 2023 at 09:08):

I don't know what is being the CI but does the CI already does the tracking of these dependencies when
scheduling?

view this post on Zulip Karl Palmskog (Jan 05 2023 at 09:09):

I believe the only tracking of deps CI does is between projects, statically. That affects scheduling, sure.

view this post on Zulip Théo Zimmermann (Jan 05 2023 at 09:17):

I am not sure what you mean Karl. Our CI indeed needs to know about the dependencies between projects.

view this post on Zulip Karl Palmskog (Jan 05 2023 at 09:18):

what I mean is that if you want to save meaningful time by selecting certain projects to check based on changes to Coq, you don't get far by just having inter-CI-project dependencies. You need to know at Coq/ML level what files they depend on, etc.

view this post on Zulip Karl Palmskog (Jan 05 2023 at 09:19):

probably the Dune/Duniverse approach would be easiest, but I don't think people will migrate to Dune for a while

view this post on Zulip Laurent Théry (Jan 05 2023 at 09:22):

oh you wantevery time to rebuild only what is needed. I just wanted to rebuild only what has failed in the previous run.

view this post on Zulip Karl Palmskog (Jan 05 2023 at 09:25):

I think you mean: "only rebuild the projects that failed in last run, and all their dependencies"

view this post on Zulip Karl Palmskog (Jan 05 2023 at 09:25):

unless we are using caching as well?

view this post on Zulip Laurent Théry (Jan 05 2023 at 09:28):

I got tired to wait for bedrock to build successfully over and over :wink:

view this post on Zulip Karl Palmskog (Jan 05 2023 at 09:31):

implementing purely error based selection in CI for Coq is probably a good idea to save CI minutes and dev time. Could be a good idea to write an issue about it (possible student internship task)

view this post on Zulip Karl Palmskog (Jan 05 2023 at 09:32):

of course, we'd be assuming no flaky CI runs (fail and pass on the same Coq revision), which is probably not true in general

view this post on Zulip Laurent Théry (Jan 05 2023 at 09:38):

I think it would be cool specially we seem to have pendings CI runs often


Last updated: Jul 13 2024 at 04:02 UTC