PR summary 08cc6a21bf

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>

!bench

Here are the benchmark results for commit 34538ab.
There were significant changes against commit 3e38319:

  Benchmark                                              Metric         Change
  ============================================================================
- ~Mathlib.Analysis.FunctionalSpaces.SobolevInequality   instructions    16.8%

I don't understand at all why this would make anything slower. I will note that the places using fun_prop the most (continuous functional calculus files) did get marginally faster.

I also find it baffling. My wild guess is that type classes are cached anyway so resynthesizing them is not such a big deal. However, you might end up with instances that are defeq but not trivially so type checking takes longer.

But I do not know what the "instructions" metric is.

Instructions are the best proxy we have for "amount of computation done independent of hardware"

Do we want to merge this? Is the 16% increase on that one file a blocker? Should that be investigated?

I'm not entirely sure about this. It does speed things up a bit in the continuous functional calculus portion of the library, where we use fun_prop heavily, but I don't have a good understanding of the slowdown in the Sobolev file.

maintainer merge

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

Overall instructions are basically flat. So from that perspective this is fine. I think the slowdown you see is exactly as @lecopivo surmised (and as core would probably chastise us for). But if this works where it needs to right now, I think it is ok to run with and evaluate as we go.

bors merge

Build failed (retrying...):

• Build

Build failed (retrying...):

• Build

Build failed:

• Lint style

bors r+

Build failed (retrying...):

• Build

bors r-
Can you merge master, fix the lint, and then send it back to bors?
bors d+

✌️ lecopivo can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Canceled.

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style