Stream: coqbot devs & users

Topic: Checks


view this post on Zulip Théo Zimmermann (Aug 31 2020 at 15:20):

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.

view this post on Zulip Théo Zimmermann (Aug 31 2020 at 15:21):

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.

view this post on Zulip Théo Zimmermann (Aug 31 2020 at 15:32):

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.

view this post on Zulip Gaëtan Gilbert (Aug 31 2020 at 17:24):

there's still pings for Jason, I suppose that's normal
https://github.com/coq/coq/pull/7825#issuecomment-683916956

view this post on Zulip Théo Zimmermann (Aug 31 2020 at 18:17):

Yep, that's on purpose.

view this post on Zulip Gaëtan Gilbert (Sep 01 2020 at 12:36):

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)?

view this post on Zulip Théo Zimmermann (Sep 01 2020 at 12:44):

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.

view this post on Zulip Gaëtan Gilbert (Sep 01 2020 at 12:56):

Can we put the pipeline / job number in the check message?

view this post on Zulip Théo Zimmermann (Sep 01 2020 at 14:01):

Sure, that would be easy to do.

view this post on Zulip Gaëtan Gilbert (Sep 03 2020 at 15:44):

it looks like checks don't update when a failing job is manually retried then succeeds, this is pretty bad

view this post on Zulip Théo Zimmermann (Sep 03 2020 at 15:56):

OK, I'll try to figure this out quickly and otherwise we'll revert this change temporarily.

view this post on Zulip Théo Zimmermann (Sep 03 2020 at 19:29):

@Gaëtan Gilbert This issue should be fixed now. Let me know if you see any new instances.

view this post on Zulip Jason Gross (Sep 07 2020 at 02:23):

@Théo Zimmermann Can you still have coqbot tag me when fiat-crypto legacy fails (assuming the base job does not)?

view this post on Zulip Théo Zimmermann (Sep 07 2020 at 07:41):

@Jason Gross It's supposed to still be the case. Have you had an occurrence where it should have happened but did not?

view this post on Zulip Jason Gross (Sep 07 2020 at 10:51):

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