What does it mean when the bot on a PR adds the tag needs full CI?
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.
ok so the full CI is automatically run if there is such tag?
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.
See https://github.com/coq/coq/pull/16600#issuecomment-1268971947 for more context and details.
I should also update the contributing guide to include this info.
@Théo Zimmermann merci!
Laurent Théry has marked this topic as resolved.
@coqbot run full ci without the colon?
The colon is optional.
Laurent Théry has marked this topic as unresolved.
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 ?
this is the script repo the minimizer uses, maybe try to run manually? https://github.com/JasonGross/coq-tools#usage
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.
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.
if you want CI project selection to be safe, that would require quite a lot of dependency tracking (plugins are the hardest)
I don't know what is being the CI but does the CI already does the tracking of these dependencies when
I believe the only tracking of deps CI does is between projects, statically. That affects scheduling, sure.
I am not sure what you mean Karl. Our CI indeed needs to know about the dependencies between projects.
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.
probably the Dune/Duniverse approach would be easiest, but I don't think people will migrate to Dune for a while
oh you wantevery time to rebuild only what is needed. I just wanted to rebuild only what has failed in the previous run.
I think you mean: "only rebuild the projects that failed in last run, and all their dependencies"
unless we are using caching as well?
I got tired to wait for bedrock to build successfully over and over :wink:
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)
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
I think it would be cool specially we seem to have pendings CI runs often
Last updated: Dec 07 2023 at 11:02 UTC