Hi @Théo Zimmermann, could you deploy the latest bench PR?
In progress at: https://github.com/Zimmi48/bot/runs/5626693355?check_suite_focus=true
I think testing this, we definitely need some sort of feedback from coqbot when doing
@coqbot bench. Even a comment that just says "bench started at url` would be good. That would also allow us to easily record feedback from errors.
So I did
@coqbot bench and nothing happened so time to dig through the logs.
As we discussed today, the feedback can also be in terms of a "check run" (we don't put one for running and passing jobs by default, but we could do it for the bench).
The issue was the exact same as the one before but for the project ID instead of the job ID. I have fixed that regex too and pushed.
@Théo Zimmermann coqbot just posted this: https://github.com/coq/coq/pull/14748#issuecomment-1073940021 was that intended?
Hum, that's because when you canceled the bench, the GitLab pipeline finished and thus coqbot did its usual job of checking for minimization suggestions.
So it is not related to the new feature, it's a more generic issue of the minimization suggestion that it should strive not to repeat itself.
I've added a check now for membership in the pushers team
I am deploying the branch now https://github.com/Alizter/bot/actions/runs/2017774931
In https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Security.20of.20bench, we said using the contributors team would be fine. Limiting to the pushers team seems a bit restrictive, compared to who has access to the GitLab organization.
@Théo Zimmermann Here is something curious. https://github.com/coq/coq/pull/15889 Coqbot doesn't know what to do when the GitLab pipeline hasn't started yet, but a fetch check was requested. Clearly It was not "more than one checksuite" but "not one checksuite".
Probably the error handling is too conflated (several cases that should lead to several error messages).
That's in get_base_and_head_checks so I guess the best thing todo is wait for the eventual get_head_checks to properly handle that.
Add to that retrying after some time when failing
Last updated: May 28 2023 at 18:29 UTC