experiment: Ideal.IsTwoSided

[alreadydone]

to understand where exactly slowdowns occur.

---

[alreadydone]

!bench

[github-actions]

PR summary cff8891989

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsTwoSided
+ instance (priority := low) : I.IsTwoSided := ⟨fun b ha ↦ mul_comm b _ ▸ I.smul_mem _ ha⟩
+ instance : Coe R (R ⧸ I)
+ instance {α} [CommRing α] (I : Ideal α) : I.IsTwoSided := inferInstance
+ ring
- instance {I : Ideal R} : Coe R (R ⧸ I)

You can run this locally as follows

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

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[leanprover-bot]

Here are the benchmark results for commit d6cb66c.
There were no significant changes against commit 75faccb.

[alreadydone]

!bench

[leanprover-bot]

Here are the benchmark results for commit cc5f3cc.
There were significant changes against commit 75faccb:

  Benchmark                             Metric         Change
  ===========================================================
- ~Mathlib.FieldTheory.LinearDisjoint   instructions     7.8%
- ~Mathlib.LinearAlgebra.Semisimple     instructions    16.5%

[alreadydone]

!bench

[leanprover-bot]

Here are the benchmark results for commit 0202c36.
There were significant changes against commit 75faccb:

  Benchmark                                         Metric         Change
  =======================================================================
- ~Mathlib.NumberTheory.RamificationInertia.Basic   instructions     6.4%

[alreadydone]

!bench

[leanprover-bot]

Here are the benchmark results for commit ef3c6f8.
There were significant changes against commit 75faccb:

  Benchmark                                         Metric         Change
  =======================================================================
- ~Mathlib.NumberTheory.RamificationInertia.Basic   instructions     7.1%

[kbuzzard]

Do you have a feeling for exactly what is slower in that file?

[kbuzzard]

All but three declarations in that file seem to compile really quickly. The three which are slow are

count_heartbeats in -- 45639 on Ideal.isTwoSided, 45569 on master
def powQuotSuccInclusion (i : ℕ) :

count_heartbeats in -- 111354 on master, 113597 on Ideal.isTwoSided
theorem powQuotSuccInclusion_injective (i : ℕ) :

count_heartbeats in -- 41679 on Ideal.isTwoSided, 33146 on master
noncomputable def quotientToQuotientRangePowQuotSucc

[alreadydone]

Thanks! Though RamificationInertia isn't my main concern; I spent a lot of efforts figuring out why AdjoinRoot gets slower in #17930, and I'm trying to isolate each confounding factor. In the latest run it only gets 0.154% slower, and in some earlier runs here it even got faster.

[alreadydone]

!bench

[kbuzzard]

Ploughing through the traces in quotientToQuotientRangePowQuotSucc. On master we have

  [tryResolve] [0.004334] ✅️ Module (R ⧸ p)
      (↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸
        LinearMap.range
          (p.powQuotSuccInclusion P
            i)) ≟ Module (R ⧸ p) (↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (p.powQuotSuccInclusion P i)) ▼
  [] [0.000015] ✅️ Ring (R ⧸ p) ▼
  [] result CommRing.toRing (cached) 
  [] [0.000365] ✅️ AddCommGroup ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ▶

and on Ideal.isTwoSided_minimization we have

  [tryResolve] [0.008238] ✅️ Module (R ⧸ p)
      (↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸
        LinearMap.range
          (p.powQuotSuccInclusion P
            i)) ≟ Module (R ⧸ p) (↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (p.powQuotSuccInclusion P i)) ▼
  [] [0.000182] ✅️ Ring (R ⧸ p) ▼
  [] result Quotient.ring p (cached) 
  [] [0.000319] ✅️ AddCommGroup ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ▶

Two observations. The first is that these numbers don't add up. Most of the 0.004 seconds on master is unexplained, the only two numbers we have add up to under 0.0004 which is 10% of the total time. Similar comment for this branch. The second observation is that it takes ten times as long to find a cached Quotient.ring p ring structure on R / P as it does to find a cached CommRing.toRing apparently.

[alreadydone]

Thanks! Are these outputs from set_option trace.Meta.synthInstance true? Maybe it's not just instance synthesis that got slower ...

[alreadydone]

!bench

[leanprover-bot]

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

[leanprover-bot]

Here are the benchmark results for commit a23c4ea.
There were significant changes against commit 75faccb:

  Benchmark                                         Metric         Change
  =======================================================================
