feat: mark predefinitions that failed to compile as noncomputable#2610
Closed
alexjbest wants to merge 1 commit intoleanprover:masterfrom
Closed
feat: mark predefinitions that failed to compile as noncomputable#2610alexjbest wants to merge 1 commit intoleanprover:masterfrom
alexjbest wants to merge 1 commit intoleanprover:masterfrom
Conversation
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 1, 2023
Contributor
Author
|
awaiting-review |
|
kim-em
approved these changes
Oct 2, 2023
kim-em
reviewed
Oct 2, 2023
Comment on lines
+125
to
126
| if preDef.modifiers.isNoncomputable || !didCompile then | ||
| modifyEnv fun env => addNoncomputable env preDef.declName |
Collaborator
There was a problem hiding this comment.
This means that all theorems will now be marked as noncomputable, whereas before they were not so marked. While it's unclear how much that matters, I think it would be good to not change things unnecessarily (and moreover, it would be great if we could have sufficiently thorough tests here that such changes are trivial to notice!)
Contributor
Author
There was a problem hiding this comment.
I agree that this is not ideal. I will rewrite it and add more tests, as always I failed to anticipate this potential issue.
I think this is yet another instance where a "library diff" tool would have been very revealing!
20 tasks
Contributor
|
I'm going to close this old PR in favor of #9021. |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
External Contribution Guidelines.
Currently definitions inside a noncomputable section that fail to compile are not explicitly tagged as noncomputable.
A noncomputable section simply attempts to compile all definitions but returns false instead of erroring when a compilation error is encountered, however this information is discarded in
addNonRecAux.It seems more useful for downstream tactics / users for the fact that compilation failed to be recorded by tagging the definition with
noncomputable.For example the
to_additivetactic in mathlib will always try to compile declarations generated from not noncomputable multiplicative versions, which means that currently to_additive breaks insidenoncomputable sections see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/noncomputable.20and.20to_additive/near/394068118, this particular issue could be dealt with downstream, but adding the noncomputable tag seems to be the cleanest implementation to me.