benchmark leanprover/lean4#13637 adaptations#250
Merged
Conversation
Lean PR leanprover/lean4#13637 splits `@[implicit_reducible]` into `@[instance_reducible]` (TC tier) and `@[implicit_reducible]` (implicit-arg defeq tier). `instance` auto-stamps `.instanceReducible`, but `to_additive` calls `addInstance` directly for the additive copy, so the auto-stamp doesn't fire on the target. Extend `copyInstanceAttribute` to copy `.instanceReducible` in addition to the pre-existing `.implicitReducible`. Fixes the cascade in `Mathlib/Algebra/CharZero/Defs.lean`, `Ring/Defs.lean`, `AddTorsor/Defs.lean`, `Homology/HasNoLoop.lean`, `Matrix/DMatrix.lean`, `Group/Basic.lean`, `Group/WithOne/Defs.lean`, and `Order/Lattice.lean`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Lean PR leanprover/lean4#13637 splits the unified `@[implicit_reducible]` into two tiers: * `@[instance_reducible]` — unfolds during type class search (the new `.instances` tier), used for declarations that participate in instance forwarding chains. * `@[implicit_reducible]` — unfolds only during implicit value-argument defeq (the new `.implicit` tier), used for narrower cases like functor laws. Most Mathlib uses of `@[implicit_reducible]` were on "reducible non-instance" helpers (`Function.Injective.distribLattice`, `SemilatticeSup.mk'`, `Lattice.mk'`, all of `Order/Copy.lean`, `Denumerable.mk'`, `Set.monoid`, `CreatesLimitOf*`, etc.) that build typeclass instances. Under the new semantics these must be tagged `@[instance_reducible]` for type class search to unfold them. This commit replaces all 818 `@[implicit_reducible]` annotations (including the 110 inline `(attr := implicit_reducible ...)` forms inside `@[to_additive]` / `@[to_dual]`) with `@[instance_reducible]` across the library. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…Archive and tests Complements the main migration in Mathlib/ by covering the remaining sites in Archive/ and MathlibTest/. * Archive/Imo/Imo2019Q2.lean * Archive/MinimalSheffer.lean * MathlibTest/DefEqAbuse.lean * MathlibTest/InferInstanceAsPercent.lean (also updates the docstring expectations to reflect the new attribute name that `instance` now auto-stamps) * MathlibTest/fast_instance.lean (same docstring update) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…le]` tier split Adapted from Sébastien Gouëzel's MWE on Zulip [1]. Pins three claims about the tier split introduced in lean#13637: 1. Without any extra attribute, TC search distinguishes the two `SGMonoidal` instances at `F ⋙ (G ⋙ H)` and `(F ⋙ G) ⋙ H`, so an `rfl` between their `n` fields rightfully fails. 2. Tagging `Functor.comp` `[implicit_reducible]` (the narrower value-defeq-only tier) does NOT corrupt the above — the `[implicit_reducible]` corruption Sébastien warned about is gone. 3. Tagging `Functor.comp` `[instance_reducible]` (the TC tier) deliberately reproduces the pre-split corruption: `rfl` succeeds even though the two instances are mathematically distinct. This pins the upper-bound semantics — if a future change accidentally narrowed `[instance_reducible]`, this case would notice. [1]: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency/near/592439262 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The toolchain update changes when `[backward_defeq]` is being used. Previously, it was used whenever a rfl lemma wasn't well-typed at instances. Now, it's used whenever it isn't well-typed at implicit. This broke a few lemmas because proofs were relying on some perfectly good rfl lemmas not being applied. In some cases, applying them triggered the application of some *bad* rfl lemmas.
Author
|
!radar |
|
Benchmark results for 57ad03e against 49e2071 are in. There are significant results. @datokrat Warning These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.
Medium changes (3🟥)
Small changes (4✅, 76🟥) Too many entries to display here. View the full report on radar instead. |
datokrat
force-pushed
the
lean-pr-testing-13637
branch
from
57ad03e to
44118da
Compare
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
5 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.
No description provided.