[Merged by Bors] - perf: improve instances in TensorProduct#7401
[Merged by Bors] - perf: improve instances in TensorProduct#7401ChrisHughes24 wants to merge 3 commits intomasterfrom
Conversation
ChrisHughes24
commented
Sep 27, 2023
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
|
!bench |
|
Here are the benchmark results for commit 1a787a0. Benchmark Metric Change
=====================================================================================
+ ~Mathlib.Algebra.Category.FGModuleCat.Basic instructions -24.5%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings instructions -7.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic instructions -54.9%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed instructions -23.5%
+ ~Mathlib.CategoryTheory.Monoidal.Internal.Module instructions -6.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange instructions -8.9%
+ ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries instructions -7.5%
+ ~Mathlib.LinearAlgebra.TensorPower instructions -6.2%
+ ~Mathlib.LinearAlgebra.TensorProduct.Opposite instructions -6.3%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower instructions -9.4%
+ ~Mathlib.RepresentationTheory.Character instructions -5.8%
+ ~Mathlib.RepresentationTheory.FdRep instructions -26.2%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution instructions -7.8%
+ ~Mathlib.RepresentationTheory.Rep instructions -20.6%
+ ~Mathlib.RingTheory.Kaehler instructions -5.6%
+ ~Mathlib.RingTheory.MatrixAlgebra instructions -20.2%
+ ~Mathlib.RingTheory.TensorProduct instructions -8.9% |
Vierkantor
left a comment
There was a problem hiding this comment.
Impressive work!
bors d+
| instance addZeroClass : AddZeroClass (M ⊗[R] N) := | ||
| { (addConGen (TensorProduct.Eqv R M N)).addMonoid with } | ||
| { (addConGen (TensorProduct.Eqv R M N)).addMonoid with | ||
| toAdd := TensorProduct.add _ _ } |
There was a problem hiding this comment.
Could you (in a comment) explain why making the addition explicit is needed? I suppose it's because we want to have the actual ancestor of the class, so unification is faster.
Idem below.
There was a problem hiding this comment.
In fact, there should probably be a library note explaining the optimal way to do this kind of inheritance, since it changed quite a bit since Lean 3.
|
✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
|
This PR was included in a batch that was canceled, it will be automatically retried |
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
|
Build failed (retrying...): |
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
|
Build failed (retrying...): |
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |