the bot should ignore coq_tools, if minimization is broken it can't minimize itself ;)
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...).
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
Yes, that sounds like a good idea.
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