Skip to content
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.

Sign up for GitHub

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

Jump to bottom

chore: refactor LeftCancelMonoid and friends #6011

Closed
wants to merge 10 commits into from
Closed

chore: refactor LeftCancelMonoid and friends #6011

wants to merge 10 commits into from

Conversation

kbuzzard
Copy link
Member

Implementing this Zulip suggestion.

Open in Gitpod

@kbuzzard kbuzzard added the WIP Work in progress label Jul 19, 2023
@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ed98890.Found no runs to compare against.

@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ed98890.Found no runs to compare against.

@kbuzzard
Copy link
Member Author

kbuzzard commented Jul 20, 2023 •
edited
Loading

My understanding is that this change shaves another 5% of maxrss. Here is a speedcenter diff against a recent push to master (wait a few seconds for the results to appear). As you can see from the top there is a lot more green than red but I'm always a bit nervous about this because I can't immediately see whether it's the case that something which used to take 1 second is now 30% faster but something which used to take 1 minute is now 20% slower.

@kbuzzard kbuzzard added awaiting-review and removed WIP Work in progress labels Jul 20, 2023
@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ed98890.Found no runs to compare against.

@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ed98890.Found no runs to compare against.

@kbuzzard
Copy link
Member Author

If I just keep typing !bench will it eventually give me some red and green print-out?

!bench

@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ed98890.
There were significant changes against commit eb706c1:

  Benchmark                                                                Metric         Change
  ==============================================================================================
- build                                                                    maxrss          10.9%
+ ~Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating   instructions    -7.5%
+ ~Mathlib.Algebra.Order.Monoid.NatCast                                    instructions    -7.7%
- ~Mathlib.Combinatorics.HalesJewett                                       instructions    32.8%
- ~Mathlib.LinearAlgebra.FreeModule.PID                                    instructions    12.8%
- ~Mathlib.RingTheory.ClassGroup                                           instructions     9.0%

@Vierkantor Vierkantor mentioned this pull request Jul 26, 2023
Closed
@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ab17523.Found no runs to compare against.

@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ab17523.Found no runs to compare against.

@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ab17523.Found no runs to compare against.

@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ab17523.Found no runs to compare against.

@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ab17523.Found no runs to compare against.

@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ab17523.Found no runs to compare against.

@kbuzzard
Copy link
Member Author

This is an attempt to merge a commit on master which has already been profiled.

@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit bef7e1a.
There were significant changes against commit 4707b47:

  Benchmark                                                                Metric         Change
  ==============================================================================================
- build                                                                    maxrss           5.6%
+ ~Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating   instructions    -7.5%
+ ~Mathlib.Algebra.Order.Monoid.NatCast                                    instructions    -7.6%
- ~Mathlib.Combinatorics.HalesJewett                                       instructions    32.7%
- ~Mathlib.RepresentationTheory.GroupCohomology.Resolution                 instructions     5.1%
- ~Mathlib.RingTheory.ClassGroup                                           instructions     5.7%
- ~Std.Lean.TagAttribute                                                   instructions     6.7%

bors bot pushed a commit that referenced this pull request Jul 31, 2023
@Vierkantor
chore: split ClassGroup.mk0_surjective (#6146)
cba384a 
Not only was this a huge declaration, it also remained unfolded throughout checking the proof, so things like defeq checking were extremely slow (total declaration elaboration time ~1 minute on my machine). Splitting it into a `def` + proofs makes everything much faster.

Total build time for this file on my machine went from ~140 seconds to ~80 seconds.

I came across this issue while trying to figure out why #6011 appeared to slow down building of `ClassGroup.lean`.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@kbuzzard
Copy link
Member Author

I'm surprised that this PR should consistently have such a bad effect on Hales-Jewett. This deserves some further investigation.

@kbuzzard kbuzzard added WIP Work in progress and removed awaiting-review labels Jul 31, 2023
semorrison pushed a commit that referenced this pull request Aug 2, 2023
@Vierkantor @semorrison
chore: split ClassGroup.mk0_surjective (#6146)
e1019d8 
Not only was this a huge declaration, it also remained unfolded throughout checking the proof, so things like defeq checking were extremely slow (total declaration elaboration time ~1 minute on my machine). Splitting it into a `def` + proofs makes everything much faster.

Total build time for this file on my machine went from ~140 seconds to ~80 seconds.

I came across this issue while trying to figure out why #6011 appeared to slow down building of `ClassGroup.lean`.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Aug 7, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Aug 9, 2023
semorrison pushed a commit that referenced this pull request Aug 14, 2023
@Vierkantor @semorrison
chore: split ClassGroup.mk0_surjective (#6146)
cc0ce92 
Not only was this a huge declaration, it also remained unfolded throughout checking the proof, so things like defeq checking were extremely slow (total declaration elaboration time ~1 minute on my machine). Splitting it into a `def` + proofs makes everything much faster.

Total build time for this file on my machine went from ~140 seconds to ~80 seconds.

I came across this issue while trying to figure out why #6011 appeared to slow down building of `ClassGroup.lean`.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:24
@semorrison semorrison changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:15
@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ac47956.
The entire run failed.
Found no significant differences.

@kbuzzard
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 3580dd4.
There were no significant changes against commit 30a9315.

@kbuzzard
Copy link
Member Author

Things have moved on so much since I opened this PR that these changes no longer have any effect.

@kbuzzard kbuzzard closed this Feb 24, 2024
@kbuzzard kbuzzard deleted the kbuzzard-LeftCancelMonoid-refactor branch February 24, 2024 19:55
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
WIP Work in progress
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@kbuzzard @leanprover-bot @leanprover-community-mathlib4-bot