Skip to content

perf: improve some instances in LinearMap#7554

Closed
ChrisHughes24 wants to merge 9 commits intomasterfrom
LinearMapPerfCH
Closed

perf: improve some instances in LinearMap#7554
ChrisHughes24 wants to merge 9 commits intomasterfrom
LinearMapPerfCH

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member

@ChrisHughes24 ChrisHughes24 commented Oct 6, 2023

Open in Gitpod

@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Oct 6, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Oct 6, 2023

Here are the benchmark results for commit d224570.
There were significant changes against commit e2c210a:

  Benchmark                                               Metric         Change
  =============================================================================
- build                                                   wall-clock      16.1%
+ ~Mathlib.Algebra.Category.FGModuleCat.Basic             instructions   -76.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Algebra             instructions    -9.4%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed     instructions   -14.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Presheaf            instructions    -6.5%
- ~Mathlib.Algebra.DirectSum.Module                       instructions    17.7%
+ ~Mathlib.Algebra.Lie.Engel                              instructions    -5.3%
+ ~Mathlib.Algebra.Lie.Matrix                             instructions   -30.1%
+ ~Mathlib.Algebra.Lie.TensorProduct                      instructions   -10.9%
+ ~Mathlib.Algebra.RingQuot                               instructions    -5.9%
+ ~Mathlib.FieldTheory.Tower                              instructions    -8.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv        instructions    -7.3%
+ ~Mathlib.LinearAlgebra.Dual                             instructions   -28.0%
+ ~Mathlib.LinearAlgebra.Eigenspace.Minpoly               instructions   -11.7%
+ ~Mathlib.LinearAlgebra.FreeModule.PID                   instructions   -19.9%
+ ~Mathlib.LinearAlgebra.FreeModule.StrongRankCondition   instructions   -70.2%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap        instructions    -9.4%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly          instructions   -42.9%
+ ~Mathlib.LinearAlgebra.Matrix.FiniteDimensional         instructions    -5.7%
+ ~Mathlib.LinearAlgebra.Trace                            instructions   -14.4%
+ ~Mathlib.RepresentationTheory.Character                 instructions   -20.0%
+ ~Mathlib.RepresentationTheory.FdRep                     instructions   -37.2%
+ ~Mathlib.RepresentationTheory.Rep                       instructions    -6.1%
+ ~Mathlib.RingTheory.Derivation.Lie                      instructions    -9.1%
+ ~Mathlib.RingTheory.Kaehler                             instructions    -5.6%

eric-wieser
eric-wieser reviewed Oct 7, 2023
View reviewed changes
@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Oct 7, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Oct 7, 2023

Here are the benchmark results for commit 38c3501.
There were significant changes against commit e2c210a:

  Benchmark                                                           Metric         Change
  =========================================================================================
+ ~Mathlib.Algebra.Category.FGModuleCat.Basic                         instructions   -76.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Algebra                         instructions    -9.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed                 instructions   -14.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Presheaf                        instructions    -6.5%
- ~Mathlib.Algebra.DirectSum.Module                                   instructions    10.5%
+ ~Mathlib.Algebra.Lie.Engel                                          instructions    -5.3%
+ ~Mathlib.Algebra.Lie.Matrix                                         instructions   -30.1%
+ ~Mathlib.Algebra.Lie.TensorProduct                                  instructions   -11.0%
- ~Mathlib.Algebra.Lie.Weights                                        instructions     5.9%
+ ~Mathlib.Algebra.RingQuot                                           instructions    -5.9%
- ~Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit   instructions     5.2%
+ ~Mathlib.FieldTheory.Tower                                          instructions    -8.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                    instructions    -7.2%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct                      instructions   -10.0%
+ ~Mathlib.LinearAlgebra.Dual                                         instructions   -28.0%
+ ~Mathlib.LinearAlgebra.Eigenspace.Minpoly                           instructions   -11.6%
+ ~Mathlib.LinearAlgebra.FreeModule.PID                               instructions    -7.0%
+ ~Mathlib.LinearAlgebra.FreeModule.StrongRankCondition               instructions   -70.2%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap                    instructions    -9.4%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly                      instructions   -43.0%
+ ~Mathlib.LinearAlgebra.Matrix.FiniteDimensional                     instructions    -5.6%
+ ~Mathlib.LinearAlgebra.Trace                                        instructions   -14.3%
+ ~Mathlib.RepresentationTheory.Character                             instructions   -20.0%
+ ~Mathlib.RepresentationTheory.FdRep                                 instructions   -37.2%
+ ~Mathlib.RepresentationTheory.Rep                                   instructions    -6.2%
+ ~Mathlib.RingTheory.Derivation.Lie                                  instructions    -9.2%
+ ~Mathlib.RingTheory.Kaehler                                         instructions    -5.6%

@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Oct 7, 2023

Speed diff for the last commit (changing the module instance)

@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Oct 16, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Oct 16, 2023

Here are the benchmark results for commit 9b1b63b.
There were significant changes against commit 38db825:

  Benchmark                                                  Metric         Change
  ================================================================================
+ ~Mathlib.Algebra.Category.AlgebraCat.Monoidal              instructions    -3.7%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings          instructions    -3.4%
+ ~Mathlib.Algebra.Lie.TensorProduct                         instructions   -14.4%
+ ~Mathlib.Analysis.NormedSpace.Multilinear                  instructions    -2.0%
+ ~Mathlib.CategoryTheory.Abelian.InjectiveResolution        instructions    -2.2%
- ~Mathlib.FieldTheory.RatFunc                               instructions     2.2%
+ ~Mathlib.LinearAlgebra.Dual                                instructions    -9.5%
+ ~Mathlib.RepresentationTheory.Character                    instructions   -12.7%
- ~Mathlib.RepresentationTheory.GroupCohomology.Resolution   instructions     6.9%

@digama0
Copy link
Copy Markdown
Member

digama0 commented Oct 21, 2023

Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause lake clean to delete your mathlib folder! If you need to do so, make sure to delete lakefile.olean manually before running any lake commands.

@ChrisHughes24 ChrisHughes24 mentioned this pull request Oct 23, 2023
Closed
@ChrisHughes24 ChrisHughes24 added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Oct 25, 2023
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 31, 2023
@YaelDillies YaelDillies deleted the LinearMapPerfCH branch August 12, 2025 05:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

Assignees

No one assigned

Labels

awaiting-author A reviewer has asked the author a question or requested changes. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@ChrisHughes24 @leanprover-bot @digama0 @eric-wieser