[Merged by Bors] - feat: use suppress_compilation in tensor products

[sgouezel]

More principled version of #7281.

---

Not completely satisfactory still, as suppress_compilation doesn't work with notation3, but the workaround using unsuppress_compilation in looks sufficient for now.

[sgouezel]

!bench

[leanprover-bot]

Here are the benchmark results for commit e525671.
There were significant changes against commit b2540cf:

  Benchmark                                                       Metric                 Change
  =============================================================================================
+ build                                                           .olean serialization    -8.0%
+ build                                                           compilation            -28.5%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic              instructions           -12.2%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed             instructions           -13.6%
+ ~Mathlib.Algebra.Category.Ring.Constructions                    instructions            -9.8%
+ ~Mathlib.Algebra.Lie.BaseChange                                 instructions           -87.7%
+ ~Mathlib.Algebra.Lie.TensorProduct                              instructions           -25.1%
+ ~Mathlib.Algebra.Lie.Weights                                    instructions           -81.3%
+ ~Mathlib.AlgebraicGeometry.Limits                               instructions            -5.8%
+ ~Mathlib.LinearAlgebra.BilinearForm.TensorProduct               instructions           -86.4%
+ ~Mathlib.LinearAlgebra.Contraction                              instructions            -7.4%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct                  instructions           -77.8%
+ ~Mathlib.LinearAlgebra.Multilinear.TensorProduct                instructions           -11.3%
+ ~Mathlib.LinearAlgebra.PiTensorProduct                          instructions           -11.1%
+ ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries   instructions           -21.7%
+ ~Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower              instructions           -35.0%
+ ~Mathlib.LinearAlgebra.TensorPower                              instructions           -11.2%
+ ~Mathlib.LinearAlgebra.TensorProduct                            instructions           -36.6%
+ ~Mathlib.LinearAlgebra.TensorProduct.Opposite                   instructions           -16.8%
+ ~Mathlib.LinearAlgebra.TensorProduct.Prod                       instructions           -33.6%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower                      instructions           -54.7%
+ ~Mathlib.LinearAlgebra.TensorProductBasis                       instructions           -21.8%
+ ~Mathlib.RepresentationTheory.FdRep                             instructions            -7.8%
+ ~Mathlib.RepresentationTheory.Invariants                        instructions           -85.6%
+ ~Mathlib.RepresentationTheory.Rep                               instructions           -44.6%
+ ~Mathlib.RingTheory.Kaehler                                     instructions           -18.8%
+ ~Mathlib.RingTheory.PolynomialAlgebra                           instructions           -10.2%
+ ~Mathlib.RingTheory.TensorProduct                               instructions           -12.3%
- ~Mathlib.Tactic.SuppressCompilation                             instructions            68.3%

[ocfnash]

Thank you very much for this

bors merge

[ocfnash]

Apparently the bors job containing this PR crashed:

Let's try again

bors merge

[ocfnash]

This is genuinely failing to build for bors with errors like:

Error: ./././Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean:130:4: error: compiler IR check failed at 'lTensor.toFun._rarg', error: unknown declaration 'LinearMap.lTensor'
Error: ./././Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean:137:4: error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'TensorProduct.lift', and it does not have executable code
Error: ./././Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean:198:4: error: compiler IR check failed at 'lTensor.linearEquiv_of_rightInverse._rarg', error: unknown declaration 'lTensor.toFun'
Error: ./././Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean:234:4: error: compiler IR check failed at 'rTensor.toFun._rarg', error: unknown declaration 'LinearMap.rTensor'
Error: ./././Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean:241:4: error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'TensorProduct.lift', and it does not have executable code
Error: ./././Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean:302:4: error: compiler IR check failed at 'rTensor.linearEquiv_of_rightInverse._rarg', error: unknown declaration 'rTensor.toFun'

I think you may need to merge master.

bors r-

[bors]

Canceled.

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style