Stream: coqbot devs & users

Topic: bench command


view this post on Zulip Ali Caglayan (Mar 21 2022 at 11:20):

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

view this post on Zulip Théo Zimmermann (Mar 21 2022 at 12:06):

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

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 21 2022 at 12:19):

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

view this post on Zulip Ali Caglayan (Mar 21 2022 at 12:19):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Mar 21 2022 at 17:20):

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

view this post on Zulip Ali Caglayan (Mar 21 2022 at 18:05):

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

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 01 2022 at 14:25):

Add to that retrying after some time when failing


Last updated: Jan 31 2023 at 10:01 UTC