Contribution questions

Stream: new members

[LordRatte]

I am trying to understand the contribution process better. Suppose I write a proof for
theorem toString_isNat (n : ℕ) : (toString n).isNat (for the sake of discussion) that I think might be useful to others.

• How do I decide whether to contribute to lean4, Mathlib or something else?
• Do I just open a PR or do I start a discussion about it?
• How do I know where to put it inside the relevant repo?

If I am asking the wrong questions, feel free help me reframe the questions. For instance, maybe the theorem toString_isNat would not be helpful to anyone. Then I would want to know how to know what would be helpful.

[Kevin Buzzard]

I shouldn't think that mathlib is interested in anything to do with strings, and many of the core Lean contributors are not reading this channel. You might want to ask in #general about plans for strings and how you might be able to help. You might also want to post your proof.

[LordRatte]

So as a rule of thumb would I ask in #general for other topics as well? Let's say the theorem wasn't about strings. Would I always start there if I don't know where the topic belongs?

[Kevin Buzzard]

Maybe someone more knowledgeable than me about the ecosystem around strings will see this discussion (maybe edit the title so that it mentions toString_isNat?) and will give you better advice. There are all kinds of basic repos like Std/Batteries which I don't know anything about and which might be the place for this lemma if it's not already there.

[Mirek Olšák]

To Kevin, I think this is a general question, not necessarily about Strings but rather about the contribution process. Unfortunately, I am not much of a contributor, so I feel other people can advise better but my understanding is:

• Discuss it here on Zulip, either in general, or perhaps mathlib if you think your contribution belongs to Mathlib. Coordinate with others interested in similar questions.
• Figure out where it belongs -- is it mathlib? batteries? cslib? something else? Getting contributions to Lean Core is considered harder.
• Break it into pieces. As far as I understand, smaller pull requests can get merged easier.
• Link the pull requests with the relevant Zulip thread (both ways)