[Merged by Bors] - chore: remove CoeFun instances where FunLike is available#17870
[Merged by Bors] - chore: remove CoeFun instances where FunLike is available#17870Vierkantor wants to merge 3 commits intomasterfrom
Conversation
|
!bench |
PR summary abd00d72e4Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
We prefer `FunLike` over `CoeFun` if possible, so we don't care that we made that change during the port. See also #17870 for applying the change that was porting noted consistently across the entirety of Mathlib.
jcommelin
left a comment
There was a problem hiding this comment.
Thanks 🎉
If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.
bors d+
|
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
We prefer `FunLike` over `CoeFun` if possible, so we don't care that we made that change during the port. See also #17870 for applying the change that was porting noted consistently across the entirety of Mathlib.
|
Here are the benchmark results for commit 36f0ed3. |
These were already unused on the master branch but became exposed to the linter after #17870 changed some `CoeFun` instances.
|
!bench |
These were already unused on the master branch but became exposed to the linter after #17870 changed some `CoeFun` instances.
|
Here are the benchmark results for commit f28c9f5. Benchmark Metric Change
===================================================================
- ~Mathlib.Analysis.InnerProductSpace.Adjoint instructions 8.4% |
|
Not sure why that one file is so much slower: I didn't touch anything involving |
|
!bench |
|
Here are the benchmark results for commit ae8a2bd. Benchmark Metric Change
===================================================================
- ~Mathlib.Analysis.InnerProductSpace.Adjoint instructions 8.6% |
|
Hmm. Binary search to see which subset of lemmas breaks the bench? |
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. This is the second half of #17870, and doesn't affect the benchmarks.
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. Compared to previous tests, this only preserves the `Finsupp` and `DFinsupp` instances; my guess is that they are the important shortcut instances preventing slowdowns.
ae8a2bd to
abd00d7
Compare
|
See #17921 for the benchmarks proving that |
|
!bench |
|
Here are the benchmark results for commit abd00d7. |
|
Thanks 🎉 bors merge |
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. There is also a shortcut instance that we need for speed reasons: `SemilinearIsometry.instCoeFun`. I don't know why this is so performance-sensitive but the benchmarks tell us that it is. See also #17871 for removing porting notes and comments where this change happened earlier on.
|
Pull request successfully merged into master. Build succeeded: |
During the port we found that
FunLikeis robust enough not to need an extraCoeFunshortcut. Let's see if that rule can be consistently applied to the whole of the library.There is still duplication between
FunLikeandCoeFunforGrp,Mon,CommGrpandCommMon, which will need a more thorough fix. See also #17866.There is also a shortcut instance that we need for speed reasons:
SemilinearIsometry.instCoeFun. I don't know why this is so performance-sensitive but the benchmarks tell us that it is.See also #17871 for removing porting notes and comments where this change happened earlier on.