Stream: coqbot devs & users

Topic: verbosity


view this post on Zulip Enrico Tassi (Sep 07 2021 at 16:15):

what about @coqbot help to get some help, including the instructions to minimize failed jobs? 99% of the times, one does not want to see these, since CI fails for all sorts of reasons.

view this post on Zulip Théo Zimmermann (Sep 07 2021 at 19:13):

We definitely need to work at lowering the verbosity. However, I don't think that we want to hide the auto-minimization feature either. Furthermore, these messages are sometimes useful to learn that a failure is not specific to the PR because it is also failing in master.

view this post on Zulip Gaëtan Gilbert (Sep 07 2021 at 19:17):

maybe we could put a neutral check "minimization available"

Furthermore, these messages are sometimes useful to learn that a failure is not specific to the PR because it is also failing in master.

that could go in the github check page for the job, ie in https://github.com/coq/coq/pull/14854/checks?check_run_id=3534300287 we could have a message "this also failed on master ($current master commit, link to job)"

view this post on Zulip Théo Zimmermann (Sep 07 2021 at 20:23):

Hum, why not? That's interesting, but would require reworking how things are done.


Last updated: Jan 29 2023 at 14:02 UTC