Théo Zimmermann (Mar 23 2022 at 13:45): 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.
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.)
Théo Zimmermann (Mar 23 2022 at 13:45):(E.g., by relying on check runs for minimization.)
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?
Gaëtan Gilbert (Mar 23 2022 at 13:46):posting the final file is good imo
Pierre-Marie Pédrot (Mar 23 2022 at 13:46):I want the ouput of the minimzation test at least
Théo Zimmermann (Mar 23 2022 at 13:46):OK. And the same is true for the bench I guess?
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.
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
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.
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
Pierre-Marie Pédrot (Mar 23 2022 at 13:48):same for minimization
Gaëtan Gilbert (Mar 23 2022 at 13:48):I'd prefer a new post for the final result, for notifications
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
Pierre-Marie Pédrot (Mar 23 2022 at 13:49):don't you also get notifications when a post is modified?
Gaëtan Gilbert (Mar 23 2022 at 13:49):not email, don't know about web
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.
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
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.
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
Pierre-Marie Pédrot (Mar 23 2022 at 13:51):because at next force push this is gone
Théo Zimmermann (Mar 23 2022 at 13:52):So indeed, one post, be it at beginning or at end, seems important.
Théo Zimmermann (Mar 23 2022 at 13:52):The post (the comment) can link to the appropriate check run for more details BTW.
Théo Zimmermann (Mar 23 2022 at 13:52):And that way, it avoids the information getting lost.
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.
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.
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: Sep 09 2024 at 06:02 UTC