VSCode lag

Stream: general

[Patrick Massot]

Is it only on my computer or do other people noticed that the VSCode extension became very laggy sometimes? Since at least one week, I often get into a situation where the info view doesn't display anything and then suddenly catches up and very quickly displays everything it should have displayed in the previous 15 seconds. This is very distracting and would be catastrophic for teaching.

[Floris van Doorn]

Yes, I have also noticed this sometimes (on Linux). On Windows I sometimes get even worse behavior, where it might take multiple minutes for the server to start "catching up".

[Bolton Bailey]

I occasionally get an issue where I experience lag for each keystroke I make. If I type rw my_lemma, The info view will display "unknown identifier: 'r'" for half a second, then "unknown identifier: 'rw'" for half a second, then "unknown identifier: 'm'", then "unknown identifier: 'my_l'", until eventually it processes the whole 'my_lemma' string and succeeds.

[Yakov Pechersky]

This usually happens if you're editing a file very basic in the import hierarchy while you have other files open that are deep descendants of the file being edited

[Yakov Pechersky]

One way to reduce that lag is to close those other files. Another is to put an #exit right below what you're editing in the moment, which will prevent the rest of the file from being reinterpreted after every keystroke. This will result in snappier UI

[Patrick Massot]

No, it happens when I'm editing a leaf file in a project which is not mathlib, without any modified mathlib file

[Patrick Massot]

And this is a recent issue.

[Yaël Dillies]

I've had that behavior this August at least.

[Huỳnh Trần Khanh]

ah i often encounter that issue when using the slow linarith tactic :joy: and I usually fix that issue by replacing linarith with an explicit proof of the inequality

[Huỳnh Trần Khanh]

I find that avoiding linarith and using clear_except help a lot

[Huỳnh Trần Khanh]

like when I run clear_except things usually run a lot faster, especially library_search and gptf also gives more accurate suggestions