- ~Mathlib.AlgebraicGeometry.EllipticCurve.Group    instructions     5.5%
- ~Mathlib.LinearAlgebra.Semisimple                 instructions    21.6%
- ~Mathlib.NumberTheory.KummerDedekind              instructions    35.2%
- ~Mathlib.NumberTheory.RamificationInertia.Basic   instructions    10.0%
- ~Mathlib.RingTheory.AdjoinRoot                    instructions    35.2%
- ~Mathlib.RingTheory.Ideal.Quotient.Operations     instructions    38.3%
- ~Mathlib.RingTheory.Jacobson.Ring                 instructions    15.8%
- ~Mathlib.RingTheory.Polynomial.Quotient           instructions    25.7%

[alreadydone]

!bench

[leanprover-bot]

Here are the benchmark results for commit f973064.
There were significant changes against commit 75faccb:

  Benchmark                                         Metric         Change
  =======================================================================
- ~Mathlib.AlgebraicGeometry.EllipticCurve.Group    instructions     5.6%
- ~Mathlib.LinearAlgebra.Semisimple                 instructions    21.5%
- ~Mathlib.NumberTheory.RamificationInertia.Basic   instructions     4.9%
- ~Mathlib.RingTheory.AdjoinRoot                    instructions    26.1%
- ~Mathlib.RingTheory.Ideal.Quotient.Operations     instructions    21.4%
- ~Mathlib.RingTheory.Jacobson.Ring                 instructions    12.6%

[alreadydone]

!bench

[leanprover-bot]

Here are the benchmark results for commit 233e123.
There were significant changes against commit 75faccb:

  Benchmark                                         Metric         Change
  =======================================================================
- ~Mathlib.AlgebraicGeometry.EllipticCurve.Group    instructions     5.6%
- ~Mathlib.LinearAlgebra.Semisimple                 instructions    21.5%
- ~Mathlib.NumberTheory.RamificationInertia.Basic   instructions     5.0%
- ~Mathlib.RingTheory.AdjoinRoot                    instructions    26.1%
- ~Mathlib.RingTheory.Ideal.Quotient.Operations     instructions    21.4%
- ~Mathlib.RingTheory.Jacobson.Ring                 instructions    12.6%

[alreadydone]

!bench

[leanprover-bot]

Here are the benchmark results for commit cff8891.
There were significant changes against commit 75faccb:

  Benchmark                                         Metric         Change
  =======================================================================
- ~Mathlib.AlgebraicGeometry.EllipticCurve.Group    instructions     5.6%
- ~Mathlib.LinearAlgebra.Semisimple                 instructions    21.5%
- ~Mathlib.NumberTheory.RamificationInertia.Basic   instructions     4.9%
- ~Mathlib.RingTheory.AdjoinRoot                    instructions    26.1%
- ~Mathlib.RingTheory.Ideal.Quotient.Operations     instructions    21.4%
- ~Mathlib.RingTheory.Jacobson.Ring                 instructions    12.6%

[MichaelStollBayreuth]

General information:

lint:                                                  +15.323 * 10⁹ (+0.210%)
build:                                                 +255.16 * 10⁹ (+0.175%)

39 files got slower by at least 10⁹ instructions

