feat(lint-style): rewrite the linter for plain string adaptation not…

…es in Lean (#14058)

In true fashion, the linter (correctly) flags itself; we add these to the nolints file.

Mathlib/Tactic/Linter/TextBased.lean

@@ -30,6 +30,9 @@ inductive StyleError where
   | copyright (context : Option String)
   /-- Malformed authors line in the copyright header -/
   | authors
+  /-- The bare string "Adaptation note" (or variants thereof): instead, the
+  #adaptation_note command should be used. -/
+  | adaptationNote
   /-- The current file was too large: this error contains the current number of lines
   as well as a size limit (slightly larger). On future runs, this linter will allow this file
   to grow up to this limit. -/
@@ -51,9 +54,11 @@ inductive ErrorFormat
 /-- Create the underlying error message for a given `StyleError`. -/
 def StyleError.errorMessage (err : StyleError) (style : ErrorFormat) : String := match err with
   | StyleError.copyright (some context) => s!"Malformed or missing copyright header: {context}"
-  | StyleError.copyright none => s!"Malformed or missing copyright header"
+  | StyleError.copyright none => "Malformed or missing copyright header"
   | StyleError.authors =>
     "Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'"
+  | StyleError.adaptationNote =>
+    "Found the string \"Adaptation note:\", please use the #adaptation_note command instead"
   | StyleError.fileTooLong current_size size_limit =>
     match style with
     | ErrorFormat.github =>
@@ -68,6 +73,7 @@ def StyleError.errorMessage (err : StyleError) (style : ErrorFormat) : String :=
 def StyleError.errorCode (err : StyleError) : String := match err with
   | StyleError.copyright _ => "ERR_COP"
   | StyleError.authors => "ERR_AUT"
+  | StyleError.adaptationNote => "ERR_ADN"
   | StyleError.fileTooLong _ _ => "ERR_NUM_LIN"
 
 /-- Context for a style error: the actual error, the line number in the file we're reading
@@ -132,6 +138,7 @@ def parse?_errorContext (line : String) : Option ErrorContext := Id.run do
         -- NB: keep this in sync with `normalise` above!
         | "ERR_COP" => some (StyleError.copyright "")
         | "ERR_AUT" => some (StyleError.authors)
+        | "ERR_ADN" => some (StyleError.adaptationNote)
         | "ERR_NUM_LIN" =>
           -- Parse the error message in the script. `none` indicates invalid input.
           match (error_message.get? 0, error_message.get? 3) with
@@ -214,6 +221,17 @@ def copyrightHeaderLinter : TextbasedLinter := fun lines ↦ Id.run do
         output := output.push (StyleError.authors, 4)
   return output
 
+/-- Lint on any occurrences of the string "Adaptation note:" or variants thereof. -/
+def adaptationNoteLinter : TextbasedLinter := fun lines ↦ Id.run do
+  let mut errors := Array.mkEmpty 0
+  let mut lineNumber := 1
+  for line in lines do
+    -- We make this shorter to catch "Adaptation note", "adaptation note" and a missing colon.
+    if line.containsSubstr "daptation note" then
+      errors := errors.push (StyleError.adaptationNote, lineNumber)
+    lineNumber := lineNumber + 1
+  return errors
+
 /-- Whether a collection of lines consists *only* of imports, blank lines and single-line comments.
 In practice, this means it's an imports-only file and exempt from almost all linting. -/
 def isImportsOnlyFile (lines : Array String) : Bool :=
@@ -240,7 +258,9 @@ def checkFileLength (lines : Array String) (existing_limit : Option ℕ) : Optio
 end
 
 /-- All text-based linters registered in this file. -/
-def allLinters : Array TextbasedLinter := #[copyrightHeaderLinter]
+def allLinters : Array TextbasedLinter := #[
+    copyrightHeaderLinter, adaptationNoteLinter
+  ]
 
 /-- Read a file, apply all text-based linters and print the formatted errors.
 `sizeLimit` is any pre-existing limit on this file's size.

