Bot idea: warn if a PR is opened against a fork

Stream: mathlib4

[Michael Rothgang]

What the title says: from experience, a number of new contributors opens a PR from a fork (because that's the usual open source workflow). It could be nice if a bot determined this automatically and accordingly commented.

• otherwise, humans have to do this :-)
• humans sometimes overlook this, and then re-articulate issues the style linters would have pointed out

Disclaimer: I do not know how to write such a bot.

[Michael Rothgang]

Similar ideas: have the bot post a welcome comment, similar to Rust's highfive; in particular this message. This could include referencing the style guide/contribution guidelines.

[Kim Morrison]

Opening up ChatGPT and saying "I'd like a github actions workflow that does XYZ", and then copying and pasting into the .github/workflows/ directory is surprisingly successful. The bar for "I do not know how to write such a bot" has become very low of late!