Stream: coqbot devs & users

Topic: coqbot comments about allowed-failues


view this post on Zulip Jasper Hugunin (Aug 20 2020 at 18:31):

@Théo Zimmermann I've been finding myself annoyed recently by the repeated coqbot comments on PRs when a CI job in allow failure mode fails. It feels distracting, and I've yet to see it be relevant to the PR commented in. Why is it set up this way?

view this post on Zulip Enrico Tassi (Aug 20 2020 at 18:45):

The plan was to have the piece of info be put in the CI box down, together with all the other CI stuff... but this last improvement did not happen yet.

view this post on Zulip Gaëtan Gilbert (Aug 20 2020 at 18:58):

How would that work? AFAIK we can only put success, failure and ongoing in there and none seem to make sense for allow failure

view this post on Zulip Jasper Hugunin (Aug 20 2020 at 19:03):

Putting the allowed failures in the CI box would make a lot of sense, if it is possible.

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

@Gaëtan Gilbert the "Checks" API is supposedly giving access to more types of results like cancelled, etc. But it is only accessible to GitHub Apps. My intern @Julien Coolen is currently working on making coqbot a proper GitHub App so that we can use this API.

view this post on Zulip Notification Bot (Aug 20 2020 at 20:35):

This topic was moved here from #Coq devs & plugin devs > coqbot comments about allowed-failues by Théo Zimmermann


Last updated: Apr 20 2024 at 00:02 UTC