Client 1 quit with exit code 0 and signal 11 about lean.nvim HOT 5 CLOSED

if I'm honest I'm not very interested in helping make sure you did :)

I appreciate your honesty :D

$ lake exe cache get          
zsh: segmentation fault  lake exe cache get

Perhaps I should try getting Lean from Elan instead, thanks for suggestion!

from lean.nvim.

/usr/bin/lake Is a slightly suspicious place for your lake to be. What's the output of type -a lake in a terminal?

How did you install Lean?

And what happens if you run lake build?

from lean.nvim.

What's the output of type -a lake in a terminal?

$ type -a lake
lake is /usr/bin/lake

How did you install Lean?

Through the package manager in Gentoo:

$ emerge lean
$ equery l lean
 * Searching for lean ...
[IP-] [  ] sci-mathematics/lean-4.2.0_rc4:0/4

And what happens if you run lake build?

$ lake build
<it consumes one processor core & some 200m of RAM, yet no output>

from lean.nvim.

Does your version of lean match your project then? Installing lean via anything but elan isn't really supported by the community. It of course will work if you do it right but if I'm honest I'm not very interested in helping make sure you did :) so you'll have to do so on your own before trying to use this plugin or else use elan.

from lean.nvim.

Ok, seems to be the problem with lean itself when compiled for x86 architecture.

from lean.nvim.