In a few minutes, coqbot is going to start reporting results of GitLab CI in the Checks tab on GitHub. In the beginning, all it will change is that allow failure jobs will stop being reported as comments, but we can add more features to it later (last X lines of trace, button to restart a job directly from GitHub, code annotations). Do not hesitate to provide feedback and ideas.
Note for the users of coqbot other than the Coq and opam-coq-archive repositories: this requires using the new "installation as a GitHub App" method documented in the README.
Note that it seems that Checks do not overwrite existing statuses so there might be some spurious red or pending statuses for a while during the transition.
there's still pings for Jason, I suppose that's normal
Yep, that's on purpose.
is there a way to get straight from the checks at the bottom of the comment list to the job log (without passing through the check tab)?
Unfortunately no, that's not something that GitHub allows us to configure. I am aware that for now this looks like a regression (one more link to click) but if we start really using the features that the Checks tab provides (showing trace extracts, providing a retry button...) I guess that we will really win by having to go to the GitLab page much less frequently.
Can we put the pipeline / job number in the check message?
Sure, that would be easy to do.
it looks like checks don't update when a failing job is manually retried then succeeds, this is pretty bad
OK, I'll try to figure this out quickly and otherwise we'll revert this change temporarily.
@Gaëtan Gilbert This issue should be fixed now. Let me know if you see any new instances.
@Théo Zimmermann Can you still have coqbot tag me when fiat-crypto legacy fails (assuming the base job does not)?
@Jason Gross It's supposed to still be the case. Have you had an occurrence where it should have happened but did not?
Ah, great, I was just preemptively replying to the transition to describing allowed failures in the checks tab, and somehow missed the comments about there still being pings for me. Sorry for the noise
Last updated: Jan 31 2023 at 10:01 UTC