Skip to content

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

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

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

Conversation

@Vierkantor
Copy link
Copy Markdown
Contributor

@Vierkantor Vierkantor commented Oct 18, 2024 •
edited
Loading

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.

Open in Gitpod

@Vierkantor Vierkantor added WIP Work in progress awaiting-bench This PR needs to be benchmarked before merging labels Oct 18, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 18, 2024 •
edited
Loading

PR summary 7d3c2804e4

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

- AffineMap.hasCoeToFun
- instCoeFun
- instance : CoeFun (Chain α) fun _ => ℕ → α := ⟨DFunLike.coe⟩
- instance : CoeFun (ContinuousMultilinearMap R M₁ M₂) fun _ => (∀ i, M₁ i) → M₂
- instance : CoeFun (M ↪ₑ[L] N) fun _ => M → N
- 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

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.

@Vierkantor
Copy link
Copy Markdown
Contributor Author

Vierkantor commented Oct 18, 2024

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Oct 18, 2024

Here are the benchmark results for commit e4181dc.
There were significant changes against commit 672f75b:

  Benchmark                                     Metric         Change
  ===================================================================
- ~Mathlib.Analysis.InnerProductSpace.Adjoint   instructions     8.5%

@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 Vierkantor force-pushed the remove-coefun-test-1 branch from e4181dc to 7d3c280 Compare October 18, 2024 10:36
@Vierkantor
Copy link
Copy Markdown
Contributor Author

Vierkantor commented Oct 18, 2024

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Oct 18, 2024

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

@Vierkantor
Copy link
Copy Markdown
Contributor Author

Vierkantor commented Oct 18, 2024

Progress! So I suppose I'll make this PR ready for review and open a new one with half of the remaining changes.

@Vierkantor Vierkantor added tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip and removed 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
@Vierkantor Vierkantor removed the WIP Work in progress label Oct 18, 2024
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Oct 18, 2024

Thanks - landing this piece-wise is still a great improvement!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 18, 2024

🚀 Pull request has been placed on the maintainer queue by grunweg.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 18, 2024
@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Oct 18, 2024

bors merge

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

mathlib-bors bot commented Oct 18, 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 18, 2024
@mathlib-bors mathlib-bors bot closed this Oct 18, 2024
@mathlib-bors mathlib-bors bot deleted the remove-coefun-test-1 branch October 18, 2024 16:57
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

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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.

4 participants

@Vierkantor @leanprover-bot @grunweg @mattrobball