Stream: coqbot devs & users

Topic: bench check


view this post on Zulip Ali Caglayan (Mar 22 2022 at 12:32):

@Théo Zimmermann I am going to deploy the latest things from the bench check PR to see how they do

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

wait a minute

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

I am really uncomfortable with the use of exceptions in this code.

view this post on Zulip Ali Caglayan (Mar 22 2022 at 12:33):

OK, what should I do instead?

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

I've just posted the review comments that I was writing.

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

FTR, the reason why I'm uncomfortable with exceptions in this situation is that with delayed computations (when using Lwt) I don't have a clear idea of where they will be raised and if they will really be caught by the exception handling mechanism that you put in place (I have strong doubts about that). So I really prefer handling errors with the result monad and keep exceptions for things that are not delayed and things that should not be caught (except by the outer exception handling mechanism).

view this post on Zulip Ali Caglayan (Mar 22 2022 at 13:19):

@Théo Zimmermann I've refactored through the monad this time

view this post on Zulip Ali Caglayan (Mar 22 2022 at 13:27):

@Théo Zimmermann Shall we deploy for a bit?

view this post on Zulip Théo Zimmermann (Mar 22 2022 at 13:27):

Yes, please go ahead.

view this post on Zulip Ali Caglayan (Mar 22 2022 at 13:29):

Deploying: https://github.com/Alizter/bot/actions/runs/2022631602

view this post on Zulip Ali Caglayan (Mar 22 2022 at 13:45):

it seems on push that the bench check isn't immediately created

view this post on Zulip Ali Caglayan (Mar 22 2022 at 13:45):

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

view this post on Zulip Ali Caglayan (Mar 22 2022 at 13:45):

I guess once the base jobs from gitlab come in it will begin to show

view this post on Zulip Ali Caglayan (Mar 22 2022 at 13:45):

I don't know if we can improve this

view this post on Zulip Ali Caglayan (Mar 22 2022 at 14:29):

other than that LGTM @Théo Zimmermann shall we merge upstream?

view this post on Zulip Théo Zimmermann (Mar 22 2022 at 14:31):

I'm fine with merging the check run PR if we are happy with the current behavior. Maybe give it a day or two to get more feedback.

view this post on Zulip Ali Caglayan (Mar 22 2022 at 14:32):

I'll work on the reporting a bit today then. I had a look at the best place the trigger the report, I think whilst handling the check status might be a good option. What do you think?

view this post on Zulip Théo Zimmermann (Mar 22 2022 at 14:33):

I absolutely agree that this is where it should be handled.

view this post on Zulip Théo Zimmermann (Mar 22 2022 at 14:34):

In fact, when the bench is successful, getting the artifact for the table that you want and then pushing that to the check_run summary should be quite straightforward.

view this post on Zulip Théo Zimmermann (Mar 22 2022 at 14:35):

And in case the bench is unsuccessful, it would also be convenient to show some lines from the trace (like we usually do).

view this post on Zulip Ali Caglayan (Mar 22 2022 at 18:54):

Hmm it seems that once the bench has succeeded. Starting a new bench doesn't update the checks

view this post on Zulip Ali Caglayan (Mar 22 2022 at 18:57):

That seems to be because get_pull_request_id_and_milestone doesn't work without a milestone :(

view this post on Zulip Théo Zimmermann (Mar 23 2022 at 08:17):

OK, sorry for having suggested using it then.

view this post on Zulip Théo Zimmermann (Mar 23 2022 at 08:17):

Unfortunately, I probably won't have time to help today.


Last updated: Jan 31 2023 at 10:01 UTC