Zulip Chat Archive

Stream: general

Topic: VSCode lag


Patrick Massot (Nov 29 2021 at 15:37):

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 (Nov 29 2021 at 17:06):

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 (Nov 29 2021 at 17:22):

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 (Nov 29 2021 at 17:43):

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 (Nov 29 2021 at 17:44):

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 (Nov 29 2021 at 17:47):

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

Patrick Massot (Nov 29 2021 at 17:47):

And this is a recent issue.

Yaël Dillies (Nov 29 2021 at 18:19):

I've had that behavior this August at least.

Huỳnh Trần Khanh (Nov 30 2021 at 02:15):

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 (Nov 30 2021 at 02:17):

I find that avoiding linarith and using clear_except help a lot

Huỳnh Trần Khanh (Nov 30 2021 at 02:18):

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


Last updated: Dec 20 2023 at 11:08 UTC