Infoview lag

Stream: lean4

[Sky Wilshaw]

I've been experiencing some dramatic slowdowns in the infoview over the last week or so; the more goals and terms, the worse it gets. I'm on latest lean/mathlib and VSCode extension - is anyone else having this issue? I'm using Ubuntu 22.04. I think it's likely that this isn't actually a Lean issue, but probably something to do with how VSCode renders webviews.

[Marc Huisinga]

Could you downgrade your VS Code extension version to 0.0.136 and see if the issue persists? (Extensions > Cog icon on lean4 extension > Install another version > 0.0.136)

[Sky Wilshaw]

Wow, that completely fixed it. What's changed between those updates?

[Marc Huisinga]

What's an example for a Mathlib file + location where you experience lag that is especially bad?

[Marc Huisinga]

(I am suspecting vscode-lean4#408 as the likely culprit)

[Sky Wilshaw]

I don't use too much of mathlib so I can't give great examples - I'm looking around to find files with very large proof states.

[Sky Wilshaw]

For example, Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean.

[Marc Huisinga]

Thanks, I'll see if I can reproduce and fix the issue tomorrow.

[Sky Wilshaw]

I'm testing the lag out by attempting to scroll up and down in the infoview. On the latest version of the extension, it renders at ~5FPS.

[Sky Wilshaw]

Thanks!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Oh no, that was supposed to be an optimization! @Marc Huisinga if you find out do let me know what went wrong.

[Floris van Doorn]

Sometimes apply? gives me 360 suggestions (which I think is its cap) and that makes the infoview very slow. Here is a non-minimal example:

import Mathlib.Algebra.Periodic

open Function Set
variable {α β : Type _} {f : α → β}

theorem exists_nsmul_near_of_pos' [LinearOrderedAddCommMonoid α] [Archimedean α] [Sub α] [OrderedSub α]
  [ExistsAddOfLE α] [CovariantClass α α (· + ·) (· ≤ ·)] [ContravariantClass α α (· + ·) (· ≤ ·)]
    {a : α} (ha : 0 < a) (y : α) :
    ∃! (x : α), ∃ (k l : ℕ), x ∈ Ico 0 a ∧ x + k • a = y + l • a := by
  classical
  have ⟨k, hk⟩ := Archimedean.arch y ha
  have ⟨l, hl, h2l⟩ := Nat.findX <| Archimedean.arch (k • a - y) ha
  rw [tsub_le_iff_left] at hl
  simp_rw [tsub_le_iff_left] at h2l
  refine ⟨y + l • a - k • a, ⟨k, l, ⟨?_, ?_⟩, ?_⟩, ?_⟩
  · apply le_tsub_of_add_le_left; rwa [add_zero]
  · rw [tsub_lt_iff_left hl, ← not_le]
    nth_rw 2 [← one_smul ℕ a]
    rw [← add_smul]
    intro h
    cases' l with l
    · simp at *
      sorry
    · simp_rw [Nat.succ_eq_add_one] at *
      apply h2l l (lt_add_one l)
      apply?

[Marc Huisinga]

PR to fix this at vscode-lean4#432. The apply? example doesn't significantly slow down the InfoView anymore for me with this fix, either.

[Marc Huisinga]

The fix has been released as part of version 0.0.140 now. If you downgraded to 0.0.136 previously to work around this issue, make sure to click "Update" in the extensions menu to unpin 0.0.136.

[Sky Wilshaw]

It seems to be fixed on my end with that update, thanks!