Stream: coqbot devs & users

Topic: in progress checks are not found?


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

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

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

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

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

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

view this post on Zulip Théo Zimmermann (May 26 2021 at 12:48):

OK, feel free to change that.

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

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

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

view this post on Zulip 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: Jan 31 2023 at 09:01 UTC