Skip to content

[Merged by Bors] - chore: remove CoeFun instances where FunLike is available#17911

Closed
Vierkantor wants to merge 3 commits intomasterfrom
remove-coefun-test-2
Closed

[Merged by Bors] - chore: remove CoeFun instances where FunLike is available#17911
Vierkantor wants to merge 3 commits intomasterfrom
remove-coefun-test-2

Conversation

@Vierkantor
Copy link
Copy Markdown
Contributor

@Vierkantor Vierkantor commented Oct 18, 2024

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.

I am currently bisecting to figure out exactly why the benchmarks are indicating a slowdown with no obvious cause.

Open in Gitpod

@Vierkantor
Basic fixups
9b9d2b7
@Vierkantor
chore: remove CoeFun instances where FunLike is available
7d3c280 
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 first half of the changes, to see if those work without slowdowns.
@Vierkantor
This is the first half of the first half of the changes.
7a06803
@Vierkantor Vierkantor added WIP Work in progress tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip awaiting-bench This PR needs to be benchmarked before merging labels Oct 18, 2024
@Vierkantor
Copy link
Copy Markdown
Contributor Author

Vierkantor commented Oct 18, 2024

!bench

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 18, 2024

PR summary 7a06803237

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

- AffineMap.hasCoeToFun
- instance : CoeFun (AbsoluteValue R S) fun _ => R → S
- instance : CoeFun (AlgebraNorm R S) fun _ => S → ℝ
- instance : CoeFun (CentroidHom α) fun _ ↦ α → α
- instance : CoeFun (Chain α) fun _ => ℕ → α := ⟨DFunLike.coe⟩
- instance : CoeFun (ContinuousMultilinearMap R M₁ M₂) fun _ => (∀ i, M₁ i) → M₂
- instance : CoeFun (GroupNorm E) fun _ => E → ℝ
- instance : CoeFun (GroupSeminorm E) fun _ => E → ℝ
- instance : CoeFun (M ↪ₑ[L] N) fun _ => M → N
- instance : CoeFun (MulAlgebraNorm R S) fun _ => S → ℝ
- instance : CoeFun (NonarchAddGroupNorm E) fun _ => E → ℝ
- instance : CoeFun (NonarchAddGroupSeminorm E) fun _ => E → ℝ
- instance : CoeFun (Path x y) fun _ => I → X
- instance : CoeFun (P₁ ≃ᵃ[k] P₂) fun _ => P₁ → P₂
- instance : CoeFun (QuadraticMap R M N) fun _ => M → N
- instance : CoeFun (WeakDual 𝕜 E) fun _ => E → 𝕜
- instance : CoeFun (X ≃ᵈ Y) fun _ ↦ (X → Y)
- instance : CoeFun (X ≃ₜ Y) fun _ ↦ X → Y := ⟨DFunLike.coe⟩
- instance : CoeFun (α →ᵈ β) fun _ => α → β
-- hasCoeToFun
-- instCoeFun

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.

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 18, 2024
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Oct 18, 2024

Here are the benchmark results for commit 7a06803.
There were no significant changes against commit 672f75b.

@Vierkantor Vierkantor removed WIP Work in progress awaiting-bench This PR needs to be benchmarked before merging labels Oct 18, 2024
@Vierkantor Vierkantor mentioned this pull request Oct 18, 2024
Closed
1 task
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 18, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Oct 18, 2024

This PR/issue depends on:

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Oct 18, 2024

During the port we found that FunLike is robust enough not to need an extra CoeFun shortcut.

Indeed, but we also found that the shortcut could often improve performance, as you are now running into!

@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Oct 19, 2024

@eric-wieser Could you please explain what you mean? Because the bench bot says there is no significant performance regression.

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Oct 19, 2024

I think "often" is compatible with what Anne is finding: removing the shortcut entirely causes a slowdown.

Let's just merge the parts that don't cause a slow down, and soon Anne will hopefully have localised the places where removing it really is damaging, and then we can study that.

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Oct 19, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 19, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 19, 2024
@Vierkantor
chore: remove CoeFun instances where FunLike is available (#17911)
418a5eb 
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.

I am currently bisecting to figure out exactly why the benchmarks are indicating a slowdown with no obvious cause.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: remove CoeFun instances where FunLike is available [Merged by Bors] - chore: remove CoeFun instances where FunLike is available Oct 19, 2024
@mathlib-bors mathlib-bors bot closed this Oct 19, 2024
@mathlib-bors mathlib-bors bot deleted the remove-coefun-test-2 branch October 19, 2024 08:00
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

ready-to-merge This PR has been sent to bors. tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@Vierkantor @leanprover-bot @mathlib4-dependent-issues-bot @eric-wieser @jcommelin @kim-em