feat: add some name validation for authors (#29806)

The check consists of verifying that each file has at least one Copyright holder and one Author.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Author: adomani

Mathlib/Probability/HasLaw.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Etienne Marion. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: EtienneMarion
+Authors: Etienne Marion
 -/
 import Mathlib.Probability.Density
 import Mathlib.Probability.Moments.Variance

Mathlib/Tactic/Linter/Header.lean

@@ -134,7 +134,14 @@ def authorsLineChecks (line : String) (offset : String.Pos.Raw) : Array (Syntax
     stxs := stxs.push
       (toSyntax line "." offset,
        s!"Please, do not end the authors' line with a period.")
-  return stxs
+  -- If there are no previous exceptions, then we try to validate the names.
+  if !stxs.isEmpty then
+    return stxs
+  if (line.drop "Authors:".length).trim.isEmpty then
+    return #[(toSyntax line "Authors:" offset,
+       s!"Please, add at least one author!")]
+  else
+    return #[]
 
 /-- The main function to validate the copyright string.
 The input is the copyright string, the output is an array of `Syntax × String` encoding:
@@ -180,6 +187,15 @@ def copyrightHeaderChecks (copyright : String) : Array (Syntax × String) := Id.
       output := output.push
         (toSyntax copyright (copyrightAuthor.take copStart.length),
          s!"Copyright line should start with 'Copyright (c) YYYY'")
+    let author := (copyrightAuthor.drop (copStart.length + 2))
+    if output.isEmpty && author.take 1 != " " then
+      output := output.push
+        (toSyntax copyright (copyrightAuthor.drop (copStart.length + 2)),
+         s!"'Copyright (c) YYYY' should be followed by a space")
+    if output.isEmpty && #["", ".", ","].contains ((author.drop 1).take 1).trim then
+      output := output.push
+        (toSyntax copyright (copyrightAuthor.drop (copStart.length + 3)),
+         s!"There should be at least one copyright author, separated from the year by exactly one space.")
     if !copyrightAuthor.endsWith copStop then
       output := output.push
         (toSyntax copyright (copyrightAuthor.takeRight copStop.length),

MathlibTest/Header.lean

@@ -55,11 +55,12 @@ open Lean Elab Command in
 `#check_copyright cop` takes as input the `String` `cop`, expected to be a copyright statement.
 It logs details of what the linter would report if the `cop` is "malformed".
 -/
-elab "#check_copyright " cop:str : command => do
-  let cop := cop.getString
+elab "#check_copyright " copStx:str : command => do
+  let cop := copStx.getString
+  let offset := copStx.raw.getPos?.get!.increaseBy 1
   for (s, m) in Mathlib.Linter.copyrightHeaderChecks cop do
     if let some rg := s.getRange? then
-      logInfo
+      logInfoAt (.ofRange ({start := rg.start.offsetBy offset, stop := rg.stop.offsetBy offset}))
         m!"Text: `{replaceMultilineComments s.getAtomVal}`\n\
            Range: {(rg.start, rg.stop)}\n\
            Message: '{replaceMultilineComments m}'"
@@ -320,3 +321,74 @@ Authors: Name LastName
   and others.
 -/
 "
+
+/--
+info: Text: `Authors:`
+Range: (140, 148)
+Message: 'The authors line should begin with 'Authors: ''
+-/
+#guard_msgs in
+#check_copyright
+"/-
+Copyright (c) 2024 Damiano Testa, another Name. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors:
+-/
+"
+
+/--
+info: Text: `. All rights reserved.`
+Range: (21, 43)
+Message: ''Copyright (c) YYYY' should be followed by a space'
+-/
+#guard_msgs in
+#check_copyright
+"/-
+Copyright (c) 2024. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: A
+-/
+"
+
+/--
+info: Text: `. All rights reserved.`
+Range: (22, 44)
+Message: 'There should be at least one copyright author, separated from the year by exactly one space.'
+-/
+#guard_msgs in
+#check_copyright
+"/-
+Copyright (c) 2024 . All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: A
+-/
+"
+
+-- We don't do further validation of names.
+
+#guard_msgs in
+#check_copyright
+"/-
+Copyright (c) 2024 nameinalllowercase. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: A
+-/
+"
+
+#guard_msgs in
+#check_copyright
+"/-
+Copyright (c) 2024 First middle LastName. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: A
+-/
+"
+
+#guard_msgs in
+#check_copyright
+"/-
+Copyright (c) 2024 First Last Name jr.. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: A
+-/
+"