mathlib file authorship

Stream: general

[Rob Lewis]

Since this came up in a PR recently, it seems time to clarify the guidelines for the "Author" attribution on mathlib files. @Bryan Gin-ge Chen proposed a change at https://github.com/leanprover-community/leanprover-community.github.io/pull/58 :

Regarding the list of authors: 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.

I think this captures the intent of the author list. In practice, it's very much not a list of everyone who has contributed to the file; this is typically tracked by the git history. Refactorings and file renamings can occasionally make the history hard to trace, but refactorings are also a problem for lists of contributors.

Just wanted to highlight the change in case anyone has thoughts/comments, since it's a community policy thing!

[Rob Lewis]

This would be policy going forward, btw, I certainly don't plan to remove any author attributions myself and I doubt anyone else does.