scripts/lint-style.py

@@ -51,7 +51,6 @@
 ERR_IND = 17 # second line not correctly indented
 ERR_ARR = 18 # space after "←"
 ERR_NSP = 20 # non-terminal simp
-ERR_ADN = 25 # the string "Adaptation note"
 
 exceptions = []
 
@@ -67,10 +66,8 @@
             exceptions += [(ERR_MOD, path, None)]
         elif errno == "ERR_LIN":
             exceptions += [(ERR_LIN, path, None)]
-        elif errno == "ERR_OPT":
-            exceptions += [(ERR_OPT, path, None)]
         elif errno == "ERR_ADN":
-            exceptions += [(ERR_ADN, path, None)]
+            pass # maintained by the Lean style linter now
         elif errno == "ERR_TAC":
             exceptions += [(ERR_TAC, path, None)]
         elif errno == "ERR_TAC2":
@@ -331,14 +328,6 @@ def left_arrow_check(lines, path):
         newlines.append((line_nr, new_line))
     return errors, newlines
 
-def adaptation_note_check(lines, path):
-    errors = []
-    for line_nr, line in lines:
-        # We make this shorter to catch "Adaptation note", "adaptation note" and a missing colon.
-        if "daptation note" in line:
-            errors += [(ERR_ADN, line_nr, path)]
-    return errors, lines
-
 def output_message(path, line_nr, code, msg):
     if len(exceptions) == 0:
         # we are generating a new exceptions file
@@ -387,8 +376,6 @@ def format_errors(errors):
             output_message(path, line_nr, "ERR_ARR", "Missing space after '←'.")
         if errno == ERR_NSP:
             output_message(path, line_nr, "ERR_NSP", "Non-terminal simp. Replace with `simp?` and use the suggested output")
-        if errno == ERR_ADN:
-            output_message(path, line_nr, "ERR_ADN", 'Found the string "Adaptation note:", please use the #adaptation_note command instead')
 
 def lint(path, fix=False):
     global new_exceptions
@@ -403,7 +390,6 @@ def lint(path, fix=False):
                             long_lines_check,
                             isolated_by_dot_semicolon_check,
                             left_arrow_check,
-                            adaptation_note_check,
                             nonterminal_simp_check]:
             errs, newlines = error_check(newlines, path)
             format_errors(errs)

scripts/nolints-style.txt

@@ -15,3 +15,17 @@ Mathlib/Tactic/Linter.lean : line 4 : ERR_COP : Malformed or missing copyright h
 Archive/Sensitivity.lean : line 2 : ERR_COP : Malformed or missing copyright header: Copyright line is malformed
 Archive/Sensitivity.lean : line 3 : ERR_COP : Malformed or missing copyright header: Second line should be "Released under Apache 2.0 license as described in the file LICENSE."
 Archive/Sensitivity.lean : line 4 : ERR_COP : Malformed or missing copyright header: The third line should describe the file's main authors
+
+-- The linter for the string "adaptation note" fires in the implementation of the linter,
+-- and in the implementation of the #adaptation_note tactic: this is as expected.
+Mathlib/Tactic/AdaptationNote.lean : line 9 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
+Mathlib/Tactic/AdaptationNote.lean : line 12 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
+Mathlib/Tactic/AdaptationNote.lean : line 21 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
+Mathlib/Tactic/AdaptationNote.lean : line 27 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
+Mathlib/Tactic/AdaptationNote.lean : line 39 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
+Mathlib/Tactic/AdaptationNote.lean : line 52 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
+Mathlib/Tactic/Linter/TextBased.lean : line 33 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
+Mathlib/Tactic/Linter/TextBased.lean : line 60 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
+Mathlib/Tactic/Linter/TextBased.lean : line 222 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
+Mathlib/Tactic/Linter/TextBased.lean : line 227 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
+Mathlib/Tactic/Linter/TextBased.lean : line 228 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead