Zulip Chat Archive
Stream: mathlib4
Topic: copyright header line lint
Edward van de Meent (Jul 27 2024 at 16:34):
it would seem that the current example for how the copyright header should look like doesn't pass CI...
Edward van de Meent (Jul 27 2024 at 16:37):
particularly, it doesn't seem to like Author:, and only allows Authors:
Edward van de Meent (Jul 27 2024 at 16:45):
reading through the linter which checks this, apparently the example is also disallowed because it ends with a period...
Edward van de Meent (Jul 27 2024 at 16:49):
the relevant piece of code can be found here at lines 206-212
Damiano Testa (Jul 28 2024 at 14:38):
I agree with you: the "normalization of copyright headers" happened some time ago, but it looks like the style-guide around it did not get updated.
I imagine that a PR setting the rules straight would be welcome!
Edward van de Meent (Jul 28 2024 at 14:43):
btw, iirc the autocomplete for copy was removed, right?
Damiano Testa (Jul 28 2024 at 14:43):
Not on my VSCode...
Edward van de Meent (Jul 28 2024 at 14:43):
oh, that might be a local issue for me then. nevermind.
Yaël Dillies (Jul 28 2024 at 14:43):
It was not
Damiano Testa (Jul 28 2024 at 14:44):
I never copy-paste copyright headers: I always autocomplete with copy and then I already have two cursors in the two places where I am supposed to write my name.
Edward van de Meent (Jul 28 2024 at 14:45):
weird that it doesn't work for me then
Edward van de Meent (Jul 28 2024 at 14:45):
oh well
Yaël Dillies (Jul 28 2024 at 14:45):
You might have to press TAB to get the autocompletions to trigger
Edward van de Meent (Jul 28 2024 at 14:46):
nope, doesn't work for me :sad:
Damiano Testa (Jul 28 2024 at 14:46):
It used to be enough to type Enter, though that controversially changed recently. :upside_down:
Edward van de Meent (Jul 28 2024 at 14:46):
ah, so that's what i was thinking of
Edward van de Meent (Jul 28 2024 at 14:53):
PR is here
Damiano Testa (Jul 28 2024 at 14:59):
Btw, there are two files in mathlib that use Author instead of Authors and they both have more than one author.
Michael Rothgang (Jul 28 2024 at 16:55):
#15231 fixes this
Michael Rothgang (Jul 28 2024 at 16:56):
Should the style linter also lint test files? Right now, it does not... which is why this was not caught.
Damiano Testa (Jul 28 2024 at 17:16):
Just for fun, I tried to match author names that I might guess represent the same person among mathlib files.
| Name | Files authored |
|---|---|
| Alex Best | 1 |
| Alex J. Best | 24 |
| -- | |
| Brendan Murphy | 5 |
| Brendan S. Murphy | 1 |
| -- | |
| Dagur Asgeirsson | 68 |
| Dagur Tómas Ásgeirsson | 1 |
| -- | |
| Edward Ayers | 2 |
| E. W. Ayers | 2 |
| E.W.Ayers | 3 |
| -- | |
| Filipo A. E. Nuccio | 1 |
| Filippo A. E. Nuccio | 20 |
| -- | |
| Floris van Doorn | 175 |
| Floris Van Doorn | 2 |
| -- | |
| Ian Benway | 1 |
| Ian Benway. | 1 |
| -- | |
| Jesse Han | 1 |
| Jesse Michael Han | 4 |
| -- | |
| Johanes Hölzl | 1 |
| Johannes Hölzl | 359 |
| -- | |
| Kevin H. Wilson | 3 |
| Kevin Wilson | 1 |
| -- | |
| María Inés de Frutos Fernández | 1 |
| María Inés de Frutos-Fernández | 18 |
| -- | |
| Matthew Ballard | 1 |
| Matthew Robert Ballard | 2 |
| -- | |
| Nick Kuhn | 2 |
| Nikolas Kuhn | 3 |
| -- | |
| Richard Hill | 1 |
| Richard M. Hill | 2 |
| -- | |
| Robert Lewis | 11 |
| Robert Y. Lewis | 59 |
| Rob Lewis | 1 |
| -- | |
| Sam van Gool | 4 |
| Sam v. Gool | 1 |
| -- | |
| Sebastien Gouezel | 1 |
| Sébastien Gouëzel | 227 |
| -- | |
| Tomas Skrivan | 9 |
| Tomáš Skřivan | 5 |
| -- | |
| Violeta Hernández | 1 |
| Violeta Hernández Palacios | 20 |
| -- | |
| Yael Dillies | 1 |
| Yaël Dillies | 286 |
| -- | |
| Yakov Pechersky | 25 |
| Yakov Peckersky | 1 |
| -- | |
| Yury G. Kudryashov | 75 |
| Yury G. KudryashovJ | 1 |
| Yury Kudriashov | 6 |
| Yury Kudryashov | 412 |
| -- |
Michael Rothgang (Jul 28 2024 at 17:25):
Since we're talking about the copyright header linter: I found a bug in the new text-based linter: it would not check if the copyright header was complete after a four lines. Most files comply, some have more or less interesting violations - and about 50 have so many authors that multiple lines are used to list them. branch#MR-copyright-check-last-line has the details: all remaining files have many authors
Michael Rothgang (Jul 28 2024 at 17:27):
Is there a preference for how to deal with this?
- We don't care, just let it be
- Remove headers which are clearly wrong; let the rest be (and do not lint this)
- add linter exceptions for all 50 files
- Format all authors on a single line (and teach the long linter to ignore this)
- Allow authors lines to span multiple lines (but: how to distinguish many authors from other rubbish?)
Yury G. Kudryashov (Jul 28 2024 at 21:56):
All "Yury Kudryashov"s are me. Do you prefer to normalize all names in one PR, or should I submit a separate PR for my copyright headers?
Damiano Testa (Jul 28 2024 at 22:01):
I'm happy to uniformize the names above and, when there is a majority of usages, I would go for that version. However, I'd give some time to people to tell me that they agree/disagree: I did no git-scavenging to check how the names above originated, for instance.
Yury G. Kudryashov (Jul 28 2024 at 22:07):
In my case, they originated from different e-mail signatures on different accounts (Emacs snippet inserts the current value of user-full-name) +1 typo.
Damiano Testa (Jul 29 2024 at 07:11):
I went ahead and performed the author name changes that the table above suggests. I always went for the most common spelling, I think!
Damiano Testa (Jul 29 2024 at 07:12):
Of course, if anyone notices that I merged two different authors, just because they had similar names, please tell me! Looking at the list, all the changes look pretty straightforward, but you never know.
Last updated: May 02 2025 at 03:31 UTC