lean4
lean4 copied to clipboard
leanprover
Linters
We need many different linters.
- Style violations.
- Common mistakes.
- Bad idioms.
- Potential performance problems.
The different linters can be developed independently of each other, and they are self-contained projects. Core developers will help with the API and integration.
Do you want linters for the Lean or C++ code (or both)?
For the C++ code, it wouldn't be very difficult for me to add tools like clang-tidy and cppcheck to the build.
They could be triggered to only run when CMAKE_BUILD_TYPE=DEBUG, for example.
It has been a while since this issue was posted. If you're aware of any Lean targeted linters, I'd like to take a look.
Mathlib has a linter framework: https://leanprover-community.github.io/mathlib_docs/commands.html#linting%20commands . Some of this should probably be incorporated into the core lean 4 distribution, but the details have not been worked out. (My impression is that the issue is primarily about Lean linters, as the C++ code is foundational and both user code and the elaborator itself are mostly written in lean.)
Let's close this issue now that the linter framework has been implemented, and reopen issues for specific linters.