Discussing contributions to mathlib

Stream: new members

[Laurance Lau]

Hello, I am not sure where to discuss contributions to mathlib. Am I to draft a PR and then post a new topic in PR reviews or discuss the intended contribution somewhere before drafting a PR? Thanks.

[Kyle Miller]

Here's a contribution guide: https://leanprover-community.github.io/contribute/index.html

[Laurance Lau]

Thanks for linking to the contribution guide! About "Use Zulip to discuss your contribution before and while you are working on it", I just was not sure whether mathlib4 or PR review would be the appropriate channel and whether all PRs should have been discussed on Zulip or if easy PRs do not need their own post.

[Ruben Van de Velde]

Easy PRs don't need a

[Ruben Van de Velde]

post

[Kyle Miller]

It's best to be in communication with what you're generally up to, so that reviewers can know the context.

If you're just starting out, it doesn't hurt to talk about even easy PRs, to make sure you've got the right calibration for what an easy PR is.

[Jireh Loreaux]

If you're just starting, it's also a good idea to post on Zulip so that people can guide you in the right way to do it before you spend a long while going down the wrong path on your own.