Info view delay

Stream: lean4

[Kyle Miller]

Scott Morrison said:

This subjective feeling is mostly wrong. We've stopped running the comparison bot against mathlib3, but there was overall about a 1.8x wallclock speedup compiling mathlib4 vs mathlib3 (and a 3.3x speedup in CPU time).

The data shows Lean 4 is faster than Lean 3 for batch processing, but interactive processing could have very different numbers. I've noticed Lean 4 subjectively feeling less snappy compared to Lean 3, especially when I go back to Lean 3, where I get worried Lean must have crashed since some things update so quickly it feels like nothing's happened.

I'm pretty sure a lot of the feeling of sluggishness is the delay between editing and the LSP updating the info view. It doesn't update until the entire file has finished processing, unlike Lean 3 where it was once the current command finished.

When compiling mathlib, doesn't Lean 4 skip doing things like generating infotrees for the LSP? Has anyone measured the performance impact of things needed to support the editor?

[Scott Morrison]

Kyle Miller said:

I'm pretty sure a lot of the feeling of sluggishness is the delay between editing and the LSP updating the info view. It doesn't update until the entire file has finished processing, unlike Lean 3 where it was once the current command finished.

Oh, I hadn't even noticed this! That's not great.

[Kevin Buzzard]

I'm pretty sure a lot of the feeling of sluggishness is the delay between editing and the LSP updating the info view. It doesn't update until the entire file has finished processing, unlike Lean 3 where it was once the current command finished.

I find myself often writing #exit just below the code I'm working on precisely for this reason. @Yaël Dillies has also flagged this -- they said something like "I feel like Lean is hiding information from me".

[Damiano Testa]

I also sometimes write #eval 0 above the linedeclaration that I am editing, to shield reprocessing the previous declaration.

[Yaël Dillies]

Yes absolutely. This in my opinion is one of the biggest pains of using Lean 4. The typical scenario is that I'm fixing 50 errors in a file, and every time I jump to the next error from the infoview, except that my brain state updates faster than the infoview, so I end up trying to fix the same error several times.

[Sebastian Ullrich]

Kyle Miller said:

I'm pretty sure a lot of the feeling of sluggishness is the delay between editing and the LSP updating the info view. It doesn't update until the entire file has finished processing, unlike Lean 3 where it was once the current command finished.

Uh, which scenario are we talking about exactly? Because I'm editing the very first proof in Kaehler (in VS Code!) and seeing updates just fine

[Yaël Dillies]

Or alternatively I'm fixing an error, and the fix creates an error downstream, but the infoview won't tell me what it is until Lean has recompiled the whole damn file.

[Scott Morrison]

I also can't reproduce (the info view not updating until the entire file has finished).

[Patrick Massot]

I can definitely reproduce. This is indeed very unpleasant.

[Patrick Massot]

Sebastian, are you testing with VSCode?

[Sebastian Ullrich]

Yes, I made sure to say so :)
image.png

[Patrick Massot]

Sorry, I read too quickly.

[Sebastian Ullrich]

In case it's not clear from the screenshot, I commented out h₂ on line 77 of Kaehler

[Sebastian Ullrich]

Which updated both the goal view and flagged the error in the next line

[Patrick Massot]

This is extremely weird. Redoing the exact same experiment here also works, but I can swear this is very unusual.

[Sebastian Ullrich]

I can however confirm that the "All Messages" list does not update until the end. This could be a regression from enabling widgets, I have never seen that happen in Emacs

[Sebastian Ullrich]

Filed as lean4#2367

[Wojciech Nawrocki]

Should be fixed here. I didn't test it very much so testing would be appreciated! You can either impatiently build the extension or wait for the next release.

[Notification Bot]

18 messages were moved here from #lean4 > Lean 4 Toolchain much bigger than lean3 by Sebastian Ullrich.

[Jireh Loreaux]

FWIW, I don't think I've ever experienced this delay.

[Sebastian Ullrich]

Kyle Miller said:

When compiling mathlib, doesn't Lean 4 skip doing things like generating infotrees for the LSP?

It doesn't (as the info trees are used to generate the .ilean files), and there is no significant overhead last we measured. In the end the number of info nodes is roughly linear to the size of the input while the all the bottlenecks usually are in the parts that are not so.

[Kevin Buzzard]

