trace debugging

Stream: general

[Kevin Buzzard]

Right now I'm looking at some trace.profiler output in quite a large block of code, and it doesn't add up. I'd like to investigate further. Right now it looks like this in the infoview when I unfold the unique output of the trace profiler:

[Elab.command] [3.682466s] /--
    The Hales-Jewett theorem. This version has a restriction on universe levels which is necessary
    for the proof. See `exists_mono_in_high_dimension` for a fully universe-polymorphic version. -/
   **100 lines omitted* ▼
  [Elab.step] [0.010713s] expected type: ∀ (α : Type u) [inst : Finite α] (κ : Type (max v u))...
  **pretty much same 100 lines omitted ▶
  [Elab.step] [0.382477s]
   ** etc** ▶
  [Kernel] [0.024552s] typechecking declaration

It was stupidly annoying having to check that the smaller numbers didn't add up to the bigger numbers (and I did it all by manual text editor in emacs, I could easily have got it wrong). Is there a way I can just view the top few nodes on the skeleton in a small number of lines as I start changing the proof, in order to further debug?

[Sebastian Ullrich]

By "top" you mean the slowest ones? If it doesn't add up, we simply may be missing a trace node for a task. Could you check the plain profiler on the declaration as well?

[Henrik Böving]

You can still use https://github.com/hargoniX/Flame to get a nice overview as well^^

[Anne Baanen]

BTW: I also ran into this question here.

[Tomas Skrivan]

Henrik Böving said:

You can still use https://github.com/hargoniX/Flame to get a nice overview as well^^

I wrote a command #profile_this_file that automatically compiles the current file with profiler and launches speedscope. I use it all the time.

https://github.com/lecopivo/SciLean/blob/master/SciLean/Profile.lean

Just on th6e line 5 change the location of flame on your system.

[Kevin Buzzard]

I have output from Flame in "collapsed stack format" here

out.txt

but have no idea what to do with it. I looked at it using an online viewer -- is it something to do with the unused variables linter? I don't even know what I'm looking at.

[Kevin Buzzard]

Aah, set_option pp.oneline true was what I was looking for earlier I think:

[Elab.command] [3.126436s] /-- The Hales-Jewett theorem. This version has a restriction on universe levels which is necessary [...] ▼
  [step] [0.011979s] expected type: ∀ (α : Type u) [inst : Finite α] (κ : Type (max v u)) [inst : Finite κ], [...], term
      Finite.induction_empty_option [...] ▶
  [step] [0.331203s] intro α _ ihα κ _ [...] ▶
  [Kernel] [0.018651s] typechecking declaration

My issue is that 0.01+0.33+0.01 is not 3.12.

[Wojciech Nawrocki]

The subtraces do not cover the parent trace, i.e. there might be more calls beyond step/step/Kernel made during the [Elab.command] step which are not traced. We only get an inequality. It would be worrying if the inequality didn't hold though!

[Kevin Buzzard]

My question is why the HalesJewett file in mathlib is slow. How should I proceed?

[Matthew Ballard]

Comment it halfway and add a sorry. See if there is a significant change. If not cut that in half. If so add in half of what was left out.

[Kevin Buzzard]

I have been trying to do that for literally hours. It's really hard. extract_goal needs some work.

[Kevin Buzzard]

I don't understand the mathematics at all, this is one of the issues.

[Kevin Buzzard]

The profiler says

tactic execution of Lean.Parser.Tactic.rewriteSeq took 124ms
linting took 2.74s
elaboration took 3.07s

So it is the unused variables linter?

[Matthew Ballard]

If I sorry any of the goals from the last refine, it is pretty snappy. There must be somethings being postponed and unified at the completion of the proof.

[Kevin Buzzard]

