PR summary 97680769fd

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

./scripts/technical-debt-metrics.sh pr_summary

@fpvandoorn, what's your preferred way for me to fix the simps error in Logic.Equiv.Set?

By making sure that Logic.Equiv.Defs imports a file containing initialize_simps_projections Subtype (val → coe) (currently Data.Subtype).
At least, I think that is the issue.
If that is the issue, please open an issue that simps should raise a warning when two conflicting configurations are found in different imports.

#23041 might also help

Or, going even further, we can disallow @[simps] at all, unless initialize_simps_projections has been called explicitly.

When I wrote @[simps], I was under the impression that being more permissive is better: if the user wants to do X, it should try to do X as best as it can. However, I realize that in the current Mathlib with its many refactors, this is not desired: refactors often unintentionally change things, and simps should just complain whenever something changes.

Please open issues (or make fixes to simps) with how you want it to behave.
In particular, the suggestion at the start of this message is easy: currently getRawProjections either retrieves projection information, or generates it. Splitting that up into two separate functions would do the trick.

By making sure that Logic.Equiv.Defs imports a file containing initialize_simps_projections Subtype (val → coe) (currently Data.Subtype).

Indeed that's the case.

If that is the issue, please open an issue that simps should raise a warning when two conflicting configurations are found in different imports.

I see that you have opened #23041 for that, so I will refrain from doing so.

It's not quite the same, but I added it to that issue.

Do you think this would be good?

Or, going even further, we can disallow @[simps] at all, unless initialize_simps_projections has been called explicitly.

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style