Fix merge; remove cdot changes.

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

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.

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:

scripts/nolints-style.txt

@@ -24,9 +24,8 @@ 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
+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