[Merged by Bors] - feat: rewrite the trailing whitespace linter in Lean

[grunweg]

---

[github-actions]

PR summary cae8fabf42

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ trailingWhitespaceLinter
- line_endings_check(lines,

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[adomani]

I have not yet looked at the PR, but batteries#920 also implements a trailing whitespace linter (actually in two different ways). Is there a way of picking one of these three implementations, get it merged somewhere and possibly upstream one to Batteries?

[grunweg]

I know about the linter in batteries! I am not sure if this will ever get merged... so my thinking is to start with a linter here, and refine later if the batteries script gets merged.

In terms of functionality, both do very similar things: the main difference is that this script is integrated with the text-based linters. Batteries has no such infrastructure currently, so needs to invent their own. Mathlib already has something which fits well.
Now, batteries could easily gain such infrastructure (I could uplift the text-based linter functionality there, and wait for it to get merged...), but it's less obvious to me how useful that would be. In summary: unless batteries wants to get such functionality, the effort of designing some ad-hoc infrastructure for running the trailing whitespace script and then figuring out how to use that in mathlib seems much higher than just landing the script here, and manually running it on batteries every now and then.

What do you think? Or should one simply try to upstream the text-based linter infrastructure there?

[adomani]

Before upstreaming the whole text-based setup, it should probably be discussed with the maintainers: this may be a much bigger undertaking and, even if accepted, may take a long time.

I did not have a chance to look at the code, but I would probably suggest to proceed with this one in its current form. I'll try to review it later today.

[grunweg]

Thank you for the careful review, Damiano! I responded to all comments, and am interested in your opinion about my opinion :-)

[grunweg]

I just re-read the discussion: while your suggestions work, I'm not convinced they are better (hence am inclined to leave the code as-is). Let me know if you disagree!

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style