Skip to content

Conversation

@chenson2018
Copy link
Collaborator

This PR adds environment linters to our testing, including one I have written to check that all new declarations fall under either an existing upstream or Cslib namespace. The remaining environment linters are from Batteries. I have left a few commented out that currently fail and could be addressed in follow-up PRs. Note that we can ignore individual failures with nolint.

Regarding performance, this seems practical when limited to the Cslib namespace. It is now taking ~25s for me to run lake test locally on the freshly built repo.

@chenson2018 chenson2018 requested a review from fmontesi as a code owner October 23, 2025 21:53
@fmontesi fmontesi merged commit f39bbcf into leanprover:main Oct 24, 2025
3 checks passed
fmontesi pushed a commit that referenced this pull request Oct 29, 2025
This PR adds almost all the lints that were left commented out in #123.
All that remains is documentation linting and `explicitVarsOfIff` which
I felt might be too opinionated.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants