lean4#2644

Stream: lean4

[Matthew Ballard]

Naive question: the improvements we see result from

• less work trying to use the cached results with transparency := default or
• more in the cache or
• something else?

[Matthew Ballard]

Comments on getting to a working mathlib:

• breakage often seemed to occur where there was already some breakage. For example, we might have had an erw [xyz] in the file and we have to change a rw [xyz] to a erw [xyz] somewhere else
• it seemed the files that improved the most suffered from "timeout by 1000 cuts". Lean had to do repeated defeq checks that were not slow themselves but were too much when aggregated.
• I don't remember breakage that wasn't at the heart a transparency change
• there is a lot of breakage overall and it will probably take significant effort to get mathlib right with these changes

[Matthew Ballard]

Do we trace the the defeq caches at all? trace.Meta.isDefEq.cache :face_palm:

[Matthew Ballard]

All toolchains have

[Meta.isDefEq.cache] cache true for Option α =?= WithTop α

for Scott's example. The only difference is that lean4#2644 also has

[Meta.isDefEq.cache] cache false for Option α =?= WithTop α

I guess the tracing has not been refined by transparency?

[Sebastian Ullrich]

Yes, this is where we would previously get a false positive in the cache

[Sebastian Ullrich]

Matthew Ballard said:

Naive question: the improvements we see result from

• less work trying to use the cached results with transparency := default or
• more in the cache or
• something else?

Fewer cache resets, so more cache hits (but also fewer false positive cache hits as just mentioned)

[Matthew Ballard]

Can I see what is generating that false positive? From which problem it arose?

[Sebastian Ullrich]

How would it do that? The old code doesn't know that it is doing something wrong, and the new code doesn't know what the old code would have done. Your trace above looks like the best approach.

[Matthew Ballard]

Sorry, I mean tracing the context on each cache addition.

[Sebastian Ullrich]

I think you mean trace.Meta.isDefEq?

[Matthew Ballard]

I didn't see a hit for Option =?= WithTop with that anywhere. I'll look again

[Matthew Ballard]

:face_palm: It was in the snippet I copied into the PR comment

[Matthew Ballard]

[] ✅ α ↪ Option α =?= α ↪ WithTop α ▼
    [] ✅ α =?= α
    [] ✅ Option α =?= WithTop α ▼
      [] ✅ Option α =?= Option α

[Matthew Ballard]

Thanks for your indulgence. Next question: can I trace the transparency setting in addition?

[Matthew Ballard]

Or here: why is transparency := .default here?

[Sebastian Ullrich]

That's not a lot of context but most likely because we always compare implicit parameters at at least default

[Matthew Ballard]

Thanks. That is helpful. I will squint at Scott's example

[Matthew Ballard]

Ok. Yes, then it seems to come from unifying using the FunLike instance. This didn't change the behavior

instance {α : Sort u} {β : Sort v} : FunLike (α ↪ β) α fun _ => β where
  coe := Embedding.toFun

[Matthew Ballard]

This seems problematic

instance coeTC : CoeTC α (WithTop α) := ⟨Option.some⟩

[Matthew Ballard]

With

def WithTop (α : Type _) := Option α

[Matthew Ballard]

Adding

protected def some {α} : α → WithTop α := Option.some

protected def Embedding.some {α} : α ↪ WithTop α := ⟨WithTop.some⟩

and changing to

instance coeTC : CoeTC α (WithTop α) := ⟨WithTop.some⟩

gets coeFn_mk to fire in simp at the expense of mem_map needing a rw instead of being applied in simp

theorem mem_map {f : α ↪ β} {s : Finset α} {b : β} : b ∈ s.map f ↔ ∃ a, a ∈ s ∧ f a = b := sorry

[Matthew Ballard]

This also probably explains why there was so much breakage in CategoryTheory.Limits and friends since similar things happen to define the indexing categories.

[Eric Wieser]

I think I made a similar comment in @Scott Morrison's other thread, that we needed a WithTop version of Embedding.some

[Matthew Ballard]

Do you know why simp only [mem_map] fails but rw [mem_map] succeeds here?