Emacs lean4-mode: major lags during autocompletion

Stream: general

[Jannis Limperg]

After an Emacs update today, lean4-mode sometimes produces major lags during autocompletion. I've reported this as lean4-mode#65, but I can't really pinpoint where the issue lies. So if other people also start experiencing these lags, any additional clues would be helpful.

[Richard Copley]

Sorry to hear that!
None of the code that implements autocompletion is in lean4-mode. I don't much use the lsp-mode based lean4-mode, but if I were investigating I might start by attempting to bisect this to a particular revision of lsp-mode. Admittedly it doesn't sound fun.

[Jannis Limperg]

Indeed I was also able to trigger the behaviour with lsp-haskell (though much more rarely -- maybe their autocompletion is faster and so the presumed race condition doesn't happen as often). So most likely not a lean4-mode issue. Thanks for the pointer!