chore: changes for leanprover/lean4#2478

[mattrobball]

These are adaptions to adjust for the changes to structure instance elaboration in leanprover/lean4#2478.

---

[semorrison]

The benchmarking seems to say:

• this results in a speed up for many files in Mathlib
• but a significant slow-down in the worst files
• overall a 4.5% decrease in instructions
• overall a 2.5% wall-clock slow-down

I'm not entirely sure what to do with that.

The optimist in me says: the worst files (particularly AlgebraicGeometry.*) have something fundamentally wrong in them (but what?), and when we sort them out they will, like everything else, get a speed up too.

The pessimist says: this is an overall slow-down.

[mattrobball]

Since there are existing fixes for RingTheory.Kaehler and Analysis.NormedSpace.Operator, let's eliminate them from consideration.

The significant regressions (double digits) in large files are then all concentrated in AlgebraicGeometry.

Parts of AG are unusable at the moment.

Everyone is affected by it since one file and the path to it completely control the build time for all of Mathlib. This is why total build time is a poor measure of performance improvement. It only measures the effect on RingHomProperties.

The terms exposed are simply too large. I'd wager that it leads all folders in use of erw when appropriately measured, for example.

The change here creates more tightly packed terms which is great when your design is disciplined but terrible when it's not. In particular, when you rely on exposing giant terms in unification, you are going to need more cycles to succeed and pay the price.

There needs to be a refactor enforcing API boundaries in AG. Should we postpone the benefits for everyone else until this is done?

[mattrobball]

but a significant slow-down in the worst files

Excluding Kaehler and OperatorNorm, there is a good net drop in instructions for the ten largest (by instructions) files.

It only gets better when you go to top 20 or 30.

Areas of concern like GroupCohomology (number 3 and 5) get noticeably better.

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 2c655ab.
There were significant changes against commit e3644b2:

  Benchmark                                                          Metric             Change
  ============================================================================================
