diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean index ad3cf40d6309b..ec5db28b6c62d 100644 --- a/Mathlib/Tactic/Linter/TextBased.lean +++ b/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. diff --git a/scripts/lint-style.py b/scripts/lint-style.py index c57027612bad9..b128dc0ae2eb1 100755 --- a/scripts/lint-style.py +++ b/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) diff --git a/scripts/nolints-style.txt b/scripts/nolints-style.txt index 6859d74725ce2..efee926577dd7 100644 --- a/scripts/nolints-style.txt +++ b/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