diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean index 511a1c693dcc57..544f44eb1d63cf 100644 --- a/Mathlib/Tactic/Linter/TextBased.lean +++ b/Mathlib/Tactic/Linter/TextBased.lean @@ -55,8 +55,6 @@ inductive StyleError where /-- Lint against "too broad" imports, such as `Mathlib.Tactic` or any module in `Lake` (unless carefully measured) -/ | broadImport (module : BroadImports) - /-- An isolated focusing dot: a focusing dot on its own line -/ - | isolatedCDot /-- Line longer than 100 characters -/ | lineLength (actual : Int) : StyleError /-- The current file was too large: this error contains the current number of lines @@ -92,7 +90,6 @@ def StyleError.errorMessage (err : StyleError) (style : ErrorFormat) : String := "In the past, importing 'Lake' in mathlib has led to dramatic slow-downs of the linter (see \ e.g. mathlib4#13779). Please consider carefully if this import is useful and make sure to \ benchmark it. If this is fine, feel free to allow this linter." - | StyleError.isolatedCDot => "Line is an isolated focusing dot ·" | StyleError.lineLength n => s!"Line has {n} characters, which is more than 100" | StyleError.fileTooLong currentSize sizeLimit previousLimit => match style with @@ -113,7 +110,6 @@ def StyleError.errorCode (err : StyleError) : String := match err with | StyleError.authors => "ERR_AUT" | StyleError.adaptationNote => "ERR_ADN" | StyleError.broadImport _ => "ERR_IMP" - | StyleError.isolatedCDot => "ERR_DOT" | StyleError.lineLength _ => "ERR_LIN" | StyleError.fileTooLong _ _ _ => "ERR_NUM_LIN" @@ -217,7 +213,6 @@ def parse?_errorContext (line : String) : Option ErrorContext := Id.run do else none | "ERR_AUT" => some (StyleError.authors) | "ERR_ADN" => some (StyleError.adaptationNote) - | "ERR_DOT" => some (StyleError.isolatedCDot) | "ERR_IMP" => -- XXX tweak exceptions messages to ease parsing? if (errorMessage.get! 0).containsSubstr "tactic" then @@ -347,17 +342,6 @@ def broadImportsLinter : TextbasedLinter := fun lines ↦ Id.run do lineNumber := lineNumber + 1 return errors -/-- Lint a collection of input strings if one of them contains an isolated focusing dot: -these should go next to the subsequent line instead. -/ -def isolatedCDotLinter : TextbasedLinter := fun lines ↦ Id.run do - let mut errors := Array.mkEmpty 0 - let mut lineNumber := 1 - for line in lines do - if line.trimLeft == "." then - errors := errors.push (StyleError.isolatedCDot, lineNumber) - lineNumber := lineNumber + 1 - return errors - /-- Iterates over a collection of strings, finding all lines which are longer than 101 chars. We allow URLs to be longer, though. -/ @@ -396,8 +380,7 @@ end /-- All text-based linters registered in this file. -/ def allLinters : Array TextbasedLinter := #[ - copyrightHeaderLinter, adaptationNoteLinter, broadImportsLinter, isolatedCDotLinter, - lineLengthLinter + copyrightHeaderLinter, adaptationNoteLinter, broadImportsLinter, lineLengthLinter ] /-- Controls what kind of output this programme produces. -/ @@ -476,7 +459,7 @@ def lintModules (moduleNames : Array String) (mode : OutputSetting) (fix : Bool) if pythonOutput != "" then IO.println pythonOutput formatErrors allUnexpectedErrors style if numberErrorFiles > 0 && mode matches OutputSetting.print _ then - IO.println s!"error: found {numberErrorFiles} new style errors\n\ + IO.println s!"error: found {allUnexpectedErrors.size} new style errors\n\ run `lake exe lint-style --update` to ignore all of them" | OutputSetting.update => formatErrors allUnexpectedErrors ErrorFormat.humanReadable diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index 2947d7b35daf0b..5c7ab0d34064f8 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -26,6 +26,8 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do let mut allModules := #[] for s in ["Archive.lean", "Counterexamples.lean", "Mathlib.lean"] do allModules := allModules.append ((← IO.FS.lines s).map (·.stripPrefix "import ")) + -- note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually + allModules := allModules.erase "Batteries" let numberErrorFiles ← lintModules allModules mode (args.hasFlag "fix") -- Make sure to return an exit code of at most 125, so this return value can be used further -- in shell scripts. diff --git a/scripts/lint-style.py b/scripts/lint-style.py index 1482ca2937b728..b8b0ed4779a5b4 100755 --- a/scripts/lint-style.py +++ b/scripts/lint-style.py @@ -40,6 +40,7 @@ ERR_MOD = 2 # module docstring ERR_IBY = 11 # isolated by ERR_IWH = 22 # isolated where +ERR_DOT = 12 # isolated or low focusing dot ERR_SEM = 13 # the substring " ;" ERR_WIN = 14 # Windows line endings "\r\n" ERR_TWS = 15 # trailing whitespace @@ -263,6 +264,11 @@ def isolated_by_dot_semicolon_check(lines, path): line = f"{indent}{line.lstrip()[3:]}" elif line.lstrip() == "where": errors += [(ERR_IWH, line_nr, path)] + if line.lstrip().startswith(". "): + errors += [(ERR_DOT, line_nr, path)] + line = line.replace(". ", "· ", 1) + if line.strip() in (".", "·"): + errors += [(ERR_DOT, line_nr, path)] if " ;" in line: errors += [(ERR_SEM, line_nr, path)] line = line.replace(" ;", ";") @@ -312,6 +318,8 @@ def format_errors(errors): output_message(path, line_nr, "ERR_IBY", "Line is an isolated 'by'") if errno == ERR_IWH: output_message(path, line_nr, "ERR_IWH", "Line is an isolated where") + if errno == ERR_DOT: + output_message(path, line_nr, "ERR_DOT", "Line is an isolated focusing dot or uses . instead of ·") if errno == ERR_SEM: output_message(path, line_nr, "ERR_SEM", "Line contains a space before a semicolon") if errno == ERR_WIN: diff --git a/scripts/nolints-style.txt b/scripts/nolints-style.txt index f388fa06afb149..d9caf2591a8684 100644 --- a/scripts/nolints-style.txt +++ b/scripts/nolints-style.txt @@ -24,9 +24,9 @@ Mathlib/Tactic/AdaptationNote.lean : line 21 : ERR_ADN : Found the string "Adapt 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 20 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead -Mathlib/Tactic/Linter/TextBased.lean : line 49 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead -Mathlib/Tactic/Linter/TextBased.lean : line 84 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead -Mathlib/Tactic/Linter/TextBased.lean : line 274 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead -Mathlib/Tactic/Linter/TextBased.lean : line 279 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead -Mathlib/Tactic/Linter/TextBased.lean : line 280 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead +#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