Stream: Coq devs & plugin devs

Topic: Minimization noise


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

Indeed. I believe that we can reduce minimization spam a lot BTW. I've just hadn't had time to work on it yet.

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2022 at 13:45):

(@Gaëtan Gilbert I agree that we should concentrate the minimization messages in one place rather than repeatedly spamming the thread. There are some PRs where coqbot talks thrice as much as humans.)

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

(E.g., by relying on check runs for minimization.)

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

Do you wish all minimization comments to go away or would you like to still keep some?

view this post on Zulip Gaëtan Gilbert (Mar 23 2022 at 13:46):

posting the final file is good imo

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2022 at 13:46):

I want the ouput of the minimzation test at least

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

OK. And the same is true for the bench I guess?

view this post on Zulip Ali Caglayan (Mar 23 2022 at 13:47):

To be clear coqbot does not comment at all about the bench report. It just updates the checks tab.

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2022 at 13:48):

ideally for both the bench and minimization, the bot should modify the same post that is the answer to the user

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

Yes, but you planned to make it comment for the final results, right? So I'm checking in advance that this is not going to be considered disruptive.

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2022 at 13:48):

i.e. you write "@coqbot bench", it tells "ok on it" and when done rewrites this post

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2022 at 13:48):

same for minimization

view this post on Zulip Gaëtan Gilbert (Mar 23 2022 at 13:48):

I'd prefer a new post for the final result, for notifications

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2022 at 13:48):

instead of spamming messages for every attempt, it should synthetize them in the top post

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2022 at 13:49):

don't you also get notifications when a post is modified?

view this post on Zulip Gaëtan Gilbert (Mar 23 2022 at 13:49):

not email, don't know about web

view this post on Zulip Ali Caglayan (Mar 23 2022 at 13:50):

Pierre-Marie Pédrot said:

i.e. you write "@coqbot bench", it tells "ok on it" and when done rewrites this post

So currently the bench will appear to run in the checks at the bottom. We've also discussed getting coqbot to thumbs up the post.

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2022 at 13:51):

the important point is that it should leave a trace as as post. It's a nightmare to find back a bench using the gitlab ui

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

Pierre-Marie Pédrot said:

don't you also get notifications when a post is modified?

No, I don't think you get any.

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2022 at 13:51):

if you only get a link in the CI checks this is as good as lost to the mist of times

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2022 at 13:51):

because at next force push this is gone

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

So indeed, one post, be it at beginning or at end, seems important.

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

The post (the comment) can link to the appropriate check run for more details BTW.

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

And that way, it avoids the information getting lost.

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

If we in addition want a notification when the bench / minimization is complete, then the comment should happen at the very end.

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

And in the meantime, only the check run / possible thumbs up reaction would indicate that the requested thing is in progress.

view this post on Zulip Jason Gross (Mar 26 2022 at 02:58):

I think we probably want a separate post for each minimization job, otherwise the files will often be severely truncated by GitHub's comment size limits. (I do think that the bot should not keep spamming on auto-resumption, and that it should auto-hide previous iterations of a given job when minimization is requested a second time)


Last updated: Feb 01 2023 at 16:03 UTC