Here's something which just happened to me and which I have always assumed was what Yael was talking about when they said "Lean is hiding things from me". This uses mathlib but I'm sure that someone who knows how to write a Lean function which just pauses for 5 seconds will be able to write a mathlib-free example. With this code:

import Mathlib.RepresentationTheory.GroupCohomology.Basic

noncomputable section

universe u

variable {k G : Type u} [CommRing k] (n : ℕ) [Group G] (A : Rep k G)

namespace GroupCohomology

open CategoryTheory InhomogeneousCochains

set_option trace.profiler true in
set_option pp.proofs.withType false in
set_option maxHeartbeats 400000 in
example : (CategoryTheory.Preadditive.homGroup
    (Opposite.op (HomologicalComplex.X (GroupCohomology.resolution k G) n)).unop A) =
    (CategoryTheory.Preadditive.homGroup (Rep.ofMulAction k G (Fin (n + 1) → G)) A) := rfl

set_option trace.profiler true in
set_option pp.proofs.withType false in
set_option maxHeartbeats 400000 in
example : (ModuleCat.of k (Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A)) =
    HomologicalComplex.X (GroupCohomology.linearYonedaObjResolution A) n :=
  rfl

I'm asking Lean to provide two traces. Both examples take 5-10 seconds on my machine. When the first one has finished compiling I get a blue underline saying to me "woohoo, I have computed your trace", but I can't seem to see any output (neither the trace, nor the goal state if I put my cursor before the rfl) until the second example has finished computing, when suddenly everything appears as normal. @Jireh Loreaux do you experience this? For me the weird thing is that the first example has clearly 100% finished computing, but I can't see any information about it until the second example is also done.

[Jireh Loreaux]

I won't be able to test this for ~10 hours. I'll update when I do.

[Kevin Buzzard]

hopefully you'll test it before I fix the slowness :-)

[Patrick Massot]

I confirm this (except it's slower on my machine, and the second rfl fails, but maybe I'm not on master).

[Matthew Ballard]

Did you overflow the buffer?

[Kevin Buzzard]

Oh I have a bunch of local changes -- maybe just set maxHeartbeats to 0?

[Alex J. Best]

Mathlib-free:

set_option trace.profiler true in
set_option pp.proofs.withType false in
example : 1 = 1:= by
  sleep 5000
  rfl


set_option trace.profiler true in
set_option pp.proofs.withType false in
example : 1 = 1:= by
  sleep 5000
  rfl

and I see the same behaviour

[Matthew Ballard]

[Elab.command] [5.010017s] set_option pp.proofs.withType false in
    example : 1 = 1 := by
      sleep 5000
      rfl ▼
  [] [5.009816s] example : 1 = 1 := by
        sleep 5000
        rfl ▼
    [step] [5.006643s]
          sleep 5000
          rfl ▼
      [] [5.006573s]
            sleep 5000
            rfl ▼
        [] [5.005185s] sleep 5000

is what I see (in nvim)

[Alex J. Best]

But when do you see it? (I can reproduce the above complaint in nvim too)

[Kevin Buzzard]

In VS Code you do not see that information on the first example until after the second example has compiled. Is this not the case in nvim? If you change first sleep to 1000 and the second to 30000 for example, can you see the first trace after 1 seconds or only after 31 seconds? For me with the 1000,30000 situation you can't interact with the first example at all for 30 seconds even though it's compiled after 1.

[Matthew Ballard]

Yes, I do not get the first trace until it finishes processing the file.

[Kevin Buzzard]

And that's why I freqently put #exit just after the declaration I'm working on (to work around this sort of thing).

[Damiano Testa]

My standard workaround for this is to place an #eval 0 in-between the two. Thus, what gets delayed is Lean showing me 0, rather than the previous output... Not great, but it works!

[Arend Mellendijk]

Wait so the issue with the infoview is that it doesn't update until the next declaration is done processing? That would explain why it happens so inconsistently.

[James Gallicchio]

that does seem to be the case -- for me, if you do 3 copies of the example it updates the first infoview after the second (but before the third) declaration processes

[Sebastian Ullrich]

Thanks for getting to the bottom of this, fixed in lean4#2370

[Scott Morrison]

This fix will arrive in Mathlib in #6247 (it looks like it builds cleanly, so if someone could delegate or merge that would be great).

[Kevin Buzzard]

Oh wow! Many thanks for the speedy bump Scott!