diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean index 7a1978302ea6bf..9ec2341937f3f2 100644 --- a/Mathlib/Tactic/Linter/TextBased.lean +++ b/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