diff --git a/Mathlib/Geometry/Manifold/Instances/Real.lean b/Mathlib/Geometry/Manifold/Instances/Real.lean index c5e8fdd7080bb..32997ffec1950 100644 --- a/Mathlib/Geometry/Manifold/Instances/Real.lean +++ b/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 diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean index 3da71f0a028bd..8ad10c1f81f95 100644 --- a/Mathlib/Tactic/Linter/TextBased.lean +++ b/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 diff --git a/scripts/print-style-errors.sh b/scripts/print-style-errors.sh index f9a9e1c1b42c8..0f0ca588e598c 100755 --- a/scripts/print-style-errors.sh +++ b/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