New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(*): restore subsingleton
instances and remove hacks
#16046
Conversation
There's one place where an earlier |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
Thanks 🎉 bors merge |
#### Background The `simp` tactic used to [look for subsingleton instances excessively](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223034551), so every subsingleton/unique instances added to mathlib could slow down `simp` performance; in fact, removing some subsingleton instances locally led to such speedup that three hacks #5779, #5878 and #6639 along this line have been merged into mathlib. Since the problem was discovered, new subsingleton instances were mostly turned into lemma/defs, with a reference to gh-6025 that @eric-wieser created to track them and a notice to restore them as instances once safe to do so. This bad behavior of `simp` was finally fixed in [lean#665](leanprover-community/lean#665) by @gebner in January 2022, so it is now safe to remove the hacks and restore the instances. In fact, the hack #5878 was already removed in [#13127](c7626b7#diff-02976f8e19552b3c7ea070e30761e4e99f1333085cc5bb94fa170861c6ed27bcL497). I [measured the difference in performance](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/293228091) from removing one of the remaining hacks and it was negligible. Therefore, in this PR, we: + Remove both hacks remaining; + Turn all would-be instances that mention gh-6025 into actual global instances; + Golf proofs that explicitly invoked these instances previously; + Remove `local attribute [instance]` lines that were added when these instances were needed. Closes #6025.
Build failed (retrying...): |
#### Background The `simp` tactic used to [look for subsingleton instances excessively](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223034551), so every subsingleton/unique instances added to mathlib could slow down `simp` performance; in fact, removing some subsingleton instances locally led to such speedup that three hacks #5779, #5878 and #6639 along this line have been merged into mathlib. Since the problem was discovered, new subsingleton instances were mostly turned into lemma/defs, with a reference to gh-6025 that @eric-wieser created to track them and a notice to restore them as instances once safe to do so. This bad behavior of `simp` was finally fixed in [lean#665](leanprover-community/lean#665) by @gebner in January 2022, so it is now safe to remove the hacks and restore the instances. In fact, the hack #5878 was already removed in [#13127](c7626b7#diff-02976f8e19552b3c7ea070e30761e4e99f1333085cc5bb94fa170861c6ed27bcL497). I [measured the difference in performance](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/293228091) from removing one of the remaining hacks and it was negligible. Therefore, in this PR, we: + Remove both hacks remaining; + Turn all would-be instances that mention gh-6025 into actual global instances; + Golf proofs that explicitly invoked these instances previously; + Remove `local attribute [instance]` lines that were added when these instances were needed. Closes #6025.
bors merge p=3 |
#### Background The `simp` tactic used to [look for subsingleton instances excessively](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223034551), so every subsingleton/unique instances added to mathlib could slow down `simp` performance; in fact, removing some subsingleton instances locally led to such speedup that three hacks #5779, #5878 and #6639 along this line have been merged into mathlib. Since the problem was discovered, new subsingleton instances were mostly turned into lemma/defs, with a reference to gh-6025 that @eric-wieser created to track them and a notice to restore them as instances once safe to do so. This bad behavior of `simp` was finally fixed in [lean#665](leanprover-community/lean#665) by @gebner in January 2022, so it is now safe to remove the hacks and restore the instances. In fact, the hack #5878 was already removed in [#13127](c7626b7#diff-02976f8e19552b3c7ea070e30761e4e99f1333085cc5bb94fa170861c6ed27bcL497). I [measured the difference in performance](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/293228091) from removing one of the remaining hacks and it was negligible. Therefore, in this PR, we: + Remove both hacks remaining; + Turn all would-be instances that mention gh-6025 into actual global instances; + Golf proofs that explicitly invoked these instances previously; + Remove `local attribute [instance]` lines that were added when these instances were needed. Closes #6025.
Build failed (retrying...): |
#### Background The `simp` tactic used to [look for subsingleton instances excessively](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223034551), so every subsingleton/unique instances added to mathlib could slow down `simp` performance; in fact, removing some subsingleton instances locally led to such speedup that three hacks #5779, #5878 and #6639 along this line have been merged into mathlib. Since the problem was discovered, new subsingleton instances were mostly turned into lemma/defs, with a reference to gh-6025 that @eric-wieser created to track them and a notice to restore them as instances once safe to do so. This bad behavior of `simp` was finally fixed in [lean#665](leanprover-community/lean#665) by @gebner in January 2022, so it is now safe to remove the hacks and restore the instances. In fact, the hack #5878 was already removed in [#13127](c7626b7#diff-02976f8e19552b3c7ea070e30761e4e99f1333085cc5bb94fa170861c6ed27bcL497). I [measured the difference in performance](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/293228091) from removing one of the remaining hacks and it was negligible. Therefore, in this PR, we: + Remove both hacks remaining; + Turn all would-be instances that mention gh-6025 into actual global instances; + Golf proofs that explicitly invoked these instances previously; + Remove `local attribute [instance]` lines that were added when these instances were needed. Closes #6025.
Pull request successfully merged into master. Build succeeded: |
subsingleton
instances and remove hackssubsingleton
instances and remove hacks
…d `mv_polynomial` (#15889) + Show `#(multiset α) = max (#α) ℵ₀` when `α` is nonempty. Show the same for `#(α →₀ ℕ)`, which is used in the mv_polynomial proof (see below). + Prove that the inequality in `polynomial.cardinal_mk_le_max` is an equality when the semiring is nontrivial. The result is no longer derived from the corresponding result for mv_polynomial to allow general `semiring`, not just `comm_semiring`. + Generalize `mv_polynomial.cardinal_mk_le_max` to two possibly different universes, and prove that the inequality is an equality when the type of variables is nonempty and the semiring is nontrivial. W_type is no longer used so that part is removed from the file. + Change the [encodable] assumption in `mk_le_aleph_0` and `mk_list_eq_aleph_0` to the weaker typeclass [countable]. - [x] depends on: #16046
Background
The
simp
tactic used to look for subsingleton instances excessively, so every subsingleton/unique instances added to mathlib could slow downsimp
performance; in fact, removing some subsingleton instances locally led to such speedup that three hacks #5779, #5878 and #6639 along this line have been merged into mathlib. Since the problem was discovered, new subsingleton instances were mostly turned into lemma/defs, with a reference to gh-6025 that @eric-wieser created to track them and a notice to restore them as instances once safe to do so.This bad behavior of
simp
was finally fixed in lean#665 by @gebner in January 2022, so it is now safe to remove the hacks and restore the instances. In fact, the hack #5878 was already removed in #13127. I measured the difference in performance from removing one of the remaining hacks and it was negligible.Therefore, in this PR, we:
Remove both hacks remaining;
Turn all would-be instances that mention Convert subsingleton lemmas to instances #6025 into actual global instances;
Golf proofs that explicitly invoked these instances previously;
Remove
local attribute [instance]
lines that were added when these instances were needed.Closes #6025.