timing depends on whether file is in Mathlib dir?

Stream: mathlib4

[Kevin Buzzard]

I was very surprised to find the following.
Create a file called scratch.lean in the root directory of Mathlib (i.e. not in the Mathlib/ directory where all the Lean files are). And populate it with this:

import Mathlib

suppress_compilation

variable (F : Type*) [Field F] [NumberField F]

variable (D : Type*) [Ring D] [Algebra F D]

namespace TotallyDefiniteQuaternionAlgebra

open scoped TensorProduct NumberField

open IsDedekindDomain

instance : CommRing (FiniteAdeleRing (𝓞 F) F) := inferInstance
instance : Ring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) := inferInstance

set_option trace.profiler true in
#count_heartbeats in -- 10037 in root , 23198 in Mathlib/
#synth Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F)

Now create a second file called Mathlib/scratch.lean and populate it with exactly the same thing. Tada: instance synthesis now takes twice as long (according to both the profiler and count_heartbeats).

I discovered this when trying to debug a slowdown in FLT, I was minimising in a scratch file which wasn't in FLT/ and it was much quicker. I didn't even know that this could happen. Can someone else reproduce or do I just need to turn it off and on again? This was on a recent master but I observed the same behaviour on tag v4.19.0.

[Eric Wieser]

Does disabling linting have the same effect?

[Kevin Buzzard]

how do I disable linting? Does that involve typing in about 20 things?

[Eric Wieser]

The extreme version is

-- no undoing this without restarting the file, commenting it out won't work
run_cmd Lean.Elab.Command.lintersRef.set #[]

[Kevin Buzzard]

I put that line in both files, restarted the server, and am still observing the same phenomenon. I'll dump the traces to a file and get the diffs.

[Kevin Buzzard]

dammit I can't use lake to build the file outside Mathlib

[Eric Wieser]

is the one outside mathlib the same lean version?

[Kevin Buzzard]

lean --version is producing the same output in both the root directory and in the Mathlib subdirectory. And adding #eval Lean.versionString to both files produces the same output.

[Kevin Buzzard]

I am kind of in shock right now because after I added a "check FLT.lean contains all the files in FLT/" linter to CI in FLT I had to move my scratch directory out of FLT/ (because I kept accidentally adding scratch files to FLT.lean when I ran lake exe mk-all) and I had no idea that this would change anything.

[Damiano Testa]

Kevin Buzzard said:

(because I kept accidentally adding scratch files to FLT.lean when I ran lake exe mk-all)

Have you tried using lake exe mk_all --git, instead?

[Damiano Testa]

By the way, re the actual issue that you reported, I also observed that import Mathlib on projects that depend on mathlib seems faster than on mathlib itself. I wonder if it is a similar underlying reason.

[Kevin Buzzard]

Aah so you're saying that I can recover my 2x slowdown by using this mk-all variant? :-)

[Damiano Testa]

Exactly!

[Damiano Testa]

And then we can close this thread as resolved.

[Kenny Lau]

sorry i'm not exactly sure i understand what the conclusion was

[Kenny Lau]

it has to do with the mk_all file?

[Kenny Lau]

but the scratch files are not in the mk_all file

[Damiano Testa]

No, I think that Kevin found out about the issue because mk_all was adding non-git-tracked files to import all.

[Damiano Testa]

I simply mentioned that lake exe mk_all --git would only create an import all-git-tracked file.

[Damiano Testa]

The slowdown is still unresolved. If Kevin had known about the --git flag, this issue would have been preempted, since no one would have never noticed.

[Kevin Buzzard]

yeah mk_all caused the discovery but has nothing to do with the problem. I would like to compare traces but I don't know how to dump the trace of the file not in the Mathlib directory to a file.

[Eric Wieser]

lake env lean yourfile.lean or maybe lake lean yourfile.lean?

[Kevin Buzzard]

Looking at the traces manually and there is a difference in typeclass synthesis. In the slow file

