Tips for speeding up company-lean

Stream: general

[Adam Topaz]

I still have this dream of using emacs for Lean(3). Today I had some OS upgrading issues and had to remove electron (and thus also vscode), so I tried emacs again, and I was immediately reminded of why I switched to vscode -- writing lean in emacs is tediously slow!
One of the main culprits is company-lean which is automatically trigerred in my setup (I'm using doom emacs, and lean is available as one of the built in packages). When it's triggered, all typing seems to stop, and things become unusable for several seconds.
Does anyone have any hints for speeding up company-lean? Does anyone have any hints for speeing up lean development in emacs in general?

[Reid Barton]

I don't remember ever seeing this behavior so maybe it is caused by the doom emacs configuration somehow?

[Henrik Böving]

The usual stuff I do to prevent my company auto complete to lag is to limit the word length at which it triggers (t's 3 rn) and the maximum count of suggestions it provides, maybe that helps?

[Reid Barton]

I'm a bit confused by the company-mode documentation, is autocompletion supposed to be getting triggered automatically?

[Reid Barton]

I see there is stuff like what Henrik mentioned, but it doesn't seem to do anything for me (luckily!)

[Henrik Böving]

Yes, company has a concept of so callled "backends" that essentially act as suggestion providers which it goes through whenever the preconditions for company to trigger (that is, the idle timeout as well as the minimum word length) is triggered, if any of the backends provide something its shown.

[Adam Topaz]

I have it set to automatically trigger after 1 idle second, but once it's triggered, the lag is crazy

[Henrik Böving]

I do for example have this setup: https://github.com/hargoniX/dotfiles/blob/master/dotfiles/init.el#L383-L400 and manually add a yasnippet backend here so I can see them in autocomplete: https://github.com/hargoniX/dotfiles/blob/master/dotfiles/init.el#L402-L409

[Reid Barton]

So just to check, you mean the selection menu pops up automatically after a short delay whenever it has suggestions?

[Reid Barton]

I just have M-n bound to company-complete and press it manually

[Adam Topaz]

Reid Barton said:

So just to check, you mean the selection menu pops up automatically after a short delay whenever it has suggestions?

yes, that's right

[Henrik Böving]

Are you on emacs 28 already? That one could also provide a huge speedup if the slowdown is inside emacs itself since it can compile the lisp stuff to C

[Adam Topaz]

I am! 28.1

[Reid Barton]

Well it looks like you can set company-idle-delay to nil to prevent that from happening, though I'm still confused why it doesn't happen to me (probably I am on an old version of something)

[Adam Topaz]

I should say that I want it to pop up automatically.

[Adam Topaz]

I'll try out some of Henrik's configurations later and see if they help! Thanks!

[Reid Barton]

I know this is very https://xkcd.com/1172/ but having the menu pop up automatically sounds awful, IMHO

[Yaël Dillies]

Why did I know precisely which xkcd that was :laughing:

[Henrik Böving]

Thats the reason I set it to 0.5, if im still in the same spot in insert mode after 0.5 seconds i probably want the menu to pop up anyways^^