Having done a lot of project maintenance and written a lot of python code, I have many opinions about both. I looked at scripts/lint-style.py and immediately thought of ~5-10 refactoring tasks, from the cosmetic to updating to the contemporary state of defensible python:
- Full mypy strict typing
- Chained
if/elif/else -> case/match and assignment operator (:=)
- (unit tests might seem overbearing for tooling, but to use the favorite wording of Claude, there's a high cost of wrong here)
- (pydantic dependency probably also undesirable unless we're willing to require
uv for project management of pythonic components, however pydantic would allow for a very easy, defensible, and conventional way to validate input data contracts, for example, style-exceptions.txt. Given how much string scraping lint-style.py is doing, pydantic would be a significant improvement)
- If python code, even as maintenance tooling, we probably would want a
pyproject.toml anyway with
[tool.ruff.lint]
select = ["E", "W", "F", "I", "N", "UP", "B", "C4", "SIM", "TID", "RUF"]
- Business logic leaking out of python into sidecar shell scripts
s/argv/argparse/gif __name__ == "__main__"
However
A comment near the top of the file says, "This is adapted from the linter for mathlib3. It should be rewritten in Lean," implying at least two constraints on the problems and the strategy of their solutions:
- What is the project coupling strength to mathlib(4)? Should we work within their conventions, specifically
- This entire file should be rewritten in lean, basically invalidating or at least dead ending any python improvements?
I'm not very familiar with lean yet, so can't judge the linting usecase or hammer-finding-nails signal. It's usually better for a language's own ecosystem to evaluate and manage style and formatting issues natively. For example: black, isort, pyupgrade, mypy for python, rustfmt, clippy, cargo-audit for rust, gofmt, go vet, goimports for go. Perhaps there's nothing to do here but instrument whatever that is, or contribute to lean tooling directly.
Having done a lot of project maintenance and written a lot of python code, I have many opinions about both. I looked at
scripts/lint-style.pyand immediately thought of ~5-10 refactoring tasks, from the cosmetic to updating to the contemporary state of defensible python:if/elif/else->case/matchand assignment operator (:=)uvfor project management of pythonic components, however pydantic would allow for a very easy, defensible, and conventional way to validate input data contracts, for example,style-exceptions.txt. Given how much string scrapinglint-style.pyis doing, pydantic would be a significant improvement)pyproject.tomlanyway withs/argv/argparse/gif __name__ == "__main__"However
A comment near the top of the file says, "This is adapted from the linter for mathlib3. It should be rewritten in Lean," implying at least two constraints on the problems and the strategy of their solutions:
I'm not very familiar with lean yet, so can't judge the linting usecase or hammer-finding-nails signal. It's usually better for a language's own ecosystem to evaluate and manage style and formatting issues natively. For example:
black,isort,pyupgrade,mypyfor python,rustfmt,clippy,cargo-auditfor rust,gofmt,go vet,goimportsfor go. Perhaps there's nothing to do here but instrument whatever that is, or contribute to lean tooling directly.