PR summary a077c04bd1

Import changes for modified files

No significant changes to the import graph

Declarations diff

No declarations were harmed in the making of this PR! 🐙

## 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.

!bench

This generalization can go quite a lot further... Let me try pushing some more.

I span off #17526 rather than getting carried away beyond MeasureTheory.

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

!bench

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

It looks good and I think we could merge. Do you still want to try and get a working benchmark?

!bench

The speed-center is back up, so let's hopefully just wait a short moment until the benchmarking results are in. If this doesn't work, I'm happy to merge it as-is.

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

Once more with feeling: need to benchmark again after merging master.

!bench

Here are the benchmark results for commit a077c04.
There were no significant changes against commit 1e919af.

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style