PR summary 7330fdbaf7

Import changes for modified files

No significant changes to the import graph

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

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

!bench

Here are the benchmark results for commit db687bf.
There were significant changes against commit 86414a8:

  Benchmark                                          Metric         Change
  ========================================================================
- ~Mathlib.RingTheory.AdicCompletion.Algebra         instructions    15.4%
- ~Mathlib.RingTheory.AdicCompletion.Basic           instructions    29.5%
+ ~Mathlib.RingTheory.AdicCompletion.Functoriality   instructions   -61.6%

!bench

Here are the benchmark results for commit ddef0a4.
There were significant changes against commit 86414a8:

  Benchmark                                    Metric         Change
  ==================================================================
- ~Mathlib.RingTheory.AdicCompletion.Algebra   instructions    15.4%
- ~Mathlib.RingTheory.AdicCompletion.Basic     instructions    29.5%

!bench

Here are the benchmark results for commit 20fe104.
There were significant changes against commit 86414a8:

  Benchmark                                          Metric         Change
  ========================================================================
- ~Mathlib.RingTheory.AdicCompletion.Algebra         instructions    28.6%
- ~Mathlib.RingTheory.AdicCompletion.Basic           instructions    47.8%
+ ~Mathlib.RingTheory.AdicCompletion.Functoriality   instructions   -60.3%

!bench

Here are the benchmark results for commit 6b20ecb.
There were significant changes against commit 86414a8:

  Benchmark                                          Metric         Change
  ========================================================================
- ~Mathlib.RingTheory.AdicCompletion.Algebra         instructions    27.9%
- ~Mathlib.RingTheory.AdicCompletion.Basic           instructions    34.4%
+ ~Mathlib.RingTheory.AdicCompletion.Functoriality   instructions   -61.7%

!bench

Here are the benchmark results for commit 571a2f2.
There were significant changes against commit 86414a8:

  Benchmark                                          Metric         Change
  ========================================================================
- ~Mathlib.RingTheory.AdicCompletion.Algebra         instructions    30.9%
- ~Mathlib.RingTheory.AdicCompletion.Basic           instructions    36.4%
+ ~Mathlib.RingTheory.AdicCompletion.Functoriality   instructions   -61.7%

It is out-dated but AdicCompletion.module didn't change its name right?

It is out-dated but AdicCompletion.module didn't change its name right?

Ah yes, no it did not change its name, but then adding the dsimp does not seem to make a significant difference to count_heartbeats in.

Oh well, it was minor I think anyway

So should I go for a final benchmark?

There is a good chance it won't make it in without using the Function.Injective constructors. We should test that fully first

I had tried out the version with Function.Injective constructors above, but it was significantly slower. See this comparison: http://speed.lean-fro.org/mathlib4/compare/04e26275-26be-4d08-8dd1-ffeb4e23bd0e/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash2=55cf90705c3509ab5da127b7ecd4db0e147af667

The first run is with Function.Injective constructors and the second one without.

Anything else I should test?

!bench

Here are the benchmark results for commit 400c96f.
There were significant changes against commit 86414a8:

  Benchmark                                          Metric         Change
  ========================================================================
+ ~Mathlib.RingTheory.AdicCompletion.Algebra         instructions   -15.3%
+ ~Mathlib.RingTheory.AdicCompletion.Functoriality   instructions   -64.1%

What's the effect on AsTensorProduct?

Benchmark is upcoming. My local one looks very good, i.e. comparable to the performance with explicit instances.

Benchmark is there. This is the comparsion:

http://speed.lean-fro.org/mathlib4/compare/e7b27246-a3e6-496a-b552-ff4b45c7236e/to/74e2d180-1ac7-47c1-9b6e-c7589ce1cd90?hash1=abf5c5635c9bde7cefa76b2c18405067b604e089

First commit: manual instances
Second commit: Function.Injective constructors with fast_instance%.

I think this looks promising, so I'll revert the commits adding the fast_instance% stuff and we add them back in later when the #11521 lands. What do you think @mattrobball ?

Also please make a separate dependent PR with the fast_instance insertions also so we can quickly put them back when that PR lands

Also please make a separate dependent PR with the fast_instance insertions also so we can quickly put them back when that PR lands

Since #11521 currently has merge conflicts, what should I do to create the dependent PR? Maybe from #11521 the actual fast_instance% code should be split of, otherwise it will collect merge conflicts all the time.

I forgot it wasn't just the single file. I'll split it later today.

Anything else I should do for this PR to be merged?

I don't think so. Thanks for your patience.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

Thanks a lot for the guidance and for helping analyzing this!