wip: testing: copyright mostly works; isolated by is too weak -> stre…

…ngthen next!

Mathlib/Tactic/Linter/TextBased.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Michael Rothgang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Rothgang
+Author: Michael Rothgang and Joe Doe
 -/
 
 import Lean.Elab.Command
@@ -175,7 +175,8 @@ def copyright_header : LinterCore := fun lines ↦ Id.run do
   -- The second line should be standard.
   let expected_second_line := "Released under Apache 2.0 license as described in the file LICENSE."
   if start.get? 2 != some expected_second_line then
-    output := output.push (StyleError.copyright s!"Second line should be {expected_second_line}", 3)
+    output := output.push (StyleError.copyright
+      s!"Second line should be \"{expected_second_line}\"", 3)
   -- The third line should contain authors.
   if let some line := start.get? 3 then
     if !line.containsSubstr "Author" then
@@ -202,7 +203,8 @@ def isolated_by_dot_semicolon : LinterCore := fun lines ↦ Id.run do
         -- should not be used in the second or later arguments of a tuple/anonymous constructor
         -- See https://github.com/leanprover-community/mathlib4/pull/3825#discussion_r1186702599
         if !previous_line.endsWith "," then
-          if !(line.containsSubstr ", fun" && (line.endsWith "=>" || line.endsWith "↦")) then
+          if !(previous_line.containsSubstr ", fun" &&
+              (previous_line.endsWith "=>" || previous_line.endsWith "↦")) then
             output := output.push (StyleError.isolated_by, line_number)
       if line.trimRight.startsWith ". " then
         output := output.push (StyleError.dot, line_number) -- has an auto-fix
@@ -230,7 +232,7 @@ def lint_file (path : System.FilePath) : IO Unit := do
   -- XXX: this list is currently not sorted: for github, that's probably fine
   format_errors (Array.flatten all_output) (Array.mkEmpty 0)
 
--- #eval lint_file (System.mkFilePath ["Mathlib", "Tactic", "Linter", "TextBased.lean"])
+#eval lint_file (System.mkFilePath ["Mathlib", "Tactic", "Linter", "TextBased.lean"])
 
 /-- Lint all files in `Mathlib.lean`. -/
 def check_all_files : IO Unit := do