Linter errors in Batteries.Data.Nat.Basic

Stream: mathlib4

[Stepan Nesterov]

Currently two of my PRs https://github.com/leanprover-community/mathlib4/pull/33216 and https://github.com/leanprover-community/mathlib4/pull/32856 fail CI with the following error messages:
Run cd pr-branch

https://github.com/leanprover-community/mathlib4/actions/runs/20762061739/job/59619298310?pr=33216#step:37:10+ cd pr-branch

https://github.com/leanprover-community/mathlib4/actions/runs/20762061739/job/59619298310?pr=33216#step:37:11+ env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --trace Mathlib

https://github.com/leanprover-community/mathlib4/actions/runs/20762061739/job/59619298310?pr=33216#step:37:12✔ [19/22] Built Batteries.Data.Array.Basic:c.o (272ms)

https://github.com/leanprover-community/mathlib4/actions/runs/20762061739/job/59619298310?pr=33216#step:37:13✔ [20/22] Built runLinter (740ms)

https://github.com/leanprover-community/mathlib4/actions/runs/20762061739/job/59619298310?pr=33216#step:37:14✔ [21/22] Built runLinter:c.o (513ms)

https://github.com/leanprover-community/mathlib4/actions/runs/20762061739/job/59619298310?pr=33216#step:37:15✔ [22/22] Built runLinter:exe (526ms)

https://github.com/leanprover-community/mathlib4/actions/runs/20762061739/job/59619298310?pr=33216#step:37:16Error parsing args: cannot parse arguments

https://github.com/leanprover-community/mathlib4/actions/runs/20762061739/job/59619298310?pr=33216#step:37:17Usage: runLinter [--update] [Batteries.Data.Nat.Basic]

https://github.com/leanprover-community/mathlib4/actions/runs/20762061739/job/59619298310?pr=33216#step:37:18Error: Process completed with exit code 1.

Run cd pr-branch

https://github.com/leanprover-community/mathlib4/actions/runs/20759862483/job/59611659969?pr=33680#step:37:10+ cd pr-branch

https://github.com/leanprover-community/mathlib4/actions/runs/20759862483/job/59611659969?pr=33680#step:37:11+ env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --trace Mathlib

https://github.com/leanprover-community/mathlib4/actions/runs/20759862483/job/59611659969?pr=33680#step:37:12✔ [19/22] Built Batteries.Data.Array.Basic:c.o (267ms)

https://github.com/leanprover-community/mathlib4/actions/runs/20759862483/job/59611659969?pr=33680#step:37:13✔ [20/22] Built runLinter (777ms)

https://github.com/leanprover-community/mathlib4/actions/runs/20759862483/job/59611659969?pr=33680#step:37:14✔ [21/22] Built runLinter:c.o (489ms)

https://github.com/leanprover-community/mathlib4/actions/runs/20759862483/job/59611659969?pr=33680#step:37:15✔ [22/22] Built runLinter:exe (493ms)

https://github.com/leanprover-community/mathlib4/actions/runs/20759862483/job/59611659969?pr=33680#step:37:16Error parsing args: cannot parse arguments

https://github.com/leanprover-community/mathlib4/actions/runs/20759862483/job/59611659969?pr=33680#step:37:17Usage: runLinter [--update] [Batteries.Data.Nat.Basic]

https://github.com/leanprover-community/mathlib4/actions/runs/20759862483/job/59611659969?pr=33680#step:37:18Error: Process completed with exit code 1.

What does this mean and how do I fix it?

[Bryan Gin-ge Chen]

The errors are happening because CI is trying to run a version of the linters that is newer than the ones are in your branch. They should go away if you merge the latest master into your branch.

[Stepan Nesterov]

Alright all checks have passes thank you :tada:

[Kim Morrison]

@Bryan Gin-ge Chen, #33691 adds scripts/find-ci-errors.sh, which you can run as ./scripts/find-ci-errors.sh "Error parsing args: cannot parse arguments", to identify all PRs that are currently failing, and contain a given string in their output (we could upgrade this to regexes, etc, if desirable). The flag --please-merge-master adds that (newly created) label to all identified PRs. When CI passes that label is automatically cleared. I've just run the script on this linter problem, resulting in 5 label additions.