Closed arbitrary-dev closed 9 months ago
/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
?
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>
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.
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!
Ok, seems to be the problem with lean
itself when compiled for x86 architecture.
I've added following to my
~/.config/nvim/lua/plugins/lean.lua
:I also enabled LSP tracing:
Yet no warnings for my file. And running
:LeanRestartFile
results in:Info window is present, though nothing there.