Laurent Théry (Jan 04 2023 at 09:53): 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?
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.
Laurent Théry (Jan 04 2023 at 09:57):ok so the full CI is automatically run if there is such tag?
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.
Théo Zimmermann (Jan 04 2023 at 09:59):See https://github.com/coq/coq/pull/16600#issuecomment-1268971947 for more context and details.
Théo Zimmermann (Jan 04 2023 at 10:00):I should also update the contributing guide to include this info.
Laurent Théry (Jan 04 2023 at 10:00):@Théo Zimmermann merci!
Notification Bot (Jan 04 2023 at 10:00):Laurent Théry has marked this topic as resolved.
Ali Caglayan (Jan 04 2023 at 14:58):Isn't it @coqbot run full ci without the colon?
Théo Zimmermann (Jan 04 2023 at 16:09):The colon is optional.
Notification Bot (Jan 04 2023 at 16:50):Laurent Théry has marked this topic as unresolved.
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 ?
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
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.
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.
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)
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?
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.
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.
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.
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
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.
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"
Karl Palmskog (Jan 05 2023 at 09:25):unless we are using caching as well?
Laurent Théry (Jan 05 2023 at 09:28):I got tired to wait for bedrock to build successfully over and over :wink:
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)
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
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: Dec 07 2023 at 11:02 UTC