Stream: coqbot devs & users

Topic: When the tested project is broken independently from the PR

view this post on Zulip Gaëtan Gilbert (May 28 2021 at 09:52):

the bot should ignore coq_tools, if minimization is broken it can't minimize itself ;)

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

It's annoying that when a project gets broken externally, it will start spamming every PR. Any idea how we could avoid that (and on the contrary post comments saying: this is not just you, this is broken on many other PRs right now...).

view this post on Zulip Jason Gross (May 28 2021 at 13:01):

The breakage in coq-tools does not impact the minimizer (this time), I just need to update the expected output in accordance with a tweak I made, sorry.

I think the first thing we should do is report some sort of checksum (ideally just a git commit hash) of the version of the CI target in the checks tab. I guess actually to get this right we need to update the overall pipeline status tab to report for each job the success/failure as well as the version identifier. Then we can report when the head version is different from the base version

view this post on Zulip Théo Zimmermann (May 28 2021 at 13:17):

Yes, that sounds like a good idea.

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

In fact, while your idea is a good first step to alleviate this issue, it gave me the idea that we could use this information to always test PRs with the same commit that was used to test the base commit. This would ensure that no independent breakage can affect PR testing (except when the breakage has already affected master but in this case, the bot could report that the breakage already happens on master and it's up to the PR authors / reviewers to decide whether to ignore it or to wait until it is fixed).

Last updated: Sep 25 2023 at 12:01 UTC