[synthInstance] [0.472236] ✅️ LieRing (FiniteAdeleRing (𝓞 F) F) ▼
  [] [0.041777] ✅️ apply @RestrictedProduct.instRingCoeOfSubringClass to Ring (FiniteAdeleRing (𝓞 F) F) ▶
  [] [0.014545] ✅️ apply @UniformSpace.Completion.ring to (i : HeightOneSpectrum (𝓞 F)) →
        Ring (HeightOneSpectrum.adicCompletion F i) ▶
  [] [0.292250] ❌️ apply WithIdeal.instNonarchimedeanRing to ∀ (i : HeightOneSpectrum (𝓞 F)),
        NonarchimedeanRing (WithVal (HeightOneSpectrum.valuation F i)) ▶
  [] [0.074443] ✅️ apply @ValuationSubring.instSubringClass to ∀ (i : HeightOneSpectrum (𝓞 F)),
        SubringClass (ValuationSubring (HeightOneSpectrum.adicCompletion F i))
          (HeightOneSpectrum.adicCompletion F i) ▶
  [check] [0.018059] ✅️ LieRing.ofAssociativeRing
[] [0.019343] ✅️ SubNegMonoid.toAddMonoid =?= SubNegMonoid.toAddMonoid ▼

and in the fast file (again let me stress that this is character-for-character the same file, just in a different location)

[synthInstance] [0.060356] ✅️ LieRing (FiniteAdeleRing (𝓞 F) F) ▼
  [] [0.014654] ✅️ apply @UniformSpace.Completion.ring to (i : HeightOneSpectrum (𝓞 F)) →
        Ring (HeightOneSpectrum.adicCompletion F i) ▶
  [] [0.010935] ✅️ apply @ValuationSubring.instSubringClass to ∀ (i : HeightOneSpectrum (𝓞 F)),
        SubringClass (ValuationSubring (HeightOneSpectrum.adicCompletion F i))
          (HeightOneSpectrum.adicCompletion F i) ▶
[] [0.012450] ✅️ SubNegMonoid.toAddMonoid =?= SubNegMonoid.toAddMonoid ▶

[Kevin Buzzard]

so typeclass inference seems to be behaving differently in the two files shrug

[Floris van Doorn]

Yes, I also see different type class inference traces:
outside Mathlib

[Elab.command] [0.921671] #synth Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▼
  [Meta.synthInstance] [0.000249] ✅️ Field F ▶
  [Meta.synthInstance] [0.000648] ✅️ CommSemiring F ▶
  [Meta.synthInstance] [0.003443] ✅️ Semiring D ▶
  [step] [0.583382] expected type: <not-available>, term
      Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▼
    [] [0.583282] expected type: Type (max u_1 u_2), term
        (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▼
      [] [0.583269] expected type: Type (max u_1 u_2), term
          D ⊗[F] FiniteAdeleRing (𝓞 F) F ▼
        [] [0.583139] expected type: Type (max u_1 u_2), term
            TensorProduct✝ F D (FiniteAdeleRing (𝓞 F) F) ▼
          [] [0.012553] expected type: Type u_1, term
              FiniteAdeleRing (𝓞 F) F ▼
            [Meta.synthInstance] [0.000124] ✅️ Field F ▶
            [Meta.synthInstance] [0.000220] ✅️ CommRing (𝓞 F) ▶
            [Meta.synthInstance] [0.000436] ✅️ IsDedekindDomain (𝓞 F) ▶
            [Meta.synthInstance] [0.000023] ✅️ Field F ▶
            [Meta.synthInstance] [0.004494] ✅️ Algebra (𝓞 F) F ▶
            [Meta.synthInstance] [0.000851] ✅️ IsFractionRing (𝓞 F) F ▶
          [Meta.synthInstance] [0.000563] ✅️ CommSemiring F ▶
          [Meta.synthInstance] [0.023315] ✅️ AddCommMonoid D ▶
          [Meta.synthInstance] [0.102239] ✅️ AddCommMonoid (FiniteAdeleRing (𝓞 F) F) ▶
          [Meta.synthInstance] [0.006492] ✅️ Module F D ▶
          [Meta.synthInstance] [0.383813] ✅️ Module F (FiniteAdeleRing (𝓞 F) F) ▶
          [Meta.isDefEq] [0.053174] ✅️ ?m.18716 =?= LieAlgebra.toModule ▶
  [Meta.synthInstance] [0.328889] ✅️ Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▼
    [] [0.000074] new goal Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▶
    [] [0.215802] ✅️ apply @Algebra.TensorProduct.instSemiring to Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▶
    [isDefEq] [0.065836] ✅️ Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) =?= Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▶
    [check] [0.046707] ✅️ Algebra.TensorProduct.instSemiring ▶
    [] result Algebra.TensorProduct.instSemiring

inside Mathlib

[Elab.command] [0.831129] #synth Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▼
  [Meta.synthInstance] [0.000151] ✅️ Field F ▶
  [Meta.synthInstance] [0.000483] ✅️ CommSemiring F ▶
  [Meta.synthInstance] [0.002658] ✅️ Semiring D ▶
  [step] [0.689016] expected type: <not-available>, term
      Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▼
    [] [0.688925] expected type: Type (max u_1 u_2), term
        (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▼
      [] [0.688914] expected type: Type (max u_1 u_2), term
          D ⊗[F] FiniteAdeleRing (𝓞 F) F ▼
        [] [0.688803] expected type: Type (max u_1 u_2), term
            TensorProduct✝ F D (FiniteAdeleRing (𝓞 F) F) ▼
          [Meta.synthInstance] [0.000096] ✅️ Field F ▶
          [Meta.synthInstance] [0.000171] ✅️ CommRing (𝓞 F) ▶
          [Meta.synthInstance] [0.000357] ✅️ IsDedekindDomain (𝓞 F) ▶
          [Meta.synthInstance] [0.000017] ✅️ Field F ▶
          [Meta.synthInstance] [0.003326] ✅️ Algebra (𝓞 F) F ▶
          [Meta.synthInstance] [0.000598] ✅️ IsFractionRing (𝓞 F) F ▶
          [Meta.synthInstance] [0.000454] ✅️ CommSemiring F ▶
          [Meta.synthInstance] [0.008607] ✅️ AddCommMonoid D ▶
          [Meta.synthInstance] [0.024117] ✅️ AddCommMonoid (FiniteAdeleRing (𝓞 F) F) ▶
          [Meta.synthInstance] [0.004967] ✅️ Module F D ▶
          [Meta.synthInstance] [0.627383] ✅️ Module F (FiniteAdeleRing (𝓞 F) F) ▶
          [Meta.isDefEq] [0.017395] ✅️ ?m.24839 =?= LieAlgebra.toModule ▶
  [Meta.synthInstance] [0.133231] ✅️ Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▼
    [] [0.000049] new goal Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▶
    [] [0.085615] ✅️ apply @Algebra.TensorProduct.instSemiring to Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▼
      [tryResolve] [0.085555] ✅️ Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ≟ Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▼
        [isDefEq] [0.051705] ✅️ Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) =?= Semiring (?m.37432 ⊗[?m.37431] ?m.37433) ▼
          [] [0.051676] ✅️ D ⊗[F] FiniteAdeleRing (𝓞 F) F =?= ?m.37432 ⊗[?m.37431] ?m.37433 ▼
            [synthInstance] [0.002619] ✅️ Semiring D ▶
            [synthInstance] [0.003738] ✅️ Semiring (FiniteAdeleRing (𝓞 F) F) ▶
            [] [0.043137] ✅️ LieAlgebra.toModule =?= Algebra.toModule ▼
              [] [0.043103] ✅️ Algebra.toModule =?= Algebra.toModule ▼
                [delta] [0.043090] ✅️ Algebra.toModule =?= Algebra.toModule ▼
                  [] [0.011402] ✅️ FiniteAdeleRing.instAlgebra (𝓞 F) F =?= ?m.37438 ▶
                  [] [0.031641] ✅️ Ring.toSemiring =?= CommSemiring.toSemiring ▶
        [isDefEq] [0.033624] ✅️ ?m.37421 =?= Algebra.TensorProduct.instSemiring ▶
      [answer] [0.000011] ✅️ Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F)
    [isDefEq] [0.034688] ✅️ Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) =?= Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) ▶
    [check] [0.012465] ✅️ Algebra.TensorProduct.instSemiring ▶
    [] result Algebra.TensorProduct.instSemiring

that's surprising.

[Kevin Buzzard]

I have no idea whether this is anything to do with anything, but with pp.explicit true the quick file has this in the trace:

    [isDefEq] [29.000000] ✅️ (i : @HeightOneSpectrum A i2) →
          SetLike
            (@ValuationSubring (@HeightOneSpectrum.adicCompletion A i2 i3 F i1 i4 i5 i)
              (@UniformSpace.Completion.instField
                (@WithVal F (WithZero (Multiplicative Int))
                  (@WithZero.instLinearOrderedCommGroupWithZero (Multiplicative Int)
...

and the slow file has this

    [isDefEq] [698518.000000] ✅️ (i : @HeightOneSpectrum A i2) →
          SetLike
            (@ValuationSubring (@HeightOneSpectrum.adicCompletion A i2 i3 F i1 i4 i5 i)
              (@UniformSpace.Completion.instField
                (@WithVal F (WithZero (Multiplicative Int))
                  (@WithZero.instLinearOrderedCommGroupWithZero (Multiplicative Int)
...

and the two very long terms, when written out in full, have the following diff:

1c1
<     [isDefEq] [698518.000000] ✅️ (i : @HeightOneSpectrum A i2) →
---
>     [isDefEq] [29.000000] ✅️ (i : @HeightOneSpectrum A i2) →
54c54
<                     (@Multiplicative.linearOrder Int Int.instLinearOrder) ⋯)
---
>                     (@Multiplicative.linearOrder Int Int.instLinearOrder) HeightOneSpectrum.intValuation._proof_1)
66c66
<                       (@Multiplicative.linearOrder Int Int.instLinearOrder) ⋯)
---
>                       (@Multiplicative.linearOrder Int Int.instLinearOrder) HeightOneSpectrum.intValuation._proof_1)
72c72
<                     (@Multiplicative.linearOrder Int Int.instLinearOrder) ⋯)
---
>                     (@Multiplicative.linearOrder Int Int.instLinearOrder) HeightOneSpectrum.intValuation._proof_1)
76c76
<                       (@Multiplicative.linearOrder Int Int.instLinearOrder) ⋯)
---
>                       (@Multiplicative.linearOrder Int Int.instLinearOrder) HeightOneSpectrum.intValuation._proof_1)

I don't really know what the ...s mean, is it likely that the terms are different because of some earlier divergence, or that the terms are the same but are being printed differently? Note the gigantic change in runtime for the defeq check.

[Eric Wieser]

... looks like a printing setting, which the lakefile only sets for mathlib

[Eric Wieser]

(or turns off for mathlib, one of the two)

[Eric Wieser]

I think https://github.com/leanprover-community/mathlib4/blob/cdf00c3262877ba8a9c34e58215d2a31dee64adb/lakefile.lean#L57 is the answer to this thread

[Kevin Buzzard]

Yes I believe you -- well spotted. I had found this monster example below, which was elaborating differently inside and outside mathlib, and indeed if I change maxSynthPendingDepth then it changes elaboration of the term.

import Mathlib
run_cmd Lean.Elab.Command.lintersRef.set #[]
#eval Lean.versionString

suppress_compilation

variable (F : Type) [i1 : Field F]
variable (A : Type) [i2 : CommRing A] [i3 : IsDedekindDomain A]
  [i4 : Algebra A F] [i5 : IsFractionRing A F]

open IsDedekindDomain

