feat: linter.loopingSimpArgs #8865
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 20, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 20, 2025
…achim/simp-arg-elab
…chim/simp-arg-elab
girray/Lemmas.lean
…achim/simp-loop-detection2
Merged
github-merge-queue bot
pushed a commit
that referenced
this pull request
Jun 22, 2025
This PR factors out the common code for running `SimpM` from `mainCore` and `dsimpMainCore`, and make it available separately (e.g. for #8865).
ec22de4 to
a17b098
Compare
wkrozowski
pushed a commit
to wkrozowski/lean4
that referenced
this pull request
Jun 24, 2025
This PR factors out the common code for running `SimpM` from `mainCore` and `dsimpMainCore`, and make it available separately (e.g. for leanprover#8865).
wkrozowski
pushed a commit
to wkrozowski/lean4
that referenced
this pull request
Jun 24, 2025
This PR allows `simp` to recognize and warn about simp lemmas that are likely looping in the current simp set. It does so automatically whenever simplification fails with the dreaded “max recursion depth” error fails, but it can be made to do it always with `set_option linter.loopingSimpArgs true`. This check is not on by default because it is somewhat costly, and can warn about simp calls that still happen to work. This closes leanprover#5111. In the end, this implemented much simpler logic than described there (and tried in the abandoned leanprover#8688; see that PR description for more background information), but it didn’t work as well as I thought. The current logic is: “Simplify the RHS of the simp theorem, complain if that fails”. It is a reasonable policy for a Lean project to say that all simp invocation should be so that this linter does not complain. Often it is just a matter of explicitly disabling some simp theorems from the default simp set, to make it clear and robust that in this call, we do not want them to trigger. But given that often such simp call happen to work, it’s too pedantic to impose it on everyone.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR allows
simpto recognize and warn about simp lemmas that are likely looping in the current simp set. It does so automatically whenever simplification fails with the dreaded “max recursion depth” error fails, but it can be made to do it always withset_option linter.loopingSimpArgs true. This check is not on by default because it is somewhat costly, and can warn about simp calls that still happen to work.This closes #5111. In the end, this implemented much simpler logic than described there (and tried in the abandoned #8688; see that PR description for more background information), but it didn’t work as well as I thought. The current logic is:
“Simplify the RHS of the simp theorem, complain if that fails”.
It is a reasonable policy for a Lean project to say that all simp invocation should be so that this linter does not complain. Often it is just a matter of explicitly disabling some simp theorems from the default simp set, to make it clear and robust that in this call, we do not want them to trigger. But given that often such simp call happen to work, it’s too pedantic to impose it on everyone.