tracing [assign]

Stream: lean4

[Kevin Buzzard]

A mathlib PR is weirdly slow. I tried

set_option trace.profiler true in
set_option trace.Meta.synthInstance true in
instance <some maths here>

and the relevant part of the trace is

  [Meta.isDefEq] [8.220413] ✅ Finite (⋯.choose.presentation i).generators.I ∧
      Finite (⋯.choose.presentation i).relations.I =?= ?m.35403 ∧ ?m.35404 ▼
  [] [0.047275] ✅ Finite (⋯.choose.presentation i).generators.I =?= ?m.35403 ▶
  [] [8.173041] ✅ Finite (⋯.choose.presentation i).relations.I =?= ?m.35404 ▼
  [assign] [8.173030] ✅ ?m.35404 := Finite (⋯.choose.presentation i).relations.I

Can I get more information from Lean about why [assign] is taking 8 seconds?

[Matthew Ballard]

set_option diagnostics true and look for terrifying behavior?

[Kevin Buzzard]

No change in output :-(

[Matthew Ballard]

It’s not giving the diagnostic output?

[Kevin Buzzard]

FWIW, it's #13464 , lines 100 to 107 of Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean ,

[Kevin Buzzard]

Screenshot-from-2024-06-26-21-56-17.png

I have two blue underlines. Which one do I click on?

[Kevin Buzzard]

Oh, maybe the extra information is this

[reduction] unfolded reducible declarations (max: 104, num: 6): ▼
  HasWeakSheafify ↦ 104
  QuasicoherentData.presentation ↦ 48
  QuasicoherentData.I ↦ 36
  Exists.choose ↦ 29
  RingCat ↦ 27
  Presentation.generators ↦ 24
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters

but I have no feeling about those numbers

[Matthew Ballard]

What about the unfolded ones that aren’t reducible? That should be before it.

[Matthew Ballard]

Those reducible numbers are pretty mild.

[Kevin Buzzard]

  have h2 : ∃ σ, _ := h.exists_quasicoherentData -- fast up until here
  have h3 := Exists.choose_spec h2 -- 23 seconds?!

[Ruben Van de Velde]

What happens if you specify the type of h3?

[Kevin Buzzard]

I've not used set_option diagnostics before but the only thing I can get it to report on is that [reduction] thing. I now have this:

  [assign] [55.644552] ✅ ?m.35401 := ∀ (i : h2.choose.I),
      Finite (h2.choose.presentation i).generators.I ∧ Finite (h2.choose.presentation i).relations.I

with no understanding of how to figure out what's happening in those 55 seconds (no triangle to unfold). The PR is on the point of being merged and after that I'll have an example which uses only mathlib master.

[Kim Morrison]

@Kevin Buzzard, I pushed a fix.

[Matthew Ballard]

@Kim Morrison did you identify what computation you are blocking with fix?

[Kevin Buzzard]

Kim Morrison said:

Kevin Buzzard, I pushed a fix.

Wooah, what the heck is going on there? :-)

[Matthew Ballard]

My guess: it is the same issue as

Patrick Massot said:

For the record, one way to turn the problematic line quoted by Matthew into instant happiness is to replace it with

    let K : ℕ → PositiveCompacts X := Nat.rec K₀ K_next
    refine ⟨K, fun n ↦ ?_, fun n ↦ (hK_next n _).trans (inter_subset_left _ _), hK₀⟩

[Kim Morrison]

Matthew Ballard said:

Kim Morrison did you identify what computation you are blocking with fix?

Not sure still.

What I observed was that if you try:

set_option pp.proofs true in
instance (i : M.quasicoherentDataOfIsFinitePresentation.I) :
    Finite (M.quasicoherentDataOfIsFinitePresentation.presentation i).generators.I := by
  unfold quasicoherentDataOfIsFinitePresentation at *
  obtain ⟨x, y⟩ := h.exists_quasicoherentData

then you reach the goal:

h : M.IsFinitePresentation
i : IsFinitePresentation.exists_quasicoherentData.choose.I
x : M.QuasicoherentData
y : ∀ (i : x.I), Finite (x.presentation i).generators.I ∧ Finite (x.presentation i).relations.I
⊢ Finite ((Exists.intro x y).choose.presentation i).generators.I

but by this point we have lost track of the fact that x := IsFinitePresentation.exists_quasicoherentData.choose, so we can't specialize y at i, and I couldn't work out anything to replace the obtain with that would simultaneously modify i.

But I'm still not exactly sure why this observation led to what I pushed. :-) Wanting to avoid have choose in multiple places, I guess.