set_option maxSynthPendingDepth 0 in -- changing this changes things
set_option pp.all true in
#count_heartbeats in
#synth (i : @HeightOneSpectrum A i2) →
                        SetLike
                          (@ValuationSubring (@HeightOneSpectrum.adicCompletion A i2 i3 F i1 i4 i5 i)
                            (@UniformSpace.Completion.instField
                              (@WithVal F (WithZero (Multiplicative Int))
                                (@WithZero.instLinearOrderedCommGroupWithZero (Multiplicative Int)
                                  (@Multiplicative.commGroup Int Int.instAddCommGroup)
                                  (@Multiplicative.linearOrder Int Int.instLinearOrder)
                                  HeightOneSpectrum.intValuation._proof_1)
                                (@DivisionRing.toRing F (@Field.toDivisionRing F i1))
                                (@HeightOneSpectrum.valuation A i2 i3 F i1 i4 i5 i))
                              (@WithVal.instField F (WithZero (Multiplicative Int))
                                (@WithZero.instLinearOrderedCommGroupWithZero (Multiplicative Int)
                                  (@Multiplicative.commGroup Int Int.instAddCommGroup)
                                  (@Multiplicative.linearOrder Int Int.instLinearOrder)
                                  HeightOneSpectrum.intValuation._proof_1)
                                i1 (@HeightOneSpectrum.valuation A i2 i3 F i1 i4 i5 i))
                              (@Valued.toUniformSpace
                                (@WithVal F (WithZero (Multiplicative Int))
                                  (@WithZero.instLinearOrderedCommGroupWithZero (Multiplicative Int)
                                    (@Multiplicative.commGroup Int Int.instAddCommGroup)
                                    (@Multiplicative.linearOrder Int Int.instLinearOrder)
                                    HeightOneSpectrum.intValuation._proof_1)
                                  (@DivisionRing.toRing F (@Field.toDivisionRing F i1))
                                  (@HeightOneSpectrum.valuation A i2 i3 F i1 i4 i5 i))
                                (@WithVal.instRing F (WithZero (Multiplicative Int))
                                  (@WithZero.instLinearOrderedCommGroupWithZero (Multiplicative Int)
                                    (@Multiplicative.commGroup Int Int.instAddCommGroup)
                                    (@Multiplicative.linearOrder Int Int.instLinearOrder)
                                    HeightOneSpectrum.intValuation._proof_1)
                                  (@DivisionRing.toRing F (@Field.toDivisionRing F i1))
                                  (@HeightOneSpectrum.valuation A i2 i3 F i1 i4 i5 i))
                                (WithZero (Multiplicative Int))
                                (@WithZero.instLinearOrderedCommGroupWithZero (Multiplicative Int)
                                  (@Multiplicative.commGroup Int Int.instAddCommGroup)
                                  (@Multiplicative.linearOrder Int Int.instLinearOrder)
                                  HeightOneSpectrum.intValuation._proof_1)
                                (@WithVal.instValued (WithZero (Multiplicative Int))
                                  (@WithZero.instLinearOrderedCommGroupWithZero (Multiplicative Int)
                                    (@Multiplicative.commGroup Int Int.instAddCommGroup)
                                    (@Multiplicative.linearOrder Int Int.instLinearOrder)
                                    HeightOneSpectrum.intValuation._proof_1)
                                  F (@DivisionRing.toRing F (@Field.toDivisionRing F i1))
                                  (@HeightOneSpectrum.valuation A i2 i3 F i1 i4 i5 i)))
                              _ _ _))
                          (@HeightOneSpectrum.adicCompletion A i2 i3 F i1 i4 i5 i)

[Kevin Buzzard]

With maxSynthPendingDepth set to 0 the term starts

