Enrico Tassi (Sep 07 2021 at 16:15): 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.
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.
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)"
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: May 28 2023 at 18:29 UTC