New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(tactic/lint): better fails_quickly linter #8932
Conversation
…e` (#8933) Previously, this instance would first look for `decidable_eq` instances and after that for `is_simple_lattice` instances. The latter has only 4 instances, while the former takes hundreds of steps. Reordering the arguments makes a lot of type-class searches fail a lot quicker. Caught by the new linter (#8932).
This instance causes loop with `is_total_preorder.to_is_total`, and was unused in the library. Caught by the new linter (#8932).
Is the plan to do these as part of this PR, or later? |
The first I sort-of did (by just setting the The status is: we might not fix them in Lean 3 if the Lean 4 loop-checking catches these loops. I haven't done the tests in Lean 4. Even if we're fixing them in Lean 3, it will be in a follow-up PR. |
bors merge |
This linter catches a lot more loops. Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
Pull request successfully merged into master. Build succeeded: |
This reverts commit 4d88ae8.
This linter catches a lot more loops.
TODO:
max_steps
[ ] fix some/all problematic instances it catches