Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - fix(lint-style): make sure Python style errors fail the linting step; fix --fix mode #15954

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - fix(lint-style): make sure Python style errors fail the linting step; fix --fix mode #15954

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
24514a4
fix(lint-style): make sure Python style errors fail the build
grunweg Aug 19, 2024
ec00e4b
Fix indentation error.
grunweg Aug 19, 2024
5841546
Fix print-style-errors.sh.
grunweg Aug 19, 2024
0f720b5
Bad test changes.
grunweg Aug 19, 2024
1f298b3
Auto-fixing works! \o/
grunweg Aug 19, 2024
4ae9f71
Undo test change
grunweg Aug 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Mathlib/Geometry/Manifold/Instances/Real.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 5 additions & 3 deletions Mathlib/Tactic/Linter/TextBased.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions scripts/print-style-errors.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading