fix(lint-style): make sure Python style errors fail the linting step;…

… fix --fix mode (#15954)

We need to pass any --fix flag down to `lint-style.py`; this detail got lost along the rewrite.

While at it, tweak the formatting of error messages slightly: avoid an extra newline after the Python output,
and pluralise errors more correctly.

Mathlib/Geometry/Manifold/Instances/Real.lean

@@ -180,7 +180,7 @@ scoped[Manifold]
       ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n))
 
 lemma range_modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] :
-  range (𝓡∂ n) = { y | 0 ≤ y 0 } := range_euclideanHalfSpace n
+    range (𝓡∂ n) = { y | 0 ≤ y 0 } := range_euclideanHalfSpace n
 
 lemma interior_range_modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] :
     interior (range (𝓡∂ n)) = { y | 0 < y 0 } := by

Mathlib/Tactic/Linter/TextBased.lean

@@ -457,10 +457,12 @@ def lintModules (moduleNames : Array String) (mode : OutputSetting) (fix : Bool)
     -- or wait until lint-style.py is fully rewritten in Lean.
     let args := if fix then #["--fix"] else #[]
     let pythonOutput ← IO.Process.run { cmd := "./scripts/print-style-errors.sh", args := args }
-    if pythonOutput != "" then IO.println pythonOutput
+    if pythonOutput != "" then
+      numberErrorFiles := numberErrorFiles + 1
+      IO.print pythonOutput
     formatErrors allUnexpectedErrors style
-    if numberErrorFiles > 0 && mode matches OutputSetting.print _ then
-      IO.println s!"error: found {allUnexpectedErrors.size} new style errors\n\
+    if allUnexpectedErrors.size > 0 && mode matches OutputSetting.print _ then
+      IO.println s!"error: found {allUnexpectedErrors.size} new style error(s)\n\
         run `lake exe lint-style --update` to ignore all of them"
   | OutputSetting.update =>
     formatErrors allUnexpectedErrors ErrorFormat.humanReadable

scripts/print-style-errors.sh

@@ -6,6 +6,6 @@
 
 # use C locale so that sorting is the same on macOS and Linux
 # see https://unix.stackexchange.com/questions/362728/why-does-gnu-sort-sort-differently-on-my-osx-machine-and-linux-machine
-find Mathlib -name '*.lean' | xargs ./scripts/lint-style.py | LC_ALL=C sort
-find Archive -name '*.lean' | xargs ./scripts/lint-style.py | LC_ALL=C sort
-find Counterexamples -name '*.lean' | xargs ./scripts/lint-style.py | LC_ALL=C sort
+find Mathlib -name '*.lean' | xargs ./scripts/lint-style.py "$@" | LC_ALL=C sort
+find Archive -name '*.lean' | xargs ./scripts/lint-style.py "$@" | LC_ALL=C sort
+find Counterexamples -name '*.lean' | xargs ./scripts/lint-style.py "$@" | LC_ALL=C sort