Policy of "Authors:" comment

Stream: mathlib4

[Jakub Nowak]

What is the policy around "Authors:" comment in mathlib that is usually present at the top of the file? The only mention of it I found in #contrib is

mathlib has a style guide and PRs fixing style violations documented in this guide are welcome. Other stylistic PRs that don't have explicit approval by the authors of the affected files may be closed. We invite authors to instead discuss the proposed change on Zulip and, when significant consensus among reviewers is reached, to open a PR to the style guide.

Which would suggest that maybe more appropriate name would be "Maintainers"? Also, whether and when should I add myself to "Authors" in my PRs?

[Yury G. Kudryashov]

I'm adding myself if I make a substantial contribution to a file. It's hard to tell what's "substantial".

[Jakub Nowak]

Actually, the question I wanted to ask, but didn't explicitly. What is the purpose of this comment? Knowing who to ping on Zulip when asking questions?

[Aaron Liu]

From the style guide:

Regarding the list of authors: use Authors even when there is only a single author. Don't end the line with a period, and use commas (, ) to separate all author names (so don't use and between the penultimate and final author.) We don't have strict rules on what contributions qualify for inclusion there. The general idea is that the people listed there should be the ones we would reach out to if we had questions about the design or development of the Lean code.

[Jakub Nowak]

Ah, I didn't expect to find this in the style guide.

[Violeta Hernández]

I only add my name to files if one of three things happens:

• I'm one of the original authors
• I've written at least a third or so of the code
• I've been PRing to and maintaining the code for at least a month or two.

These are just my personal guidelines, but maybe it gives you an idea for what a reasonable standard might be.

[Wrenna Robson]

Yeah I have generally added myself when I have done substantial work on a file such that I know my way around it/the original author would no longer recognise where they started.

[Johan Commelin]

Personally, I never make use of the Authors: line. I only add myself if I start a new file, because otherwise the linter complains.