Skip to content

[Merged by Bors] - perf: improve some instances in GroupTheory/Congruence#6874

Closed
ChrisHughes24 wants to merge 6 commits intomasterfrom
ConPerfCH
Closed

[Merged by Bors] - perf: improve some instances in GroupTheory/Congruence#6874
ChrisHughes24 wants to merge 6 commits intomasterfrom
ConPerfCH

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member

@ChrisHughes24 ChrisHughes24 commented Aug 30, 2023

Open in Gitpod

@ChrisHughes24 ChrisHughes24 added WIP Work in progress awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Aug 30, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Aug 30, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Aug 30, 2023

Here are the benchmark results for commit c077c39.
There were significant changes against commit 571a128:

  Benchmark                                                Metric         Change
  ==============================================================================
+ ~Mathlib.Algebra.Category.FGModuleCat.Basic              instructions   -12.9%
+ ~Mathlib.Algebra.Category.GroupCat.Adjunctions           instructions    -5.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Abelian              instructions   -20.5%
+ ~Mathlib.Algebra.Category.ModuleCat.Kernels              instructions    -9.4%
+ ~Mathlib.Algebra.Category.ModuleCat.Limits               instructions   -42.7%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic       instructions   -26.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed      instructions    -6.7%
+ ~Mathlib.Algebra.DirectLimit                             instructions    -7.7%
+ ~Mathlib.Algebra.Lie.TensorProduct                       instructions    -5.4%
+ ~Mathlib.Analysis.Complex.Arg                            instructions    -5.6%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle   instructions   -14.5%
+ ~Mathlib.Dynamics.Ergodic.AddCircle                      instructions   -12.9%
+ ~Mathlib.GroupTheory.CoprodI                             instructions   -11.9%
+ ~Mathlib.LinearAlgebra.Dual                              instructions    -8.9%
+ ~Mathlib.LinearAlgebra.FreeModule.IdealQuotient          instructions   -16.6%
+ ~Mathlib.LinearAlgebra.TensorPower                       instructions   -13.7%
+ ~Mathlib.LinearAlgebra.TensorProduct.Opposite            instructions    -7.0%
+ ~Mathlib.MeasureTheory.Group.AddCircle                   instructions   -20.0%
+ ~Mathlib.NumberTheory.WellApproximable                   instructions   -10.4%
+ ~Mathlib.RepresentationTheory.FdRep                      instructions    -7.3%
+ ~Mathlib.RepresentationTheory.Rep                        instructions    -5.6%
+ ~Mathlib.RingTheory.Ideal.Cotangent                      instructions    -6.2%
+ ~Mathlib.RingTheory.Kaehler                              instructions    -8.3%
+ ~Mathlib.RingTheory.MatrixAlgebra                        instructions    -6.1%

@ChrisHughes24 ChrisHughes24 added awaiting-review and removed WIP Work in progress awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Aug 30, 2023
@ChrisHughes24 ChrisHughes24 mentioned this pull request Aug 30, 2023
Closed
9 tasks
@ChrisHughes24 ChrisHughes24 added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Aug 31, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Aug 31, 2023

I think this can wait until after the related Lean4 issue, and we can see if there is still a benefit to this.

@ChrisHughes24 ChrisHughes24 added blocked-by-core-PR This PR depends on a PR to Core/Std and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Aug 31, 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 Sep 15, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 15, 2023
@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:26
@kim-em kim-em changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:06
@mattrobball mattrobball removed the blocked-by-core-PR This PR depends on a PR to Core/Std label Sep 28, 2023
mattrobball
mattrobball approved these changes Sep 28, 2023
View reviewed changes
Mathlib/GroupTheory/Congruence.lean
@[to_additive "The quotient of an `AddSemigroup` by an additive congruence relation is
an `AddSemigroup`."]
instance semigroup {M : Type*} [Semigroup M] (c : Con M) : Semigroup c.Quotient :=
Function.Surjective.semigroup _ Quotient.surjective_Quotient_mk'' fun _ _ => rfl
Copy link
Copy Markdown
Contributor

@mattrobball mattrobball Sep 28, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think a note explaining situation is good here. I would hope the slowdown in unification we see here (and in related files) can be fixed further up the library. Similarly for the other explicit projections below.

@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Sep 28, 2023

bors d+

I think this is orthogonal to leanprover/lean4#2478 and it would be really nice to have it now without waiting.

@bors
Copy link
Copy Markdown

bors bot commented Sep 28, 2023

✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Sep 28, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Sep 29, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Sep 29, 2023

Here are the benchmark results for commit 36df7f7.
There were significant changes against commit b3b5ba1:

  Benchmark                                                           Metric         Change
  =========================================================================================
+ ~Mathlib.Algebra.Category.GroupCat.Adjunctions                      instructions    -5.2%
+ ~Mathlib.Algebra.Category.GroupCat.Injective                        instructions    -7.5%
+ ~Mathlib.Algebra.Category.ModuleCat.Abelian                         instructions   -20.2%
+ ~Mathlib.Algebra.Category.ModuleCat.Kernels                         instructions    -9.2%
+ ~Mathlib.Algebra.Category.ModuleCat.Limits                          instructions   -42.8%
+ ~Mathlib.Algebra.DirectLimit                                        instructions    -7.5%
+ ~Mathlib.Analysis.Complex.Arg                                       instructions    -5.2%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle              instructions   -13.7%
+ ~Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit   instructions    -5.7%
+ ~Mathlib.Dynamics.Ergodic.AddCircle                                 instructions   -12.2%
+ ~Mathlib.GroupTheory.HNNExtension                                   instructions   -10.1%
+ ~Mathlib.LinearAlgebra.Dual                                         instructions    -8.7%
+ ~Mathlib.LinearAlgebra.FreeModule.IdealQuotient                     instructions   -16.7%
+ ~Mathlib.LinearAlgebra.TensorPower                                  instructions   -12.5%
+ ~Mathlib.MeasureTheory.Group.AddCircle                              instructions   -17.7%
+ ~Mathlib.NumberTheory.WellApproximable                              instructions    -9.1%
+ ~Mathlib.RingTheory.Ideal.Cotangent                                 instructions    -8.6%

@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Sep 29, 2023

bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 29, 2023
bors bot pushed a commit that referenced this pull request Sep 29, 2023
@ChrisHughes24
perf: improve some instances in GroupTheory/Congruence (#6874)
7017600
@bors
Copy link
Copy Markdown

bors bot commented Sep 29, 2023

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.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title perf: improve some instances in GroupTheory/Congruence [Merged by Bors] - perf: improve some instances in GroupTheory/Congruence Sep 29, 2023
@bors bors bot closed this Sep 29, 2023
@bors bors bot deleted the ConPerfCH branch September 29, 2023 10:58
@ChrisHughes24 ChrisHughes24 mentioned this pull request Sep 29, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mattrobball mattrobball mattrobball approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@ChrisHughes24 @leanprover-bot @mattrobball