mathlib contributions

Stream: new members

[James Arthur]

Hello!
I was chatting to people on the Xena Project discord about starting to contribute to mathlib. They suggested going through and editing the docstrings on files to make them more descriptive. Could I start doing this?

[Shing Tak Lam]

@James Arthur 's GitHub username is jamesa9283

[Scott Morrison]

@James Arthur, I've just sent you an invitation giving you the ability to create and push non-master branches of the mathlib repository. Looking forwards to some docstrings! :-)

[James Arthur]

Thankyou :D

[James Arthur]

Just to clarify, am I to create my own branch to edit docstrings or use the ones already there?

[Johan Commelin]

Nope, please start a new branch

[Johan Commelin]

git checkout -b algebra-docstrings or something like that

[Johan Commelin]

(Change algebra to whatever you're working on :wink:)

[James Arthur]

Brilliant! (Is that a subtle note that algebra needs looking at?)

[Johan Commelin]

No, just a random example

[James Arthur]

Fair enough, thankyou

[Rob Lewis]

There's an official list of files/declarations that need docs: https://github.com/leanprover-community/mathlib/blob/master/scripts/nolints.txt

[Rob Lewis]

If you're looking for a random place to dive in, find a file on that list with a lot of entries, it's probably a good place to start.

[Rob Lewis]

(These are declaration doc strings, not the module docs at the top, but there's a correlation between missing decl docs and missing/small module docs.)

[Johan Commelin]

Otoh, I suggest starting with a small file

[Johan Commelin]

To get a feel for the PR/review process

[Johan Commelin]

A first PR with just 5 docstrings is totally fine

[Johan Commelin]

@James Arthur Small note: defs are now required to have docstrings, but lemmas don't. However, there are still a lot of old defs from before the requirement, that don't have docstrings. So doccing defs is considered more worthwile practice than lemmas. (Even though good docstrings on important theorems is certainly encouraged.)

[James Arthur]

OK I shall look for defs next time :)

[Bryan Gin-ge Chen]

Johan Commelin said:

A first PR with just 5 docstrings is totally fine

Even a PR adding 1 docstring can be fine too. Small PRs are easy to review and can get merged more quickly. (There's a tradeoff here of course, one bigger PR fixing a bunch of related docstrings in the same file is probably better than a chain of tiny PRs.)

[James Arthur]

I did four. It was a good time to get some experience with the whole process

[Chase Fleming]

Hi all, I'm a third year PhD student at University of South Carolina focusing in set theory and topology. I'm interested in contributing to mathlib - specifically working on expanding the ordinal topology section. Can anyone orient me here with getting set up to contribute?

[Johan Commelin]

@Chase Fleming Welcome. Have you see https://leanprover-community.github.io/contribute/index.html?

[Johan Commelin]

Does that answer (most of) your questions?

[Chase Fleming]

@Johan Commelin Yep! I missed that page from the Lean4 documentation. Thank you so much!

[Matias Heikkilä]

thanks for a nice experience with my first PR :pray: