search

leanprover-community / lean4-mode

Emacs major mode for Lean 4
https://leanprover.github.io/
Apache License 2.0
62 stars 27 forks source link

Major lags during autocompletion #65

Closed JLimperg closed 2 months ago

JLimperg commented 2 months ago

I updated to Emacs 29.4 today and since then, autocompletion has regularly produced ~3s lags during which the entire editor UI freezes. Unfortunately, I also updated a number of packages during the update, so it's hard to tell where the issue lies exactly. I hope you'll be able to reproduce with the following info.

Emacs: 29.4 Doom Emacs: a99c6b9036bde2f60697ce9f2ac259dfa2266dbf Relevant packages (?):

lsp-mode cec9e56390e90d7ced3b18a922ab954e782b8628
lsp-ui 00f1fecdfb41c30428734cf27e492f26f46627fb
lean4-mode da7b63d854d010d621e2c82a53d6ae2d94dd53b0
company-mode 1a0fc12a9c3d25e28c22f319e7b097f435b1c27d

Repro:

  1. Clone https://github.com/leanprover-community/aesop and check out f465af4466eeb1f195692745fd58bb3f552692f1.
  2. Open Aesop/RuleTac/Forward.lean.
  3. On line 170, remove elabRuleTermForApplyLikeMetaM and type elabRuleTermForApplyLikeMetaM instead. This reliably freezes the UI at some point and autocompletion appears once the UI unfreezes again.

The freeze doesn't always happen at the same point and it only happens when I type somewhat slower than normal, so perhaps the issue is typing when an autocompletion request is already in-flight.

Disabling autocompletion (lsp-completion-enable nil) works around the issue.

JLimperg commented 2 months ago

This appears to be an issue of lsp-mode, not of lean4-mode. See discussion on Zulip.