feat: have IR checker suggest noncomputable
#4729
Merged
Conversation
This file contains 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
|
@leodemoura Keven Buzzard was telling me today that he has to frequently help people with this IR compiler check issue. I'm not sure if this is the correct fix, but putting this error message is this particular place seemed potentially appropriate after studying If anything, this PR contains a simpler version of the test case at #1785. Note that removing the typeclass argument makes |
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Currently, `ll_infer_type` is responsible for telling the user about `noncomputable` when a definition depends on one without executable code. However, this is imperfect because type inference does not check every subexpression. This leads to errors later on that users find to be hard to interpret. Now, `Lean.IR.checkDecls` has a friendlier error message when it encounters constants without compiled definitions, suggesting to consider using `noncomputable`. While this function is an internal IR consistency check, it is also reasonable to have it give an informative error message in this particular case. The suggestion to use `noncomputable` is limited to just unknown constants. Some alternatives would be to either (1) create another checker just for missing constants, (2) change `ll_infer_type` to always visit every subexpression no matter if they are necessary for inferring the type, or (3) investigate whether `tests/lean/run/1785.lean` is due to a deeper issue. Closes leanprover#1785
kmill
force-pushed
the
compiler_check_noncomputable
branch
from
fb07ecf to
0820de5
Compare
tobiasgrosser
pushed a commit
to opencompl/lean4
that referenced
this pull request
Sep 16, 2024
Currently, `ll_infer_type` is responsible for telling the user about `noncomputable` when a definition depends on one without executable code. However, this is imperfect because type inference does not check every subexpression. This leads to errors later on that users find to be hard to interpret. Now, `Lean.IR.checkDecls` has a friendlier error message when it encounters constants without compiled definitions, suggesting to consider using `noncomputable`. While this function is an internal IR consistency check, it is also reasonable to have it give an informative error message in this particular case. The suggestion to use `noncomputable` is limited to just unknown constants. Some alternatives would be to either (1) create another checker just for missing constants, (2) change `ll_infer_type` to always visit every subexpression no matter if they are necessary for inferring the type, or (3) investigate whether `tests/lean/run/1785.lean` is due to a deeper issue. Closes leanprover#1785
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.
Currently,
ll_infer_typeis responsible for telling the user aboutnoncomputablewhen a definition depends on one without executable code. However, this is imperfect because type inference does not check every subexpression. This leads to errors later on that users find to be hard to interpret.Now,
Lean.IR.checkDeclshas a friendlier error message when it encounters constants without compiled definitions, suggesting to consider usingnoncomputable. While this function is an internal IR consistency check, it is also reasonable to have it give an informative error message in this particular case. The suggestion to usenoncomputableis limited to just unknown constants.Some alternatives would be to either (1) create another checker just for missing constants, (2) change
ll_infer_typeto always visit every subexpression no matter if they are necessary for inferring the type, or (3) investigate whethertests/lean/run/1785.leanis due to a deeper issue.Closes #1785