Skip to content

[Merged by Bors] - perf: to_additive (attr := reducible) -> abbrev#15476

Closed
astrainfinita wants to merge 14 commits intomasterfrom
FR_perf_toadditive_abbrev
Closed

[Merged by Bors] - perf: to_additive (attr := reducible) -> abbrev#15476
astrainfinita wants to merge 14 commits intomasterfrom
FR_perf_toadditive_abbrev

Conversation

@astrainfinita
Copy link
Copy Markdown
Collaborator

@astrainfinita astrainfinita commented Aug 3, 2024 •
edited by github-actions bot
Loading

@astrainfinita astrainfinita added the t-algebra Algebra (groups, rings, fields, etc) label Aug 3, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 3, 2024 •
edited
Loading

PR summary dcba14d553

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

- Away
- Away.monoidOf
- AwayMap
- Function.Injective.linearOrderedCancelCommMonoid
- Function.Injective.linearOrderedCommGroup
- Function.Injective.linearOrderedCommMonoid
- Function.Injective.mulAction
- Function.Injective.orderedCancelCommMonoid
- Function.Injective.orderedCommGroup
- Function.Injective.orderedCommMonoid
- Function.Surjective.mulAction
- Function.Surjective.mulActionLeft
- Group.ofLeftAxioms
- Group.ofRightAxioms
- GroupNorm.toNormedCommGroup
- GroupNorm.toNormedGroup
- GroupSeminorm.toSeminormedCommGroup
- GroupSeminorm.toSeminormedGroup
- Inv
- NormedCommGroup.induced
- NormedCommGroup.ofMulDist
- NormedCommGroup.ofMulDist'
- NormedCommGroup.ofSeparation
- NormedGroup.induced
- NormedGroup.ofMulDist
- NormedGroup.ofMulDist'
- NormedGroup.ofSeparation
- SeminormedCommGroup.induced
- SeminormedCommGroup.ofMulDist
- SeminormedCommGroup.ofMulDist'
- SeminormedGroup.induced
- SeminormedGroup.ofMulDist
- SeminormedGroup.ofMulDist'
- cancelCommMonoid
- cancelMonoid
- commMonoidOfExponentTwo
- comp
- compHom
- div
- divInvOneMonoid
- divisionCommMonoid
- divisionMonoid
- haar
- invOneClass
- leftCancelMonoid
- leftCancelSemigroup
- mul
- mulEquiv
- one
- orbitRel.Quotient
- rightCancelMonoid
- rightCancelSemigroup
-- commMagma
-- divInvMonoid
-- involutiveInv
--- commSemigroup
--- group
--- monoid
--- mulOneClass
--- semigroup
---- commGroup
---- commMonoid

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 3, 2024
@astrainfinita astrainfinita mentioned this pull request Aug 3, 2024
Closed
@astrainfinita astrainfinita mentioned this pull request Aug 3, 2024
Open
2 tasks
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Aug 4, 2024

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Aug 4, 2024

Here are the benchmark results for commit 6deba5d.
There were significant changes against commit d631146:

  Benchmark                                               Metric         Change
  =============================================================================
+ ~Mathlib.Algebra.Category.Grp.Limits                    instructions   -24.0%
+ ~Mathlib.Algebra.Category.Ring.Limits                   instructions   -29.7%
+ ~Mathlib.Algebra.Order.Field.Subfield                   instructions   -60.3%
+ ~Mathlib.Algebra.Ring.Subring.Order                     instructions   -47.0%
+ ~Mathlib.Algebra.Ring.Subsemiring.Order                 instructions   -55.2%
- ~Mathlib.FieldTheory.Adjoin                             instructions     3.8%
+ ~Mathlib.GroupTheory.CosetCover                         instructions   -18.0%
- ~Mathlib.LinearAlgebra.TensorProduct.Graded.Internal    instructions     7.6%
+ ~Mathlib.Logic.Equiv.TransferInstance                   instructions   -26.9%
+ ~Mathlib.RingTheory.AdicCompletion.AsTensorProduct      instructions   -44.8%
+ ~Mathlib.Topology.ContinuousFunction.Ideals             instructions   -23.0%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass   instructions   -14.0%

@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Aug 5, 2024
@ghost
Copy link
Copy Markdown

ghost commented Aug 8, 2024

This PR/issue depends on:

@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Aug 9, 2024

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Aug 9, 2024

Here are the benchmark results for commit dcba14d.
There were significant changes against commit 1339db1:

  Benchmark                                               Metric         Change
  =============================================================================
+ ~Mathlib.Algebra.Category.Grp.Limits                    instructions   -23.4%
+ ~Mathlib.Algebra.Category.Ring.Limits                   instructions   -26.8%
+ ~Mathlib.Algebra.Field.Subfield                         instructions   -17.1%
+ ~Mathlib.Algebra.Order.Field.Subfield                   instructions   -61.9%
+ ~Mathlib.Algebra.Ring.Subring.Order                     instructions   -48.8%
+ ~Mathlib.Algebra.Ring.Subsemiring.Order                 instructions   -56.5%
- ~Mathlib.FieldTheory.Adjoin                             instructions     4.7%
- ~Mathlib.LinearAlgebra.TensorProduct.Graded.Internal    instructions     9.0%
+ ~Mathlib.Logic.Equiv.TransferInstance                   instructions   -29.5%
+ ~Mathlib.Logic.Small.Ring                               instructions   -59.8%
+ ~Mathlib.RingTheory.AdicCompletion.AsTensorProduct      instructions   -45.2%
+ ~Mathlib.Topology.ContinuousFunction.Ideals             instructions   -22.9%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass   instructions   -14.1%

@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 Aug 9, 2024
@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Aug 9, 2024

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 9, 2024

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 9, 2024
@urkud
Copy link
Copy Markdown
Member

urkud commented Aug 9, 2024

Thanks! 🎉
bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 9, 2024
@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Aug 9, 2024

Yes, thanks @FR-vdash-bot! This was very annoying.

mathlib-bors bot pushed a commit that referenced this pull request Aug 9, 2024
@astrainfinita
perf: to_additive (attr := reducible) -> abbrev (#15476)
4d65f9e
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 9, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title perf: to_additive (attr := reducible) -> abbrev [Merged by Bors] - perf: to_additive (attr := reducible) -> abbrev Aug 9, 2024
@mathlib-bors mathlib-bors bot closed this Aug 9, 2024
@mathlib-bors mathlib-bors bot deleted the FR_perf_toadditive_abbrev branch August 9, 2024 15:52
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@astrainfinita @bjoernkjoshanssen
perf: to_additive (attr := reducible) -> abbrev (#15476)
5bd7901
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@astrainfinita @bjoernkjoshanssen
perf: to_additive (attr := reducible) -> abbrev (#15476)
76d0004
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@astrainfinita @bjoernkjoshanssen
perf: to_additive (attr := reducible) -> abbrev (#15476)
93d5f5e
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@astrainfinita @leanprover-bot @j-loreaux @urkud @mattrobball