erw and IsDedekindDomain.HeightOneSpectrum.adicCompletion

Stream: mathlib4

[Kevin Buzzard]

Finite adele rings don't really have a lot of love right now in mathlib and I need to use them for FLT so I'm trying to get on top of what's going on in the relevant files. When trying to write some code extending the API for these objects, I got myself into a situation where rw failed and erw worked, but if I wrote change <copy the goal here> beforehand then rw suddenly worked again. I've managed to debug this...to a certain extent.

In Mathlib/RingTheory/DedekindDomain/AdicValuation.lean there's the definition docs#IsDedekindDomain.HeightOneSpectrum.adicCompletion :

def adicCompletion :=
  @UniformSpace.Completion K v.adicValued.toUniformSpace

On lines 431 to 432 of that file, we have

      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
      erw [mem_adicCompletionIntegers, h, Valued.valuedCompletion_apply]

We can take this apart as

      rw [mem_adicCompletionIntegers, h]
      -- ⊢ Valued.v (↑K ((algebraMap R K) r)) ≤ 1
      erw [Valued.valuedCompletion_apply]

and erw fails if you change it to rw. (NB That ↑K in the goal is pretty weird, but this is a coercion issue unrelated to what I want to talk about here; this is a coercion docs#UniformSpace.Completion.coe' which takes an explicit input and the input is being displayed explicitly. )

OK so here's a fix to make that erw into a rw: just change the goal to itself :-/

      rw [mem_adicCompletionIntegers, h]
      -- ⊢ Valued.v (↑K ((algebraMap R K) r)) ≤ 1
      change Valued.v (↑((algebraMap R K) r) : UniformSpace.Completion K) ≤ 1
      -- ⊢ Valued.v (↑K ((algebraMap R K) r)) ≤ 1
      rw [Valued.valuedCompletion_apply] -- now works fine

With pp.all on of course there _is_ a difference (quite a large one), and the main difference is that, for reasons unknown to me, the change line is unfolding IsDedekindDomain.HeightOneSpectrum.adicCompletion. Indeed, this works too:

      rw [mem_adicCompletionIntegers, h]
      unfold IsDedekindDomain.HeightOneSpectrum.adicCompletion -- no visible effect on goal
      rw [Valued.valuedCompletion_apply] -- now works fine

I don't know why change is choosing to do this, but it occurred to me that this might be evidence that if we want to avoid erw then perhaps IsDedekindDomain.HeightOneSpectrum.adicCompletion should be an abbrev rather than a def. So I tried making this change, and the consequences are:

1) The erw around line 431 can be changed back to a rw;
2) the porting note around line 438 ("this proof used to be X") -- the original proof X now works again;
3) The erw on line 445 can be changed to a rw (except that this erw is now going to be deleted completely because of point (2));
4) The porting notes "added dsimp" on lines 461 and 466 or so can now be deleted;
and, unfortunately
5) the instance at the end of the file breaks :-(

The issue at the end of the file is that

#synth SMul (↥(adicCompletionIntegers K v)) (adicCompletion K v)

used to work, but now fails. Here

def adicCompletionIntegers : ValuationSubring (v.adicCompletion K) :=
  Valued.v.valuationSubring

So here are some proposals:

1) Leave IsDedekindDomain.HeightOneSpectrum.adicCompletion as a def, add

lemma adicCompletion_def : v.adicCompletion K = @UniformSpace.Completion K v.adicValued.toUniformSpace := rfl

and then add in a bunch of simp_rw [adicCompletion_def], e.g.

     erw [mem_adicCompletionIntegers, Valued.valuedCompletion_apply]

becomes

      simp_rw [mem_adicCompletionIntegers, adicCompletion_def, Valued.valuedCompletion_apply]

(you need simp_rw not rw because the adicCompletion is buried in the term, and the motive isn't type correct if you just rw).

2) Make it an abbrev, get nice clean code, delete some porting notes, and then deal with the fact that even though

