trace.profiler.output

Stream: lean4

[Patrick Massot]

I am also trying the new profiling stuff. I’m testing on https://github.com/leanprover-community/mathlib4/blob/incr-tactic-fixes-toolchain/Mathlib/Topology/Baire/LocallyCompactRegular.lean because this file has only one declaration and it is a bit slow (but not awful). So I got
out.json and I can open it in Firefox. Could you help me interpret it? What is this trying to tell me?

[Sebastian Ullrich]

First thing, you can upload it on the top right to share it with others :)

[Notification Bot]

2 messages were moved here from #lean4 > Incrementality Call for Testing by Sebastian Ullrich.

[Patrick Massot]

https://share.firefox.dev/3WU73P5

[Patrick Massot]

I think this is what you mean, right?

[Sebastian Ullrich]

Well, you definitely have some hairy unification problems in there! Just from hovering over the timeline you can see that almost all non-import time is spent in isDefEq. The one that is auto-selected is already 732ms long.

[Patrick Massot]

I also tried the new diagnostic trace and got:

[reduction] unfolded declarations (max: 101424, num: 17): ▼
  Nat.rec ↦ 101424
  Add.add ↦ 46937
  HAdd.hAdd ↦ 46937
  Nat.add ↦ 32191
  OfNat.ofNat ↦ 11060
  SetLike.coe ↦ 8158
  Set ↦ 7470
  Membership.mem ↦ 1560
  Set.Mem ↦ 1546
  LE.le ↦ 1437
  Subset ↦ 1423
  Set.Subset ↦ 1396
  setOf ↦ 762
  closure ↦ 90
  sInf ↦ 90
  sInter ↦ 90
  Set.Nonempty ↦ 22
[reduction] unfolded instances (max: 8158, num: 8): ▼
  PositiveCompacts.instSetLike ↦ 8158
  instAddNat ↦ 7374
  instHAdd ↦ 7374
  instOfNatNat ↦ 5531
  instMembership ↦ 1546
  instLE ↦ 1417
  instHasSubset ↦ 1407
  instInfSet ↦ 90
[reduction] unfolded reducible declarations (max: 46136, num: 4): ▼
  PositiveCompacts.toCompacts ↦ 46136
  Nat.casesOn ↦ 32191
  Compacts.carrier ↦ 8158
  outParam ↦ 96
[def_eq] heuristic for solving `f a =?= f b` (max: 8148, num: 13): ▼
  PositiveCompacts.toCompacts ↦ 8148
  SetLike.coe ↦ 4077
  Compacts.carrier ↦ 4074
  Membership.mem ↦ 766
  Set.Mem ↦ 763
  Subset ↦ 692
  Set.Subset ↦ 684
  LE.le ↦ 680
  setOf ↦ 378
  Set ↦ 66
  closure ↦ 51
  sInf ↦ 42
  sInter ↦ 42

but I’m not sure what is meant to be alarming (because I don’t have anything to compare to).

[Patrick Massot]

I the firefox thing knowing what defEq took that long?

[Matthew Ballard]

Those unfolded declarations are in almost every diagnostic trace I've seen so far

[Matthew Ballard]

Actually not the Nat.rec

[Matthew Ballard]

The Set stuff

[Matthew Ballard]

101424 incidents is also a new record from what I've seen

[Patrick Massot]

The thing that seem specific to this proof is all the PositiveCompacts stuff.

[Sebastian Ullrich]

There is a trace.profiler.output.pp option that didn't fit on the slide; if you set it to true, the profile will include not only when isDefEq is used but also on what problem. Which may or may not be more helpful, I haven't experimented with it very much yet.

[Matthew Ballard]

The add stuff is data and therefore concerning

[Patrick Massot]

Sebastian, for later readers, could you edit your message to trace.profiler.output.pp? You swapped two words.

[Patrick Massot]

New link: https://share.firefox.dev/4dydQnk

[Patrick Massot]

Optimization trick: including more to the profile cuts the defEq time in half :man_shrugging:

[Sebastian Ullrich]

Oh, the fact that they're all failing (presumably with all succeeding ones being below trace.profiler.threshold) already seems like new valuable information

[Sebastian Ullrich]

Patrick Massot said:

Optimization trick: including more to the profile cuts the defEq time in half :man_shrugging:

The previous profile merged the two defEq times as they had the same label and tree position

[Patrick Massot]

I would be nice to include line numbers in those profiles.

[Matthew Ballard]

refine ⟨Nat.rec K₀ K_next, fun n ↦ ?_, fun n ↦ (hK_next n _).trans (inter_subset_left _ _), hK₀⟩
    exact subset_closure.trans <| (hK_next _ _).trans <|
      (inter_subset_right _ _).trans interior_subset

3 seconds of the total is here

[Patrick Massot]

Yes, I know

[Patrick Massot]

But it would have been nice to have direct access to this information.

[Matthew Ballard]

Right, is that clear from the output here?

[Sebastian Ullrich]

You can see the refine node in the unfolded path. But I don't think I intended to print the raw syntax like that, not very readable :thinking:

[Patrick Massot]

Matthew Ballard said:

Right, is that clear from the output here?

No, that’s why I asked for line numbers in the profiler output.

[Patrick Massot]

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₀⟩

[Patrick Massot]

So I’m replacing the existential witness from Nat.rec K₀ K_next to K where K is a let.

[Patrick Massot]

And in this let lean needs to be provided the type.

[Patrick Massot]

Despite the fact that the local context has

K₀ : PositiveCompacts X
K_next : ℕ → PositiveCompacts X → PositiveCompacts X

[Patrick Massot]

Note that using let seems necessary, putting a type ascription is not enough.

[Matthew Ballard]

Is that blocking the unfolding somehow?

[Patrick Massot]

I guess so.

[Matthew Ballard]

It works even if I replace K with __K

[Patrick Massot]

What does it mean?

[Patrick Massot]

What are those underscore meant to mean?

[Matthew Ballard]

Implementation detail and gets unfolded more eagerly

[Matthew Ballard]

This seems like #mathlib4 > exposed data where if you inline a data field too much, Lean will happily try to unfold it

[Patrick Massot]

Should we work on a minimization or is this already tracked?

[Patrick Massot]

@Sebastian Ullrich do you want us to open issues about suggestions from this discussion?

[Matthew Ballard]

I don't think its tracked

[Patrick Massot]

Of course the most naive minimization fails (I mean it works without any delay).

[Patrick Massot]

I give up. It is really delicate. I was able to minimize it with mocking down to:

theorem BaireSpace.extracted_1 {X : Type} [TopologicalSpace X]
   (f : ℕ → Set X)  (K₀ : PositiveCompacts X)
  (K_next : ℕ → PositiveCompacts X → PositiveCompacts X)
  (hK_next : ∀ (n : ℕ) (K : PositiveCompacts X), closure (K_next n K) ⊆ f n ) :
  ∃ K : ℕ → PositiveCompacts X,  (∀ (n : ℕ), closure ↑(K (n + 1)) ⊆ f n)  := by
  exact ⟨Nat.rec K₀ K_next, fun n ↦ hK_next n _⟩

but simplifying further dissolves the bug. For instance removing both occurrences of closure (and adding an up arrow to help Lean understand the assumption) fixes the bug.

[Patrick Massot]

Then I tried to build a mathlib-free mockup but failed. My attempt is

class Topo (α : Type)
axiom PC (α : Type) [Topo α] : Type
def set (α : Type) := α → Prop

@[instance]
axiom PCcoe {α : Type} [Topo α] : CoeTC (PC α) (set α)

axiom Closure {α : Type} [Topo α] : set α → set α

@[instance]
axiom fooh (α : Type) : HasSubset (set α)

theorem BaireSpace.extracted_2 {X : Type} [Topo X]
   (f : ℕ → Set X)  (K₀ : PC X)
  (K_next : ℕ → PC X → PC X)
  (hK_next : ∀ (n : ℕ) (K : PC X), Closure (K_next n K) ⊆ f n ) :
  ∃ K : ℕ → PC X,  (∀ (n : ℕ), Closure ↑(K (n + 1)) ⊆ f n)  := by
  exact ⟨Nat.rec K₀ K_next, fun n ↦ hK_next n _⟩

but it does not have the bug.

[Patrick Massot]

I understand that having axiom does not encourage Lean to unfold stuff, but I don’t know how to minimize without them.