Skip to content

[Merged by Bors] - perf: improve some instances in Finsupp#7430

Closed
ChrisHughes24 wants to merge 2 commits intomasterfrom
FinsuppPerfCH2
Closed

[Merged by Bors] - perf: improve some instances in Finsupp#7430
ChrisHughes24 wants to merge 2 commits intomasterfrom
FinsuppPerfCH2

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member

@ChrisHughes24 ChrisHughes24 commented Sep 29, 2023 •
edited
Loading

Open in Gitpod

@ChrisHughes24 ChrisHughes24 added WIP Work in progress awaiting-author A reviewer has asked the author a question or requested changes. labels Sep 29, 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 2bf5292.
There were significant changes against commit 7017600:

  Benchmark                                                  Metric         Change
  ================================================================================
+ ~Mathlib.Algebra.Category.ModuleCat.Adjunctions            instructions    -8.6%
+ ~Mathlib.Algebra.Category.ModuleCat.Projective             instructions    -7.7%
- ~Mathlib.LinearAlgebra.FinsuppVectorSpace                  instructions     5.6%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Basic        instructions   -28.1%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution   instructions    -5.3%
+ ~Mathlib.RingTheory.Artinian                               instructions    -5.1%
+ ~Mathlib.RingTheory.Kaehler                                instructions    -6.2%
- ~Mathlib.RingTheory.MvPolynomial.Homogeneous               instructions     5.5%
+ ~Mathlib.RingTheory.WittVector.Teichmuller                 instructions   -11.5%

@ChrisHughes24 ChrisHughes24 mentioned this pull request Sep 29, 2023
Closed
@ChrisHughes24 ChrisHughes24 added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Sep 30, 2023
mattrobball
mattrobball reviewed Oct 3, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@mattrobball mattrobball left a comment

Choose a reason for hiding this comment

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

I think the actual changes to the code are straightforward and it would benefit everyone to have them in sooner rather than later.

What would think about moving all the applications of comments from #7432 to #7432? Here and in the other PRs. That PR might take more discussion to sharpen.

@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Oct 3, 2023

I don't understand what you want me to do about the comments

@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Oct 4, 2023

Sorry for being obtuse. I'm just saying move the comments involving the library note to the library note PR itself. For this and the others.

I think we are still working out best practices for that note and don't think this should be held up by that process.

@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Oct 4, 2023

Or to be safe add TODOs here.

@ChrisHughes24 ChrisHughes24 removed WIP Work in progress blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Oct 4, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 4, 2023
@ChrisHughes24 ChrisHughes24 added awaiting-review and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Oct 4, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Oct 4, 2023

I added some TODOs here.

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 4, 2023
@ChrisHughes24 ChrisHughes24 removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 4, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 4, 2023
@ChrisHughes24 ChrisHughes24 removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 4, 2023
@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Oct 4, 2023

bors d+

Thanks!

@bors
Copy link
Copy Markdown

bors bot commented Oct 4, 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 delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Oct 4, 2023
@mattrobball mattrobball mentioned this pull request Oct 4, 2023
Closed
@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Oct 5, 2023

bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 5, 2023
bors bot pushed a commit that referenced this pull request Oct 5, 2023
@ChrisHughes24
perf: improve some instances in Finsupp (#7430)
7f01c99
@bors
Copy link
Copy Markdown

bors bot commented Oct 5, 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 Finsupp [Merged by Bors] - perf: improve some instances in Finsupp Oct 5, 2023
@bors bors bot closed this Oct 5, 2023
@bors bors bot deleted the FinsuppPerfCH2 branch October 5, 2023 11:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mattrobball mattrobball mattrobball left review comments

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