Mathlib.RingTheory.AdjoinRoot:                         +35.926 * 10⁹ (+26.1%)
Mathlib.RingTheory.Ideal.Quotient.Operations:          +28.137 * 10⁹ (+21.4%)
Mathlib.LinearAlgebra.Semisimple:                      +23.570 * 10⁹ (+21.5%)
Mathlib.RingTheory.Jacobson.Ring:                      +11.991 * 10⁹ (+12.6%)
Mathlib.AlgebraicGeometry.EllipticCurve.Group:         +10.772 * 10⁹ (+5.59%)
Mathlib.NumberTheory.RamificationInertia.Basic:        +10.362 * 10⁹ (+4.94%)
Mathlib.RingTheory.Polynomial.Quotient:                +9.9087 * 10⁹ (+19.0%)
Mathlib.RingTheory.Kaehler.Basic:                      +8.9860 * 10⁹ (+2.88%)
Mathlib.NumberTheory.KummerDedekind:                   +8.9233 * 10⁹ (+17.5%)
Mathlib.RingTheory.LocalRing.ResidueField.Basic:       +6.7685 * 10⁹ (+22.7%)
Mathlib.Topology.Algebra.Valued.LocallyCompact:        +5.9294 * 10⁹ (+9.70%)
Mathlib.RingTheory.Ideal.Over:                         +5.4946 * 10⁹ (+6.46%)
Mathlib.FieldTheory.KummerExtension:                   +5.0513 * 10⁹ (+4.01%)
Mathlib.RingTheory.Ideal.Cotangent:                    +4.7227 * 10⁹ (+5.80%)
Mathlib.RingTheory.Smooth.Pi:                          +3.6497 * 10⁹ (+13.4%)
Mathlib.RingTheory.Invariant:                          +3.6194 * 10⁹ (+6.73%)
Mathlib.FieldTheory.LinearDisjoint:                    +3.4544 * 10⁹ (+1.48%)
Mathlib.RingTheory.Regular.RegularSequence:            +3.2422 * 10⁹ (+3.65%)
Mathlib.RingTheory.LocalRing.Quotient:                 +3.2108 * 10⁹ (+11.8%)
Mathlib.RingTheory.Nullstellensatz:                    +2.9621 * 10⁹ (+10.9%)
Mathlib.RingTheory.Trace.Quotient:                     +2.8128 * 10⁹ (+4.84%)
Mathlib.RingTheory.DedekindDomain.Ideal:               +2.6922 * 10⁹ (+1.17%)
Mathlib.RingTheory.PowerSeries.Inverse:                +2.4410 * 10⁹ (+8.31%)
Mathlib.RingTheory.Valuation.ValuationSubring:         +2.4078 * 10⁹ (+1.58%)
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic:
                                                       +2.2458 * 10⁹ (+2.69%)
Mathlib.RingTheory.Smooth.Basic:                       +1.8006 * 10⁹ (+6.12%)
Mathlib.RingTheory.AdicCompletion.Algebra:             +1.7810 * 10⁹ (+2.09%)
Mathlib.RingTheory.Smooth.Kaehler:                     +1.7640 * 10⁹ (+0.723%)
Mathlib.RingTheory.Ideal.Quotient.Basic:               +1.6813 * 10⁹ (+6.13%)
Mathlib.RingTheory.MvPolynomial.Localization:          +1.5723 * 10⁹ (+4.42%)
Mathlib.RingTheory.QuotSMulTop:                        +1.3345 * 10⁹ (+3.14%)
Mathlib.RingTheory.Ideal.MinimalPrime:                 +1.3287 * 10⁹ (+7.92%)
Mathlib.LinearAlgebra.InvariantBasisNumber:            +1.2710 * 10⁹ (+6.13%)
Mathlib.RingTheory.Jacobson.Ideal:                     +1.2585 * 10⁹ (+5.52%)
Mathlib.RingTheory.EisensteinCriterion:                +1.2455 * 10⁹ (+12.9%)
Mathlib.RingTheory.Unramified.Field:                   +1.2133 * 10⁹ (+1.97%)
Mathlib.Analysis.CStarAlgebra.GelfandDuality:          +1.1362 * 10⁹ (+1.40%)
Mathlib.Algebra.CharP.MixedCharZero:                   +1.1243 * 10⁹ (+7.99%)
Mathlib.RingTheory.Ideal.Quotient.Nilpotent:           +1.0552 * 10⁹ (+13.7%)

13 files got slower by at least 10%

Mathlib.RingTheory.AdjoinRoot:                                        +26.1%
Mathlib.RingTheory.LocalRing.ResidueField.Basic:                      +22.7%
Mathlib.LinearAlgebra.Semisimple:                                     +21.5%
Mathlib.RingTheory.Ideal.Quotient.Operations:                         +21.4%
Mathlib.RingTheory.Polynomial.Quotient:                               +19.0%
Mathlib.NumberTheory.KummerDedekind:                                  +17.5%
Mathlib.RingTheory.Ideal.Quotient.Nilpotent:                          +13.7%
Mathlib.RingTheory.Smooth.Pi:                                         +13.4%
Mathlib.RingTheory.EisensteinCriterion:                               +12.9%
Mathlib.RingTheory.Jacobson.Ring:                                     +12.6%
Mathlib.RingTheory.LocalRing.Quotient:                                +11.8%
Mathlib.RingTheory.Jacobson.Polynomial:                               +10.9%
Mathlib.RingTheory.Nullstellensatz:                                   +10.9%

No file got faster by at least 10⁹ instructions.

No file got faster by at least 10%.