fix: type class issues with maxSynthPendingDepth := 1
#4119
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
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 10, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 10, 2024
leanprover-community-mathlib4-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 10, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 10, 2024
leanprover-community-mathlib4-bot
added
builds-mathlib
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 11, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 11, 2024
leanprover-community-mathlib4-bot
added
breaks-mathlib
|
(Mathlib build will come good again after the toolchain rebuilds after the rebase ... It's okay locally so likely I'll merge this without waiting for a final check.) |
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 14, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 14, 2024
Closed
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 14, 2024
The main underlying change here is leanprover/lean4#4119, which fixed a number of typeclass search bugs. In particular, it fixed a caching bug (the `synthPendingDepth` was being ignored during caching, resulting in both false positive and false negatives). For the false positives (i.e. things that synthesis was finding that it really shouldn't have been!), we've had to introduce `set_option maxSynthPendingDepth 2 in` in places. These are all explained with `#adaptation_notes`. There's also leanprover/lean4#4061, which makes well-founded definitions irreducible by default. This helps avoid some horrible run-away unfoldings, and was surprisingly un-painful to Mathlib to (credit to @nomeata for discovering this!) There are some minor adaptations still required, however. --------- Co-authored-by: sgouezel <[email protected]>
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.
Summary:
synthPendingDepthinto account when caching TC resultsmaxSynthPendingDepthoption with default := 2.synthPendingfailures when usingset_option diagnostics truecloses #2522
closes #3313
closes #3927
Identical to #4114 but with
maxSynthPendingDepth := 1closes #4114
cc @semorrison