SyncPRSummary: make a separate bot comment for

[shravanngoswamii]

ref chalk-lab/Mooncake.jl#1095 (comment)

[penelopeysm]

So this will probably create a single comment, but it will come after the PR first comment, and it will also come after all the individual bot spam. I wonder if you could also somehow use the GitHub API to hide all the individual bot comments (since with the consolidated version, they wouldn't be necessary anymore)? We can't delete them ofc, because the individual benchmark etc. workflows need to have them, that's why I'm thinking of hiding.

[shravanngoswamii]

I wonder if you could also somehow use the GitHub API to hide all the individual bot comments

tbh, I would prefer having all the bot comments in single comment, maybe adding separate markers for each might help (Code Coverage, docs, benchmarks comments). I am not sure how Code Coverage setup works, I will have to look into that.

[penelopeysm]

Right, I guess the issue is that we're using someone else's workflow for the review comment stuff, and we might have to hand-roll our own. I wouldn't mind that too, it would be more elegant -- it's mostly a question of whether it's worth the time to implement it, but that's a decision you can make.

[shravanngoswamii]

Right, I guess the issue is that we're using someone else's workflow for the review comment stuff

I think we are using reviewdog for review comments and peterevans actions for other commenting purpose. And we also have some thollander action for commenting -- I don't exactly remember where are we using this one but I am sure I did add that somewhere. (edit: docs, main website and DoodleBUGS)

If we can put together something of our own, it would be great to have! But I don't think it's worth the time because even if we combine all bot comments into one, review comments should still be kept separated (obvious reasons of them getting deleted once resolved) and reviewdog is well maintained for this purpose too.