Beyond some point

    refine' Or.inl ⟨⟨(s.lines.map _).cons ⟨(l'.map some).vertical s.focus, C' s.focus, fun x => _⟩,
            Sum.elim s.focus (l'.map some none), _, _⟩, _⟩

stopped working for me

[Kevin Buzzard]

there was some unification issue which I couldn't resolve

[Anne Baanen]

There are some benchmark results in this file that I would like to understand better: between the merges of #6256 and #5998 VelCom reports an increase from 44M to 58M instructions, then between #6395 and #6441 it goes down to 48M instructions. I can't figure out what would cause either change: in the first range I don't see a commit that would obviously affect the build times, while in the second range we have #6145 which reports a benchmark increase.

[Anne Baanen]

@Sebastian Ullrich, would you be willing to prioritize benchmarking 1accb5fb?

[Sebastian Ullrich]

Done

[Anne Baanen]

Thank you!

[Sebastian Ullrich]

The instructions counts have been very reliable so far, if they cease to do that, that would be worrying. I think the next step there would be for someone to reproduce those timings on their own machine (requires Linux perf stat)

[Sebastian Ullrich]

I can also rerun the commit with the unexpected rise but of course that's two more hours of queueing

[Anne Baanen]

My hypothesis is that the instruction counts are accurate (they seem to be reliable across commits that don't affect the imported files, at least) and we just don't know what subtle thing causes them to go up and down so much.

[Anne Baanen]

Here's my latest attempt at splitting up the slow proof. Splitting key off made the whole thing go from 9s to 7s + 0.2s. Splitting off refine as well made it go to 2s + 0.2s + 0.2s. This is similar to, but less dramatic than, what I saw with ClassGroup, where the speedup seemed to be in hiding a big expression behind a def so it wouldn't get unfolded in the rest of the proof. Maybe something similar is going on here?

set_option trace.profiler true

-- ~2s
theorem exists_mono_in_high_dimension'.refine {α : Type u} (κ : Type (max v u))
    [Nonempty α] (r : ℕ) (ι ι' : Type) (C : (ι ⊕ ι' → Option α) → κ) (l' : Line α ι') (C' : (ι → Option α) → κ)
    (hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) ((fun x i ↦ Option.getD (idxFun l' i) x) x) = C')
    (s : ColorFocused C') (sr : Multiset.card s.lines = r)
    (h : ¬∃ p, p ∈ s.lines ∧ p.color = C' s.focus) : (∃ (s : ColorFocused C), Multiset.card s.lines = Nat.succ r) ∨ ∃ l, IsMono C l := by
  refine' Or.inl ⟨⟨(s.lines.map _).cons ⟨(l'.map some).vertical s.focus, C' s.focus, fun x => _⟩,
          Sum.elim s.focus (l'.map some none), _, _⟩, _⟩
  -- Porting note: Needed to reorder the following two goals
  -- The product lines are almost monochromatic.
  · refine' fun p => ⟨p.line.prod (l'.map some), p.color, fun x => _⟩
    rw [Line.prod_apply, Line.map_apply, ← p.has_color, ← congr_fun (hl' x)]
  -- The vertical line is almost monochromatic.
  · rw [vertical_apply, ← congr_fun (hl' x), Line.map_apply]
  -- Our `r+1` lines have the same endpoint.
  · simp_rw [Multiset.mem_cons, Multiset.mem_map]
    rintro _ (rfl | ⟨q, hq, rfl⟩)
    · simp only [vertical_apply]
    · simp only [prod_apply, s.is_focused q hq]
  -- Our `r+1` lines have distinct colors (this is why we needed to split into cases above).
  · rw [Multiset.map_cons, Multiset.map_map, Multiset.nodup_cons, Multiset.mem_map]
    exact ⟨fun ⟨q, hq, he⟩ => h ⟨q, hq, he⟩, s.distinct_colors⟩
  -- Finally, we really do have `r+1` lines!
  · rw [Multiset.card_cons, Multiset.card_map, sr]

-- ~ 0.2s
theorem exists_mono_in_high_dimension'.key {α : Type u} [Fintype α]
    (ihα : ∀ (κ : Type (max v u)) [Finite κ],
      ∃ (ι : Type) (_x : Fintype ι), ∀ (C : (ι → α) → κ), ∃ l, IsMono C l) (κ : Type (max v u))
    [inst : Fintype κ] (h : Nonempty α) (r : ℕ) :
    ∃ (ι : Type) (_x : Fintype ι),
      ∀ (C : (ι → Option α) → κ), (∃ (s : ColorFocused C), Multiset.card s.lines = r) ∨ ∃ l, IsMono C l := by
  induction' r with r ihr
  -- The base case `r = 0` is trivial as the empty collection is color-focused.
  · exact ⟨PEmpty, inferInstance, fun C => Or.inl ⟨default, Multiset.card_zero⟩⟩
  -- Supposing the key claim holds for `r`, we need to show it for `r+1`. First pick a high
  -- enough dimension `ι` for `r`.
  obtain ⟨ι, _inst, hι⟩ := ihr
  -- Then since the theorem holds for `α` with any number of colors, pick a dimension `ι'` such
  -- that `ι' → α` always has a monochromatic line whenever it is `(ι → Option α) → κ`-colored.
  -- have : Finite ((ι → Option α) → κ) := Fintype.finite (@Pi.fintype _ _ _ _ _)
  specialize ihα ((ι → Option α) → κ)
  obtain ⟨ι', _inst, hι'⟩ := ihα
  -- We claim that `ι ⊕ ι'` works for `Option α` and `κ`-coloring.
  refine' ⟨Sum ι ι', inferInstance, _⟩
  intro C
  -- A `κ`-coloring of `ι ⊕ ι' → Option α` induces an `(ι → Option α) → κ`-coloring of `ι' → α`.
  specialize hι' fun v' v => C (Sum.elim v (some ∘ v'))
  -- By choice of `ι'` this coloring has a monochromatic line `l'` with color class `C'`, where
  -- `C'` is a `κ`-coloring of `ι → α`.
  obtain ⟨l', C', hl'⟩ := hι'
  -- If `C'` has a monochromatic line, then so does `C`. We use this in two places below.
  have mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l := by
    rintro ⟨l, c, hl⟩
    refine' ⟨l.horizontal (some ∘ l' (Classical.arbitrary α)), c, fun x => _⟩
    rw [Line.horizontal_apply, ← hl, ← hl']
  -- By choice of `ι`, `C'` either has `r` color-focused lines or a monochromatic line.
  specialize hι C'
  rcases hι with (⟨s, sr⟩ | h)
  on_goal 2 => exact Or.inr (mono_of_mono h)
  -- Here we assume `C'` has `r` color focused lines. We split into cases depending on whether
  -- one of these `r` lines has the same color as the focus point.
  by_cases h : ∃ p ∈ s.lines, (p : AlmostMono _).color = C' s.focus
  -- If so then this is a `C'`-monochromatic line and we are done.
  · obtain ⟨p, p_mem, hp⟩ := h
    refine' Or.inr (mono_of_mono ⟨p.line, p.color, _⟩)
    rintro (_ | _)
    rw [hp, s.is_focused p p_mem]
    apply p.has_color
  -- If not, we get `r+1` color focused lines by taking the product of the `r` lines with `l'`
  -- and adding to this the vertical line obtained by the focus point and `l`.
  exact Combinatorics.Line.exists_mono_in_high_dimension'.refine.{u, v} κ r ι ι' C l' C' hl' s sr h

-- ~ 0.2s
/-- The Hales-Jewett theorem. This version has a restriction on universe levels which is necessary
for the proof. See `exists_mono_in_high_dimension` for a fully universe-polymorphic version. -/
theorem exists_mono_in_high_dimension' :
    ∀ (α : Type u) [Finite α] (κ : Type max v u) [Finite κ],
      ∃ (ι : Type) (_ : Fintype ι), ∀ C : (ι → α) → κ, ∃ l : Line α ι, l.IsMono C :=
-- The proof proceeds by induction on `α`.
  Finite.induction_empty_option
  (-- We have to show that the theorem is invariant under `α ≃ α'` for the induction to work.
  fun {α α'} e =>
    forall_imp fun κ =>
      forall_imp fun _ =>
        Exists.imp fun ι =>
          Exists.imp fun _ h C =>
            let ⟨l, c, lc⟩ := h fun v => C (e ∘ v)
            ⟨l.map e, c, e.forall_congr_left.mp fun x => by rw [← lc x, Line.map_apply]⟩)
  (by
    -- This deals with the degenerate case where `α` is empty.
    intro κ _
    by_cases h : Nonempty κ
    · refine' ⟨Unit, inferInstance, fun C => ⟨default, Classical.arbitrary _, PEmpty.rec⟩⟩
    · exact ⟨Empty, inferInstance, fun C => (h ⟨C (Empty.rec)⟩).elim⟩)
  (by
    -- Now we have to show that the theorem holds for `Option α` if it holds for `α`.
    intro α _ ihα κ _
    cases nonempty_fintype κ
    -- Later we'll need `α` to be nonempty. So we first deal with the trivial case where `α` is
    -- empty.
    -- Then `Option α` has only one element, so any line is monochromatic.
    by_cases h : Nonempty α
    case neg =>
      refine' ⟨Unit, inferInstance, fun C => ⟨diagonal _ Unit, C fun _ => none, ?_⟩⟩
      rintro (_ | ⟨a⟩)
      · rfl
      · exact (h ⟨a⟩).elim
    -- The key idea is to show that for every `r`, in high dimension we can either find
    -- `r` color focused lines or a monochromatic line.
    suffices key :
      ∀ r : ℕ,
        ∃ (ι : Type) (_ : Fintype ι),
          ∀ C : (ι → Option α) → κ,
            (∃ s : ColorFocused C, Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
    -- Given the key claim, we simply take `r = |κ| + 1`. We cannot have this many distinct colors
    -- so we must be in the second case, where there is a monochromatic line.
    · obtain ⟨ι, _inst, hι⟩ := key (Fintype.card κ + 1)
      refine' ⟨ι, _inst, fun C => (hι C).resolve_left _⟩
      rintro ⟨s, sr⟩
      apply Nat.not_succ_le_self (Fintype.card κ)
      rw [← Nat.add_one, ← sr, ← Multiset.card_map, ← Finset.card_mk]
      exact Finset.card_le_univ ⟨_, s.distinct_colors⟩
    exact exists_mono_in_high_dimension'.key.{u, v} (α := α) (κ := κ) @ihα h)

[Kevin Buzzard]

So you are saying that if you split up the argument then you can avoid the secret time hole. Here is my attempt to minimise the secret time hole:

import Mathlib.Combinatorics.HalesJewett

-- 44K heartbeats, 4.3 seconds
/-
    [] [4.407894s] theorem extracted_1 {α : Type} [Finite α] [...] ▼
      [step] [0.713942s] suffices key : [...] ▶
      [Kernel] [0.025385s] typechecking declaration
-/
count_heartbeats in
set_option trace.profiler true in
set_option profiler true in
set_option pp.oneline true in
theorem Combinatorics.Line.extracted_1
    {α : Type} [Finite α]
    (ihα : ∀ (κ : Type) [Finite κ], ∃ (ι : Type) (_ : Fintype ι),
      ∀ (C : (ι → α) → κ), ∃ l : Line α ι, l.IsMono C)
    (κ : Type) [Finite κ] (h : Nonempty α) :
     ∃ (ι : Type) (_ : Fintype ι), ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l := by
  suffices key :
    ∀ r : ℕ,
      ∃ (ι : Type) (_ : Fintype ι),
        ∀ C : (ι → Option α) → κ,
          (∃ s : ColorFocused C, Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
  -- Given the key claim, we simply take `r = |κ| + 1`. We cannot have this many distinct colors
  -- so we must be in the second case, where there is a monochromatic line.
  · classical
    let inst37 : Fintype κ := Fintype.ofFinite κ
    obtain ⟨ι, _inst, hι⟩ := key (Fintype.card κ + 1)
    refine' ⟨ι, _inst, fun C => (hι C).resolve_left _⟩
    rintro ⟨s, sr⟩
    apply Nat.not_succ_le_self (Fintype.card κ)
    rw [← Nat.add_one, ← sr, ← Multiset.card_map, ← Finset.card_mk]
    exact Finset.card_le_univ ⟨_, s.distinct_colors⟩
  -- We now prove the key claim, by induction on `r`.
  intro r
  induction' r with r ihr
  -- The base case `r = 0` is trivial as the empty collection is color-focused.
  · exact ⟨Empty, inferInstance, fun C => Or.inl ⟨default, Multiset.card_zero⟩⟩
  -- Supposing the key claim holds for `r`, we need to show it for `r+1`. First pick a high
  -- enough dimension `ι` for `r`.
  obtain ⟨ι, _inst, hι⟩ := ihr
  classical
  let iFα : Fintype α := Fintype.ofFinite α
  let iFκ : Fintype κ := Fintype.ofFinite κ
--    let moo : Fintype (ι → Option α) := Pi.fintype
--    let foo : Fintype ((ι → Option α) → κ) := Pi.fintype
  -- Then since the theorem holds for `α` with any number of colors, pick a dimension `ι'` such
  -- that `ι' → α` always has a monochromatic line whenever it is `(ι → Option α) → κ`-colored.
  specialize ihα ((ι → Option α) → κ)
  obtain ⟨ι', _inst, hι'⟩ := ihα
  -- We claim that `ι ⊕ ι'` works for `Option α` and `κ`-coloring.
  refine' ⟨Sum ι ι', inferInstance, _⟩
  intro C
  -- A `κ`-coloring of `ι ⊕ ι' → Option α` induces an `(ι → Option α) → κ`-coloring of `ι' → α`.
  specialize hι' fun v' v => C (Sum.elim v (some ∘ v'))
  -- By choice of `ι'` this coloring has a monochromatic line `l'` with color class `C'`, where
  -- `C'` is a `κ`-coloring of `ι → α`.
  obtain ⟨l', C', hl'⟩ := hι'
  -- If `C'` has a monochromatic line, then so does `C`. We use this in two places below.
  have mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l := by
    rintro ⟨l, c, hl⟩
    refine' ⟨l.horizontal (some ∘ l' (Classical.arbitrary α)), c, fun x => _⟩
    rw [Line.horizontal_apply, ← hl, ← hl']
  -- By choice of `ι`, `C'` either has `r` color-focused lines or a monochromatic line.
  specialize hι C'
  rcases hι with (⟨s, sr⟩ | h)
  on_goal 2 => exact Or.inr (mono_of_mono h)
  -- Here we assume `C'` has `r` color focused lines. We split into cases depending on whether
  -- one of these `r` lines has the same color as the focus point.
  by_cases h : ∃ p ∈ s.lines, (p : AlmostMono _).color = C' s.focus
  -- If so then this is a `C'`-monochromatic line and we are done.
  · obtain ⟨p, p_mem, hp⟩ := h
    refine' Or.inr (mono_of_mono ⟨p.line, p.color, _⟩)
    rintro (_ | _)
    rw [hp, s.is_focused p p_mem]
    apply p.has_color
  -- If not, we get `r+1` color focused lines by taking the product of the `r` lines with `l'`
  -- and adding to this the vertical line obtained by the focus point and `l`.
  refine' Or.inl ⟨⟨(s.lines.map _).cons ⟨(l'.map some).vertical s.focus, C' s.focus, fun x => _⟩,
          Sum.elim s.focus (l'.map some none), _, _⟩, _⟩
  -- Porting note: Needed to reorder the following two goals
  -- The product lines are almost monochromatic.
  · refine' fun p => ⟨p.line.prod (l'.map some), p.color, fun x => _⟩
    rw [Line.prod_apply, Line.map_apply, ← p.has_color, ← congr_fun (hl' x)]
  -- The vertical line is almost monochromatic.
  · rw [vertical_apply, ← congr_fun (hl' x), Line.map_apply]
  -- Our `r+1` lines have the same endpoint.
  · simp_rw [Multiset.mem_cons, Multiset.mem_map]
    rintro _ (rfl | ⟨q, hq, rfl⟩)
    · simp only [vertical_apply]
    · simp only [prod_apply, s.is_focused q hq]
  -- Our `r+1` lines have distinct colors (this is why we needed to split into cases above).
  · rw [Multiset.map_cons, Multiset.map_map, Multiset.nodup_cons, Multiset.mem_map]
    exact ⟨fun ⟨q, hq, he⟩ => h ⟨q, hq, he⟩, s.distinct_colors⟩
  -- Finally, we really do have `r+1` lines!
  · rw [Multiset.card_cons, Multiset.card_map, sr]

This proof goes: "suffices blah, <proof>, <proof>". If you replace either of the proofs with sorry then the secret time hole disappears. But with both sorrys filled you get this funny trace

    [] [4.407894s] theorem extracted_1 {α : Type} [Finite α] [...] ▼
      [step] [0.713942s] suffices key : [...] ▶
      [Kernel] [0.025385s] typechecking declaration

which doesn't add up.

[Anne Baanen]

Yep, that also matches my experience a couple weeks ago.

[Sebastian Ullrich]

That does point to the unused variables linter as it ignores decls with sorry. Does turning off linter.unusedVariables fix it then?

[Anne Baanen]

On both the current and modified version of the file, set_option linter.unusedVariables false does not actually seem to change the Elab.command time, although the Elab.lint time indeed goes from 3s to 0.2s.

[Sebastian Ullrich]

Uh, interesting?

[Sebastian Ullrich]

I'm kind of at a loss of words. Does the plain profiler output change?

[Anne Baanen]

Let me check... (By the way, the VelCom queue says "No worker registered :( I will not be able to benchmark anything! Please setup a runner and point it to this instance.", is that supposed to happen / a known issue?)

[Matthew Ballard]

Uh oh

[Anne Baanen]

With set_option profiler true:

▶ 219:1-219:1: information:
tactic execution of Lean.Parser.Tactic.rewriteSeq took 228ms
linting took 2.77s
elaboration took 7.75s

With set_option profiler true; set_option linter.unusedVariables false:

▶ 221:1-221:1: information:
tactic execution of Lean.Parser.Tactic.rewriteSeq took 219ms
elaboration took 7.97s

[Matthew Ballard]

This file gets almost 20% faster with #6370 if I remember correctly

[Matthew Ballard]

Maybe useful info

[Anne Baanen]

Good point! There is certainly some universe trickery inside these theorems so that sounds likely to have an impact.

[Kevin Buzzard]

In my "minimal" example above I have stripped out all the universes (for precisely this reason)

[Matthew Ballard]

Anne Baanen said:

Let me check... (By the way, the VelCom queue says "No worker registered :( I will not be able to benchmark anything! Please setup a runner and point it to this instance.", is that supposed to happen / a known issue?)

I know you can't do anything now but FYI @Sebastian Ullrich if you haven't seen it

[Sebastian Ullrich]

Nothing I can do about it right now, please bear with it a little while longer

[Matthew Ballard]

Of course.