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.

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

feat: golf using gcongr throughout the library #7901

Closed
wants to merge 8 commits into from

Conversation

hrmacbeth
Copy link
Member

Following on from #4702 and #4784.


Open in Gitpod

@hrmacbeth
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 3aed923.
There were significant changes against commit bf077b1:

  Benchmark                            Metric         Change
  ==========================================================
- lint                                 wall-clock       5.3%
- ~Mathlib.Analysis.Analytic.Inverse   instructions     9.6%

@hrmacbeth
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 39161d1.
There were significant changes against commit bf077b1:

  Benchmark                            Metric         Change
  ==========================================================
- ~Mathlib.Analysis.Analytic.Inverse   instructions    10.1%

@hrmacbeth
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 2c84531.
There were no significant changes against commit bf077b1.

@hrmacbeth
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

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

@hrmacbeth
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

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

@hrmacbeth
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 818206f.
There were significant changes against commit bf077b1:

  Benchmark                            Metric         Change
  ==========================================================
- ~Mathlib.Analysis.Analytic.Inverse   instructions     8.4%

@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 Nov 11, 2023
@hrmacbeth
Copy link
Member Author

Closing in favour of #8752.

@hrmacbeth hrmacbeth closed this Nov 30, 2023
mathlib-bors bot pushed a commit that referenced this pull request Nov 30, 2023
Following on from previous `gcongr` golfing PRs #4702 and #4784.

This is a replacement for #7901: this round of golfs, first introduced there, there exposed some performance issues in `gcongr`, hopefully fixed by #8731, and I am opening a new PR so that the performance can be checked against current master rather than master at the time of #7901.
awueth pushed a commit that referenced this pull request Dec 19, 2023
Following on from previous `gcongr` golfing PRs #4702 and #4784.

This is a replacement for #7901: this round of golfs, first introduced there, there exposed some performance issues in `gcongr`, hopefully fixed by #8731, and I am opening a new PR so that the performance can be checked against current master rather than master at the time of #7901.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge-conflict The PR has a merge conflict with master, and needs manual merging.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants