Style Exceptions

Stream: mathlib4

[Pietro Monticone]

Hi everyone, I'm working on the resolution of style exceptions starting from ERR_COPs.

How should I attribute authorships to individual Lean files? Is it enough to check the author of the first commit or I should include other contributors to a given file? What are the exact criteria?

Consider the first ERR_COP as a paradigmatic example:

Mathlib/Data/Array/Basic.lean : line 1 : ERR_COP : Malformed or missing copyright header

I've checked the commit history of that file and noticed that @Mario Carneiro is the author of the first commit (dated May 2021) and added this copyright header immediately above the first import:

/-
Copyright (c) 2021 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Std.Tactic.Alias

attribute [simp] Array.toArrayAux_eq

alias List.toArray_data := Array.data_toArray

namespace Array

Is it acceptable or I should include other people as authors?

[Pietro Monticone]

PS: I'm not sure why both line 1 and line 3 are involved here:

Mathlib/Data/Array/Basic.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Array/Basic.lean : line 1 : ERR_COP : Malformed or missing copyright header
Mathlib/Data/Array/Basic.lean : line 3 : ERR_COP : Malformed or missing copyright header

Adding the copyright header as I've done above should be enough, right?

[Eric Wieser]

For many files, the right thing to do is look in the mathlib3 history

[Pietro Monticone]

Ok, I'll do it.

[Pietro Monticone]

Here is the first PR for the "Data" folder: #11825.

[Pietro Monticone]

Here is the PR for the "Tactic" folder: #11826.

[Pietro Monticone]

Opened PR #11854 removing ERR_COP style exceptions that have been resolved in #11825 already merged.

[Pietro Monticone]

Opened PR #11892 removing ERR_COP and ERR_MOD style exceptions I've resolved.

[Pietro Monticone]

Opened PR #11893 solving some ERR_MOD style exceptions by adding brief module docstrings in Basic.lean files and removing the associated lines in scripts/style-exceptions.txt accordingly.

[Michael Rothgang]

I left some comments on #11893. TL;DR I wonder if some files should rather be removed. @Yaël Dillies may have an opinion :-)

[Yaël Dillies]

Yes indeed. See #10709, #11882, #11887, #11898 for what's going to happen to those files

[Pietro Monticone]

I should have fixed all ERR_COPs. I will tackle the remaining ERR_MODs in the coming days / weeks.