+ build                                                              compilation         -5.2%
+ build                                                              elaboration         -6.0%
+ build                                                              tactic execution    -6.8%
+ build                                                              type checking      -12.2%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization                    instructions       -14.5%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                  instructions        -6.6%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                 instructions       -22.4%
+ ~Mathlib.Algebra.DirectLimit                                       instructions       -36.0%
+ ~Mathlib.Algebra.DirectSum.Ring                                    instructions       -13.7%
+ ~Mathlib.Algebra.DualQuaternion                                    instructions       -21.9%
+ ~Mathlib.Algebra.Jordan.Basic                                      instructions        -4.0%
+ ~Mathlib.Algebra.Lie.DirectSum                                     instructions       -20.9%
+ ~Mathlib.Algebra.Module.GradedModule                               instructions       -33.3%
+ ~Mathlib.Algebra.Module.PID                                        instructions       -14.9%
+ ~Mathlib.Algebra.RingQuot                                          instructions       -15.4%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra                          instructions        -3.0%
- ~Mathlib.AlgebraicGeometry.AffineScheme                            instructions         7.9%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point                     instructions        -2.8%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass               instructions        -3.0%
- ~Mathlib.AlgebraicGeometry.Properties                              instructions        19.1%
+ ~Mathlib.Analysis.Calculus.ContDiff                                instructions        -9.0%
+ ~Mathlib.Analysis.Calculus.ContDiffDef                             instructions        -5.3%
+ ~Mathlib.Analysis.Convolution                                      instructions        -2.6%
+ ~Mathlib.Analysis.Fourier.AddCircle                                instructions        -9.1%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                        instructions        -3.6%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                           instructions        -8.0%
- ~Mathlib.Analysis.InnerProductSpace.TwoDim                         instructions        16.9%
+ ~Mathlib.Analysis.LocallyConvex.WithSeminorms                      instructions       -13.7%
+ ~Mathlib.Analysis.Normed.Field.Basic                               instructions       -14.7%
+ ~Mathlib.Analysis.NormedSpace.FiniteDimension                      instructions        -8.9%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential                    instructions       -38.9%
+ ~Mathlib.Analysis.NormedSpace.Multilinear                          instructions        -6.1%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                  instructions       -22.2%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                      instructions        -4.7%
+ ~Mathlib.Analysis.NormedSpace.lpSpace                              instructions       -11.7%
+ ~Mathlib.Analysis.Seminorm                                         instructions        -7.2%
+ ~Mathlib.CategoryTheory.Abelian.InjectiveResolution                instructions        -6.9%
+ ~Mathlib.CategoryTheory.Abelian.Projective                         instructions        -1.3%
+ ~Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory          instructions        -4.4%
+ ~Mathlib.Data.IsROrC.Basic                                         instructions        -3.6%
+ ~Mathlib.Data.Matrix.Rank                                          instructions       -13.6%
+ ~Mathlib.Data.MvPolynomial.Basic                                   instructions        -5.4%
- ~Mathlib.FieldTheory.AbelRuffini                                   instructions        12.5%
+ ~Mathlib.FieldTheory.Adjoin                                        instructions        -3.8%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                  instructions       -15.1%
+ ~Mathlib.FieldTheory.IsAlgClosed.Basic                             instructions        -6.4%
+ ~Mathlib.FieldTheory.RatFunc                                       instructions        -3.2%
+ ~Mathlib.FieldTheory.Subfield                                      instructions       -10.0%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                           instructions        -8.3%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation         instructions       -40.3%
+ ~Mathlib.Geometry.Manifold.DerivationBundle                        instructions       -29.7%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion                        instructions        -5.6%
+ ~Mathlib.LinearAlgebra.AdicCompletion                              instructions       -13.0%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                     instructions       -12.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                  instructions       -22.5%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                       instructions       -20.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation                 instructions       -43.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                 instructions       -36.4%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs                      instructions       -14.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                   instructions       -13.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold                        instructions       -25.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                     instructions       -19.1%
+ ~Mathlib.LinearAlgebra.Dual                                        instructions        -7.3%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic                       instructions       -33.5%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                     instructions       -24.7%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating               instructions       -25.0%
- ~Mathlib.LinearAlgebra.FinsuppVectorSpace                          instructions         6.4%
+ ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm                     instructions        -2.6%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum                             instructions       -24.7%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                instructions        -5.6%
+ ~Mathlib.LinearAlgebra.QuotientPi                                  instructions       -14.6%
+ ~Mathlib.MeasureTheory.Constructions.Pi                            instructions        -4.5%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2   instructions       -10.6%
+ ~Mathlib.MeasureTheory.Function.LpSeminorm                         instructions        -4.0%
+ ~Mathlib.MeasureTheory.Function.LpSpace                            instructions       -17.0%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                  instructions        -8.4%
+ ~Mathlib.MeasureTheory.Integral.Bochner                            instructions        -4.8%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                            instructions        -7.4%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure                       instructions       -31.1%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                        instructions        -6.9%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                  instructions       -20.9%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                    instructions       -11.0%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding               instructions        -8.0%
+ ~Mathlib.NumberTheory.NumberField.Units                            instructions        -7.6%
+ ~Mathlib.NumberTheory.RamificationInertia                          instructions       -10.4%
+ ~Mathlib.RepresentationTheory.Character                            instructions       -11.6%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution           instructions        -1.3%
+ ~Mathlib.RepresentationTheory.Rep                                  instructions        -4.9%
+ ~Mathlib.RingTheory.Adjoin.Field                                   instructions       -17.7%
+ ~Mathlib.RingTheory.AdjoinRoot                                     instructions        -3.5%
+ ~Mathlib.RingTheory.AlgebraicIndependent                           instructions        -8.9%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                   instructions       -12.5%
+ ~Mathlib.RingTheory.FinitePresentation                             instructions       -13.5%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                            instructions       -22.5%
+ ~Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal                 instructions       -24.3%
+ ~Mathlib.RingTheory.HahnSeries                                     instructions        -5.3%
+ ~Mathlib.RingTheory.Ideal.Quotient                                 instructions       -14.1%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                       instructions        -5.8%
+ ~Mathlib.RingTheory.Norm                                           instructions        -9.5%
+ ~Mathlib.RingTheory.Nullstellensatz                                instructions       -29.5%
+ ~Mathlib.RingTheory.Perfection                                     instructions        -4.5%
+ ~Mathlib.RingTheory.Polynomial.Quotient                            instructions       -26.0%
+ ~Mathlib.RingTheory.PowerSeries.Basic                              instructions        -3.9%
+ ~Mathlib.RingTheory.Subring.Basic                                  instructions       -11.6%
+ ~Mathlib.RingTheory.Valuation.Basic                                instructions        -4.9%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                     instructions       -13.1%
+ ~Mathlib.RingTheory.WittVector.Isocrystal                          instructions       -15.1%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass              instructions       -10.8%

[semorrison]

That benchmark is great news!