Stream: coqbot devs & users

Topic: bench command

Ali Caglayan (Mar 21 2022 at 11:20):

Hi @Théo Zimmermann, could you deploy the latest bench PR?

Théo Zimmermann (Mar 21 2022 at 12:06):

In progress at: https://github.com/Zimmi48/bot/runs/5626693355?check_suite_focus=true

Ali Caglayan (Mar 21 2022 at 12:19):

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.

Ali Caglayan (Mar 21 2022 at 12:19):

So I did @coqbot bench and nothing happened so time to dig through the logs.

Ali Caglayan (Mar 21 2022 at 12:19):

https://github.com/coq/coq/pull/14748

Théo Zimmermann (Mar 21 2022 at 13:14):

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

Ali Caglayan (Mar 21 2022 at 13:21):

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.

Ali Caglayan (Mar 21 2022 at 14:15):

@Théo Zimmermann coqbot just posted this: https://github.com/coq/coq/pull/14748#issuecomment-1073940021 was that intended?

Théo Zimmermann (Mar 21 2022 at 14:21):

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.

Théo Zimmermann (Mar 21 2022 at 14:21):

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.

Ali Caglayan (Mar 21 2022 at 17:20):

I've added a check now for membership in the pushers team

Ali Caglayan (Mar 21 2022 at 18:05):

I am deploying the branch now https://github.com/Alizter/bot/actions/runs/2017774931

Théo Zimmermann (Mar 22 2022 at 08:26):

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.

Ali Caglayan (Apr 01 2022 at 10:39):

@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".

Théo Zimmermann (Apr 01 2022 at 10:43):

Probably the error handling is too conflated (several cases that should lead to several error messages).

Ali Caglayan (Apr 01 2022 at 10:46):

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.

Ali Caglayan (Apr 01 2022 at 14:25):

Add to that retrying after some time when failing

Last updated: May 28 2023 at 18:29 UTC