Gaëtan Gilbert (May 28 2021 at 09:52): Gaëtan Gilbert (May 28 2021 at 09:52):the bot should ignore coq_tools, if minimization is broken it can't minimize itself ;)
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...).
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
Théo Zimmermann (May 28 2021 at 13:17):Yes, that sounds like a good idea.
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: May 28 2023 at 18:29 UTC