fun (i : @IsDedekindDomain.HeightOneSpectrum.{0} A i2) =>
  @ValuationSubring.instSetLike.{0} (@IsDedekindDomain.HeightOneSpectrum.adicCompletion.{0, 0} A i2 i3 F i1 i4 i5 i)
    (@UniformSpace.Completion.instField.{0}
      (@WithVal.{0, 0} F (WithZero.{0} (Multiplicative.{0} Int))
        (@WithZero.instLinearOrderedCommGroupWithZero.{0} (Multiplicative.{0} Int)
          (@Multiplicative.commGroup.{0} Int Int.instAddCommGroup)
          (@Multiplicative.linearOrder.{0} Int Int.instLinearOrder)
          IsDedekindDomain.HeightOneSpectrum.intValuation._proof_1)
        (@DivisionRing.toRing.{0} F (@Field.toDivisionRing.{0} F i1))
        (@IsDedekindDomain.HeightOneSpectrum.valuation.{0, 0} A i2 i3 F i1 i4 i5 i))
      (@WithVal.instField.{0, 0} F (WithZero.{0} (Multiplicative.{0} Int))
        (@WithZero.instLinearOrderedCommGroupWithZero.{0} (Multiplicative.{0} Int)
          (@Multiplicative.commGroup.{0} Int Int.instAddCommGroup)
          (@Multiplicative.linearOrder.{0} Int Int.instLinearOrder)
          IsDedekindDomain.HeightOneSpectrum.intValuation._proof_1)
        i1 (@IsDedekindDomain.HeightOneSpectrum.valuation.{0, 0} A i2 i3 F i1 i4 i5 i))
      (@Valued.toUniformSpace.{0, 0}
...

and with it set to 3 it looks like

fun (i : @IsDedekindDomain.HeightOneSpectrum.{0} A i2) =>
  @ValuationSubring.instSetLike.{0} (@IsDedekindDomain.HeightOneSpectrum.adicCompletion.{0, 0} A i2 i3 F i1 i4 i5 i)
    (@UniformSpace.Completion.instField.{0}
      (@WithVal.{0, 0} F (WithZero.{0} (Multiplicative.{0} Int))
        (@WithZero.instLinearOrderedCommGroupWithZero.{0} (Multiplicative.{0} Int)
          (@Multiplicative.commGroup.{0} Int Int.instAddCommGroup)
          (@Multiplicative.linearOrder.{0} Int Int.instLinearOrder)
          IsDedekindDomain.HeightOneSpectrum.intValuation._proof_1)
        (@DivisionRing.toRing.{0} F (@Field.toDivisionRing.{0} F i1))
        (@IsDedekindDomain.HeightOneSpectrum.valuation.{0, 0} A i2 i3 F i1 i4 i5 i))
      (@WithVal.instField.{0, 0} F (WithZero.{0} (Multiplicative.{0} Int))
        (@WithZero.instLinearOrderedCommGroupWithZero.{0} (Multiplicative.{0} Int)
          (@Multiplicative.commGroup.{0} Int Int.instAddCommGroup)
          (@Multiplicative.linearOrder.{0} Int Int.instLinearOrder)
          (@Multiplicative.isOrderedMonoid.{0} Int Int.instAddCommMonoid
            (@SemilatticeInf.toPartialOrder.{0} (Multiplicative.{0} Int)
              (@Lattice.toSemilatticeInf.{0} (Multiplicative.{0} Int)
                (@DistribLattice.toLattice.{0} (Multiplicative.{0} Int)
                  (@instDistribLatticeOfLinearOrder.{0} (Multiplicative.{0} Int)
                    (@Multiplicative.linearOrder.{0} Int Int.instLinearOrder)))))
            Int.instIsOrderedAddMonoid))
        i1 (@IsDedekindDomain.HeightOneSpectrum.valuation.{0, 0} A i2 i3 F i1 i4 i5 i))
      (@Valued.toUniformSpace.{0, 0}
...

[Kevin Buzzard]

In other words,

#check IsDedekindDomain.HeightOneSpectrum.intValuation._proof_1

#check (@Multiplicative.isOrderedMonoid.{0} Int Int.instAddCommMonoid
            (@SemilatticeInf.toPartialOrder.{0} (Multiplicative.{0} Int)
              (@Lattice.toSemilatticeInf.{0} (Multiplicative.{0} Int)
                (@DistribLattice.toLattice.{0} (Multiplicative.{0} Int)
                  (@instDistribLatticeOfLinearOrder.{0} (Multiplicative.{0} Int)
                    (@Multiplicative.linearOrder.{0} Int Int.instLinearOrder)))))
            Int.instIsOrderedAddMonoid)

are both proofs of IsOrderedMonoid (Multiplicative ℤ) and different ones are being found depending on the setting. Why does this affect IsDefEq though?

[Aaron Liu]

Kevin Buzzard said:

In other words,

#check IsDedekindDomain.HeightOneSpectrum.intValuation._proof_1

#check (@Multiplicative.isOrderedMonoid.{0} Int Int.instAddCommMonoid
            (@SemilatticeInf.toPartialOrder.{0} (Multiplicative.{0} Int)
              (@Lattice.toSemilatticeInf.{0} (Multiplicative.{0} Int)
                (@DistribLattice.toLattice.{0} (Multiplicative.{0} Int)
                  (@instDistribLatticeOfLinearOrder.{0} (Multiplicative.{0} Int)
                    (@Multiplicative.linearOrder.{0} Int Int.instLinearOrder)))))
            Int.instIsOrderedAddMonoid)

are both proofs of IsOrderedMonoid (Multiplicative ℤ) and different ones are being found depending on the setting. Why does this affect IsDefEq though?

The two proofs are actually the same, just one has been wrapped up

[Aaron Liu]

Try #print IsDedekindDomain.HeightOneSpectrum.intValuation._proof_1 and see the result

[Kevin Buzzard]

Well sounds like I'm talking about a red herring then, but Eric's answer is certainly correct:

import Mathlib

suppress_compilation

variable (F : Type*) [Field F] [NumberField F]

variable (D : Type*) [Ring D] [Algebra F D]

namespace TotallyDefiniteQuaternionAlgebra

open scoped TensorProduct NumberField

open IsDedekindDomain

instance : CommRing (FiniteAdeleRing (𝓞 F) F) := inferInstance
instance : Ring (D ⊗[F] FiniteAdeleRing (𝓞 F) F) := inferInstance

set_option maxSynthPendingDepth 1 in
#count_heartbeats in -- 6672
#synth Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F)

set_option maxSynthPendingDepth 3 in
#count_heartbeats in -- 20002
#synth Semiring (D ⊗[F] FiniteAdeleRing (𝓞 F) F)