#synth CommRing (adicCompletion K v)

works,

#synth SMul (adicCompletion K v) (adicCompletion K v)

fails (?!). This can be fixed with

instance : Algebra (adicCompletion K v) (adicCompletion K v) := Algebra.id _

but this is perhaps indicative of something not being OK.

Any suggestions?

[Kevin Buzzard]

Thinking about this a bit more, I'm minded to go for the abbrev approach and try and debug the typeclass instance failure. The trace for this

variable (A : Type*) [CommRing A] in
#synth Algebra A A

is

[Meta.synthInstance] ✅ Algebra A A ▼
  [] new goal Algebra A A ▼
    [instances] #[Algebra.id, inst✝²]
  [] ❌ apply inst✝² to Algebra A A ▶
  [] ✅ apply Algebra.id to Algebra A A ▶
  [] result Algebra.id A

However the trace for this

#synth Algebra (adicCompletion K v) (adicCompletion K v) -- fails

is this:

[Meta.synthInstance] 💥 Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
      (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ▼
  [] new goal Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
        (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ▼
    [instances] #[Algebra.id, UniformSpace.Completion.algebra, UniformSpace.Completion.algebra', IsDedekindDomain.HeightOneSpectrum.AdicCompletion.algebra', IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion, inst✝¹]
  [] ❌ apply inst✝¹ to Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
        (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ▶
  [] ❌ apply IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion to Algebra
        (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ▶
  [] 💥 apply IsDedekindDomain.HeightOneSpectrum.AdicCompletion.algebra' to Algebra
        (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ▶

My reading of that trace is: "there are 6 ways that Lean can think of as feasible for finding this instance; the one which works (Algebra.id) is the most fundamental and is hence tried last because of design decisions which I am still not 100% sure that I buy, and of the five other ways, the first two fail and then the third one explodes (what the heck does 💥 mean and how is it different from ❌?) and for some reason we can never recover from the explosion and try the other two instances including the one which would have worked."

[Ruben Van de Velde]

Is the explosion "ran out of heartbeats"?

[Kevin Buzzard]

The error is failed to synthesize Algebra (adicCompletion K v) (adicCompletion K v) (as opposed to "please bump up heartbeats").

Here's a mwe:

import Mathlib.RingTheory.DedekindDomain.Ideal
import Mathlib.RingTheory.Valuation.ExtendToLocalization
import Mathlib.Topology.Algebra.ValuedField
import Mathlib.Algebra.Order.Group.TypeTags

noncomputable section

open scoped Classical DiscreteValuation

open IsDedekindDomain

variable {R : Type*} [CommRing R] [IsDedekindDomain R] {K : Type*} [Field K]
  [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R)

namespace IsDedekindDomain.HeightOneSpectrum

def intValuationDef (r : R) : ℤₘ₀ :=
  if r = 0 then 0
  else
    ↑(Multiplicative.ofAdd
      (-(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r} : Ideal R)).factors : ℤ))

theorem int_valuation_ne_zero' (x : nonZeroDivisors R) : v.intValuationDef x ≠ 0 :=
  sorry

/-- The `v`-adic valuation on `R`. -/
def intValuation : Valuation R ℤₘ₀ where
  toFun := v.intValuationDef
  map_zero' := sorry
  map_one' := sorry
  map_mul' := sorry
  map_add_le_max' := sorry

def valuation (v : HeightOneSpectrum R) : Valuation K ℤₘ₀ :=
  v.intValuation.extendToLocalization
    (fun r hr => Set.mem_compl <| v.int_valuation_ne_zero' ⟨r, hr⟩) K

def adicValued : Valued K ℤₘ₀ :=
  Valued.mk' v.valuation

variable (K)

abbrev adicCompletion :=
  @UniformSpace.Completion K v.adicValued.toUniformSpace

#synth Algebra (v.adicCompletion K) (v.adicCompletion K) -- works

instance AdicCompletion.algebra' : Algebra R (v.adicCompletion K) := sorry

#synth Algebra (v.adicCompletion K) (v.adicCompletion K) -- fails

[Kevin Buzzard]

If you don't like the sorried data in AdicCompletion.algebra', then another approach is to open the file Mathlib/RingTheory/DedekindDomain/AdicValuation.lean, change def adicCompletion := on line 336 to abbrev adicCompletion := and then observe that #synth Algebra (adicCompletion K v) (adicCompletion K v) doesn't work at the end of the file just before the error, but does work before line 395 where the exploding algebra' instance is defined)

[Kevin Buzzard]

It also fails on nightly-testing with what looks like the same failure, which is this:

[Meta.synthInstance] 💥 Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
      (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ▼
  [] new goal Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
        (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ▼
    [instances] #[Algebra.id, UniformSpace.Completion.algebra, UniformSpace.Completion.algebra', IsDedekindDomain.HeightOneSpectrum.AdicCompletion.algebra', inst✝¹]
  [] ❌ apply inst✝¹ to Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
        (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ▶
  [] 💥 apply IsDedekindDomain.HeightOneSpectrum.AdicCompletion.algebra' to Algebra
        (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ▼
    [tryResolve] 💥 Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
          (IsDedekindDomain.HeightOneSpectrum.adicCompletion K
            v) ≟ Algebra ?m.391137 (IsDedekindDomain.HeightOneSpectrum.adicCompletion ?m.391140 ?m.391144) ▼
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▼
        [] new goal Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
        [] ❌ apply inst✝¹ to Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
        [] ❌ apply Algebra.id to Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▼
        [] result <not-available> (cached)
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶
      [] ❌ Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K ▶

[Michael Stoll]

The question is, why does it try Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) K so many times?

[Kevin Buzzard]

Just to be clear, I didn't truncate; it tries it that many times.

[Michael Stoll]

(after it decided that such an instance is not available the first time round)

[Kevin Buzzard]

My understanding of this trace is: "we need to find an Algebra instance, there are 5 ways to do it; the 5th one we'll try will work but we're not to know this yet; the first one fails, the second one explodes and we never recover, finishing by asking the same question 15 times"

[Kevin Buzzard]

This was supposed to be a question about the subtleties of rw v erw but I'm becoming convinced that the solution is just to change the def to an abbrev and then work around this issue somehow.

[Michael Stoll]

With set_option trace.Meta.synthPending true, I see [synthPending] synthPending ?m.8600 each time this is tried, but I have no idea what this means (there is no ?m8600 elsewhere in the output).

[Michael Stoll]

My feeling is that this is a bug in the instance synthesis algorithm.

[Michael Stoll]

It would be good to minimize this more. (I need to get some sleep, though.)

[Jovan Gerbscheid]

If you set_option trace.Meta.isDefEq true, you can see that the unification invoked by this instance does a lot of stuff, and throws an error in the end. In the type class resolution algorithm, there is one big tryCatch function on the outside, but there is no tryCatch around the individual isDefEq calls. It is for this reason that the error propagates all the way to the outside, and the other instances are not attempted.

[Kevin Buzzard]

I have it down to this but it's not going to get any smaller and it's still huge, it uses loads of algebra and loads of topology:

import Mathlib.RingTheory.DedekindDomain.Ideal
import Mathlib.RingTheory.Valuation.ExtendToLocalization
import Mathlib.Topology.Algebra.ValuedField
import Mathlib.Algebra.Order.Group.TypeTags

open scoped Classical DiscreteValuation

open IsDedekindDomain

variable {R : Type*} [CommRing R] [IsDedekindDomain R] {K : Type*} [Field K]
  [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R)

namespace IsDedekindDomain.HeightOneSpectrum

def intValuation {R : Type*} [CommRing R] [IsDedekindDomain R]
  (v : HeightOneSpectrum R) : Valuation R ℤₘ₀ where
  toFun r := if r = 0 then 0 else 0 -- just 0 doesn't work
  map_zero' := sorry
  map_one' := sorry
  map_mul' := sorry
  map_add_le_max' := sorry

-- this uses loads of algebra
noncomputable def valuation {R : Type*} [CommRing R] [IsDedekindDomain R] {K : Type*}
    [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Valuation K ℤₘ₀ :=
  v.intValuation.extendToLocalization
    (sorry : nonZeroDivisors R ≤ v.intValuation.supp.primeCompl) K

variable (K)

-- this uses loads of topology
abbrev adicCompletion :=
  @UniformSpace.Completion K (Valued.mk' v.valuation).toUniformSpace

#synth Algebra (adicCompletion K v) (adicCompletion K v) -- works

instance AdicCompletion.algebra' {R : Type u_1} [CommRing R] [IsDedekindDomain R] [DecidableEq R]
    (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
  Algebra R (v.adicCompletion K) := sorry

-- set_option trace.Meta.synthInstance true
-- set_option trace.Meta.isDefEq true
#synth Algebra (adicCompletion K v) (adicCompletion K v) -- fails

@Jovan Gerbscheid what is this "error in the end"? Are you talking about

                                                      [onFailure] 💥 Decidable.rec (fun h ↦ (fun x ↦ 0) h) (fun h ↦ (fun x ↦ 0) h)
                                                            (Classical.propDecidable
                                                              (((IsLocalization.toLocalizationMap (nonZeroDivisors R)
                                                                        K).sec
                                                                    z).1 =
                                                                0)) =?= Decidable.rec (fun h ↦ (fun x ↦ 0) h)
                                                            (fun h ↦ (fun x ↦ 0) h)
                                                            (Classical.propDecidable
                                                              (((IsLocalization.toLocalizationMap
                                                                        (nonZeroDivisors
                                                                          (IsDedekindDomain.HeightOneSpectrum.adicCompletion
                                                                            K v))
                                                                        K).sec
                                                                    z).1 =
                                                                0))

?

[Jovan Gerbscheid]

Hmmm, when setting set_option trace.Meta.isDefEq.hint true, the trace goes a bit further even.

[Kevin Buzzard]

It's possible to remove Classical and add decidable instances instead:

import Mathlib.RingTheory.DedekindDomain.Ideal
import Mathlib.RingTheory.Valuation.ExtendToLocalization
import Mathlib.Topology.Algebra.ValuedField
import Mathlib.Algebra.Order.Group.TypeTags

open scoped DiscreteValuation

open IsDedekindDomain

variable {R : Type*} [CommRing R] [IsDedekindDomain R] [DecidableEq R] {K : Type*} [Field K]
  [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R)

namespace IsDedekindDomain.HeightOneSpectrum

def intValuation {R : Type*} [CommRing R] [IsDedekindDomain R] [DecidableEq R]
  (v : HeightOneSpectrum R) : Valuation R ℤₘ₀ where
  toFun r := if r = 0 then 0 else 0 -- just 0 doesn't work
  map_zero' := sorry
  map_one' := sorry
  map_mul' := sorry
  map_add_le_max' := sorry

-- this uses loads of algebra
noncomputable def valuation {R : Type*} [CommRing R] [IsDedekindDomain R] [DecidableEq R] {K : Type*}
    [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Valuation K ℤₘ₀ :=
  v.intValuation.extendToLocalization
    (sorry : nonZeroDivisors R ≤ v.intValuation.supp.primeCompl) K

variable (K)

-- this uses loads of topology
abbrev adicCompletion :=
  @UniformSpace.Completion K (Valued.mk' v.valuation).toUniformSpace

#synth Algebra (adicCompletion K v) (adicCompletion K v) -- works

instance AdicCompletion.algebra' {R : Type u_1} [CommRing R] [IsDedekindDomain R] [DecidableEq R]
    (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
  Algebra R (v.adicCompletion K) := sorry

-- set_option trace.Meta.synthInstance true
--set_option trace.Meta.isDefEq true
--set_option trace.Meta.isDefEq.hint true
#synth Algebra (adicCompletion K v) (adicCompletion K v) -- fails

[Jovan Gerbscheid]

In the trace, I see at the end a [onFailure] trace node with the explode emoji, followed by two [hint] traces. Here is the code that must have thrown an error:

@[specialize] private def unstuckMVar (e : Expr) (successK : Expr → MetaM Bool) (failK : MetaM Bool): MetaM Bool := do
  match (← getStuckMVar? e) with
  | some mvarId =>
    trace[Meta.isDefEq.stuckMVar] "found stuck MVar {mkMVar mvarId} : {← inferType (mkMVar mvarId)}"
    if (← Meta.synthPending mvarId) then
      let e ← instantiateMVars e
      successK e
    else
      failK
  | none   => failK

private def isDefEqOnFailure (t s : Expr) : MetaM Bool := do
  withTraceNodeBefore `Meta.isDefEq.onFailure (return m!"{t} =?= {s}") do
    unstuckMVar t (fun t => Meta.isExprDefEqAux t s) <|
    unstuckMVar s (fun s => Meta.isExprDefEqAux t s) <|
    tryUnificationHints t s <||> tryUnificationHints s t

From this I conclude that the second call to tryUnificationHints throws an error.

We have

def tryUnificationHints (t s : Expr) : MetaM Bool := do
  trace[Meta.isDefEq.hint] "{t} =?= {s}"
  unless (← read).config.unificationHints do
    return false
  if t.isMVar then
    return false
  let hints := unificationHintExtension.getState (← getEnv)
  let candidates ← hints.discrTree.getMatch t UnificationHints.config
  for candidate in candidates do
    if (← tryCandidate candidate) then
      return true
  return false
where
  tryCandidate candidate : MetaM Bool :=
    withTraceNode `Meta.isDefEq.hint
      (return m!"{exceptBoolEmoji ·} hint {candidate} at {t} =?= {s}") do
    ...

from the trace I conclude that tryCandidate is not called. The only function I see that could give an error is hints.discrTree.getMatch.

[Jovan Gerbscheid]

The tryCatch block that I was talking about earlier only catches the very specific error throwIsDefEqStuck. It just so happens to be that DiscrTree.getMatch is able to throw this error :)

[Kevin Buzzard]

Indeed I see this in the trace:

[stuckMVar] found stuck MVar ?m.7891 : DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

[Jovan Gerbscheid]

I don't know whether that is related or not

[Jovan Gerbscheid]

The expression being looked up the the DiscrTree during tryUnificationHints is this:

Decidable.rec
(fun h ↦
  (fun x ↦
      ↑(Multiplicative.ofAdd
          (-↑((Associates.mk
                    ?m.8602.asIdeal).count
                (Associates.mk
                    (Ideal.span
                      {((IsLocalization.toLocalizationMap
                                (nonZeroDivisors
                                  (IsDedekindDomain.HeightOneSpectrum.adicCompletion
                                    K v))
                                K).sec
                            z).1})).factors))))
    h)
(fun h ↦ (fun x ↦ 0) h)
(Classical.propDecidable
  (((IsLocalization.toLocalizationMap
            (nonZeroDivisors
              (IsDedekindDomain.HeightOneSpectrum.adicCompletion
                K v))
            K).sec
        z).1 =
    0))

And in the code for DiscrTree lookup, we have

  | .const c _     =>
    if (← getConfig).isDefEqStuckEx && e.hasExprMVar then
      if (← isRec c) then
        Meta.throwIsDefEqStuck

[Jovan Gerbscheid]

So that is what triggers the error

[Jovan Gerbscheid]

Note that recursors are unfolded if possible before lookup, so the fact that the recursor is still there means that it can't be unfolded due to metavariables.

[Jovan Gerbscheid]

Now I don't know what the correct fix for this bug is: do we put more catchInternalId isDefEqStuckExceptionId inside of type class synthesis, or do we put this in tryUnificationHints?

[Kevin Buzzard]

I think that this needs to move to #lean4 now -- would you like to open a thread there asking for advice? You can explain what's going on far more coherently than me. I think I'll just work around this by adding an instance and press on.

[Jovan Gerbscheid]

Update: I tried turning off unification hints, which gets rid of the bug. But then we get a deterministic time-out.

import Mathlib.RingTheory.DedekindDomain.Ideal
import Mathlib.RingTheory.Valuation.ExtendToLocalization
import Mathlib.Topology.Algebra.ValuedField
import Mathlib.Algebra.Order.Group.TypeTags

open scoped Classical DiscreteValuation

open IsDedekindDomain

variable {R : Type*} [CommRing R] [IsDedekindDomain R] {K : Type*} [Field K]
  [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R)

namespace IsDedekindDomain.HeightOneSpectrum

def intValuation {R : Type*} [CommRing R] [IsDedekindDomain R]
  (v : HeightOneSpectrum R) : Valuation R ℤₘ₀ where
  toFun r := if r = 0 then 0 else 0 -- just 0 doesn't work
  map_zero' := sorry
  map_one' := sorry
  map_mul' := sorry
  map_add_le_max' := sorry

-- this uses loads of algebra
noncomputable def valuation {R : Type*} [CommRing R] [IsDedekindDomain R] {K : Type*}
    [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Valuation K ℤₘ₀ :=
  v.intValuation.extendToLocalization
    (sorry : nonZeroDivisors R ≤ v.intValuation.supp.primeCompl) K

variable (K)

-- this uses loads of topology
abbrev adicCompletion :=
  @UniformSpace.Completion K (Valued.mk' v.valuation).toUniformSpace

#synth Algebra (adicCompletion K v) (adicCompletion K v) -- works

instance AdicCompletion.algebra' {R : Type u_1} [CommRing R] [IsDedekindDomain R] [DecidableEq R]
    (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
  Algebra R (v.adicCompletion K) := sorry

-- set_option trace.Meta.synthInstance true
-- set_option trace.Meta.isDefEq true
open Lean Meta Elab Command

syntax (name := ha) "#mysynth" term : command
@[command_elab ha] def elabSynth : CommandElab := fun stx => do
  let term := stx[1]
  withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_synth_cmd do
    withConfig ({· with unificationHints := false}) do
    let inst ← Term.elabTerm term none
    Term.synthesizeSyntheticMVarsNoPostponing
    let inst ← instantiateMVars inst
    let val  ← synthInstance inst
    logInfo val
    pure ()

#mysynth Algebra (adicCompletion K v) (adicCompletion K v) -- fails

[Kevin Buzzard]

My instinct is that you'll get more relevant eyes on this stuff if you open a new thread in #lean4 .

[Michael Stoll]

Kevin Buzzard said:

I think I'll just work around this by adding an instance and press on.

Alternatively, I assume that

attribute [local instance 1100] Algebra.id

would also make it use the instance that is successful.

[Michael Stoll]

BTW, Algebra.id has default priority 1000, but it is the very first Algebra instance defined, so it is tried last among the default priority instances.

[Kevin Buzzard]

And probably a great one to have higher priority because it's likely to fail quickly when it doesn't apply

[Michael Stoll]

I'm just now trying to see what the effect is: #13032

[Michael Stoll]

build instructions: -113.839 * 10⁹ (-0.1%)
I had to set the priority back to default in two places, where proofs broke.

[Jovan Gerbscheid]

Note that it is not true that instances with the same priority are always first-in-last-out. This is only true for instances that get stored under the same index in the DiscrTree. Which index is retrieved first is a DiscrTree implementation detail. But the implementation is such that star-patterns end up being tried last (which I think is a good thing), and Algebra.id has a star pattern for all its arguments, so that is why it gets tried last.

[Michael Stoll]

Kevin has fixed the breakages without the need to restore default instance priority, and the effect is a net positive (if small compared to the total build). I'll add the "awaiting review" label to #13032; let's see if there are further comments...

[Henrik Böving]

Michael Stoll said:

build instructions: -113.839 * 10⁹ (-0.1%)
I had to set the priority back to default in two places, where proofs broke.

Came here from Jovan's latest PR. Just to make sure: You are aware of the fact that build instructions are not at all deterministic for Lean and changes at this magnitude can also simply amount to noise yes? Lean's implementation contains a couple of things that do not have deterministic behavior in terms of instruction count at all so elaborating a Lean file twice does not have to yield the same instruction count.

[Kevin Buzzard]

Which things don't have deterministic behaviour, out of interest? I've seen count_heartbeats give different answers on the same declaration before and never understood why.

[Michael Stoll]

And can you be more precise as to the (expected) relative size of the noise? That would be helpful in interpreting the !bench results.

[Henrik Böving]

Kevin Buzzard said:

Which things don't have deterministic behaviour, out of interest? I've seen count_heartbeats give different answers on the same declaration before and never understood why.

I'm not aware of all things that produce non deterministic behavior but I know one for sure. Some of the core routines that operate on Expr do build caches based on pointers modulo cache size. For example forEachExprWhere has this implementation for its cache.

abbrev cacheSize : USize := 8192 - 1

structure State where
  /--
  Implements caching trick similar to the one used at `FindExpr` and `ReplaceExpr`.
  -/
  visited : Array Expr   -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr
  /--
  Set of visited subterms that satisfy the predicate `p`.
  We have to use this set to make sure `f` is applied at most once of each subterm that satisfies `p`.
  -/
  checked : HashSet Expr

unsafe def initCache : State := {
  visited := mkArray cacheSize.toNat (cast lcProof ())
  checked := {}
}

abbrev ForEachM {ω : Type} (m : Type → Type) [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] := StateRefT' ω State m

unsafe def visited (e : Expr) : ForEachM m Bool := do
  let s ← get
  let h := ptrAddrUnsafe e
  let i := h % cacheSize
  let k := s.visited.uget i lcProof
  if ptrAddrUnsafe k == h then
    return true
  else
    modify fun s => { s with visited := s.visited.uset i e lcProof }
    return false

Now what can happen is that because all modern operating systems use ASLR and similar mechanisms to randomize addresses it might be that an Expr that was previously cached just happens to get evicted from the cache earlier on the next run and you end up doing different computation. A similar mechanism is used in Expr.replace, potentially causing a result to be cached in one run but by coincidence not in another run.

There are probably more things but this is at least a witness for the existence of non determinism.

Michael Stoll said:

And can you be more precise as to the (expected) relative size of the noise? That would be helpful in interpreting the !bench results.

I think the best way to figure that out for mathlib would be to simply rerun a !bench twice (or more) on the same commit and see how much your values are varying? All numbers I'm aware of are specific to the Lean compiler repository though there it is usually in the .x percent or lower. Other "almost deterministic" metrics like branch-misses do tend to vary low single digit percentages for example.

[Kim Morrison]

Definitely ignore anything under 0.5% variation in instruction count, and be skeptical of anything under 1%. Above 1% you're allowed to bring out the :tada: right away. :-)

[Kim Morrison]

file#CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit has previously been identified as an example of a particularly nondeterministic file.

[Kim Morrison]

It has been on my TODO list for too long to try to identify exactly what part of this file is so variable.

[Kim Morrison]

If anyone would like to help out there that would be extremely helpful.

[Kim Morrison]

We would really like to reduce this nondeterminism, because of course it makes optimisation hard. But we need better examples still for this.

[Kim Morrison]

Note that Mathlib now has count_heartbeats! in tac which will run tac 10 times and report the variation.

[Kim Morrison]

I hope this is useful for understanding examples like this file (which it was written for, but then I haven't got back to).