Adding new contributor comment on PR

Stream: general

[Kevin Wilson]

Hi all. I was talking with @Jireh Loreaux about some confusion on my part of why my PRs weren't appearing in the review queue. The information is clearly in the contributing document, but I thought that it might be helpful to feature it in a comment on the PR when the new-contributor label is added to a PR.

I added that PR here: https://github.com/leanprover-community/mathlib4/pull/35109

Happy for any comments!

[Kim Morrison]

@Kevin Wilson I pushed some changes, and delegated. If you're happy, please merge as is, or otherwise reply here/github for further review.

[Michael Rothgang]

I just added another small idea to the PR. If you prefer, we can merge your PR now and add it in a future change.

[Kevin Wilson]

Thanks, y'all! @Michael Rothgang I think your change is a good idea, but honestly perhaps should be in one of the other actions? That seems like a useful link not just for new contributors but for anyone.

[Kevin Wilson]

@Kim Morrison I went ahead and merged it. Thanks for catching the idempotency issue in particular!

[Kim Morrison]

Kevin Wilson said:

Thanks for catching the idempotency issue in particular!

(checks notes... actually both Claude and I missed that, but Codex caught it.)

[Thomas Murrills]

Off-topic, but @Kim Morrison, does that mean that your Claude in turn uses Codex? :eyes:

[Thomas Murrills]

Also, very glad to see the new contributor experience being improved! Thanks @Kevin Wilson for the PR! :D

[Kim Morrison]

Yes. I have a .claude/skills/second-opinion/SKILL.md that delegates to Codex for mid-conversation reviews.

[Marcelo Lynch]

re: the idempotency thing (although I don't think it should be that big of a deal because this workflow is only triggered on open, but better safe than sorry!), we already use sticky-pull-request-comment elsewhere, what do you think of #35160 for consistency?

[Marcelo Lynch]

Regarding posting comments, something to keep in mind is reusing the ones we already post to avoid clutter (this actually came up today in one of my own PRs where I was tempted to add yet another comment and Anne suggested to reuse the "PR summary" one, which made total sense).

I do think this case warrants its own comment! But just to be aware of this slippery slope (and maybe even some of Michael's suggestions can use this?)

[Kevin Wilson]

Personally, I'm all for consistency :-)

[Kevin Wilson]

If you want to see what it looks like, here's a live example: https://github.com/leanprover-community/mathlib4/pull/35159

[Michael Rothgang]

Kevin Wilson said:

Thanks, y'all! Michael Rothgang I think your change is a good idea, but honestly perhaps should be in one of the other actions? That seems like a useful link not just for new contributors but for anyone.

I just made #35583 to add this line to the welcome message. Reviews welcome! especially by somebody who can help me test the yaml interpolation aspect of it. tested now!

[Chris Henson]

I ran the above in my fork and the interpolation seemed to work as expected.