Jason Gross (May 21 2021 at 18:41): Jason Gross (May 21 2021 at 18:41):Is it deliberate that in-progress checks seem to not be reported? (The ci minimization routine is not finding in-progress pipeline checks.)
Jason Gross (May 21 2021 at 19:00):Hm, seems deliberate. @Théo Zimmermann do you think that a non-completed overall pipeline should be a fatal error for the minimizer? Or should to bot proceed with whatever pipelines are available?
Théo Zimmermann (May 22 2021 at 12:25):Yes, this is deliberate. The reason is that if the pipeline is not completed, then we have no evidence that the test-suite jobs do not fail.
Théo Zimmermann (May 22 2021 at 12:25):That being said, we could decide to bypass that whenever the minimization is explicitly requested by the user.
Théo Zimmermann (May 22 2021 at 12:25):OTOH, we could also fear that's the most common scenario in this case would be that the user is requesting a minimization for the previous run but has force-pushed a new version in the meantime...
Jason Gross (May 26 2021 at 12:23):I think we should allow the pipeline check to be incomplete when explicit requests are passed, as in https://github.com/coq/coq/pull/13969#issuecomment-848719499
Théo Zimmermann (May 26 2021 at 12:48):OK, feel free to change that.
Théo Zimmermann (May 27 2021 at 07:32):It's confusing to read both "I checked that the corresponding jobs for the base commit ac9a310 succeeded." and "However, you may want to wait until the pipeline for the base commit (ac9a310) finishes."
What does coqbot now check exactly?
Théo Zimmermann (May 27 2021 at 07:34):BTW, here is a good example where running the auto-minimization would be pretty pointless (when restricting a feature / breaking compatibility on purpose): https://github.com/coq/coq/pull/14395/checks?check_run_id=2678566745
Jason Gross (May 27 2021 at 20:23):The technically accurate thing is "I checked that there was no corresponding job that failed at the base commit" It does not suggest jobs which have a corresponding failing job. There's no way to distinguish "the job at the base commit succeeded" from "the job at the base commit never ran", AFAIK. The second message is about the overall pipeline job, and gets emitted if it's in progress (or if it never ran because "activity limit exceeded").
Théo Zimmermann (May 28 2021 at 07:57):Indeed, no way using the GitHub Checks, although if we really want, we could call the GitLab API to get this info.
Last updated: May 28 2023 at 18:29 UTC