feat: add linter

[markusdemedeiros]

Description

Adds the batteries linter to the project. This should not be merged until the linter is fully configured and the code passes lint.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.
Please carefully review your code to ensure it meets the following standards.

• Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
• have statements that do not aid readability or code reuse should be inlined.
• Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
• In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.
We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.

[Kaptch]

Is it possible to configure the linter to ignore some files, so that we gradually change them to meet the standards? I am bit worried of bulk changes, especially if it is not only formatting.

[Kaptch]

Seems it is possible. Then I would propose to ignore existing files in the very beginning, require passing linter from future PRs, and add chore to make old files pass the linter gradually, similar what is done with Rocq annotations.

[markusdemedeiros]

That is a good idea! We should still discuss the linting rules we want to follow beforehand, but I agree with a gradual rollout.

[alvinylt]

I have been doing some testing with the linters in the branch on top of this PR (see diff).

Since last month (Lean 4.32.0) there has been changes to lake lint. We can now run the built-in linter for particular submodules.

Batteries' linter is different though: with the configurations under [leanOptions] in lakefile.toml, the linter warnings are enabled throughout the project. But I reckon the trickiest part is the code style linter as it lives within the Mathlib repository. The linter does not depend on other Mathlib modules, so it's relatively easy to have it in our repository. But I still have not figured out how to organise things nicely.