should lean.vim be working on BigSur macos?

Stream: general

[Ao Decipher]

Hi everyone,
Quick question, is lean.vim working for you on macos, can't get lean.vim to work on my mac here. I got lean working in both VScode and emacs work on mac, so probably not a hardware thing. I have an Apple silicon mac mini with BigSur. The same lean and vim settings works on my Ubuntu 20.04. I attached the error in vim below. The plugin I use is coc.
Runing "lean test.lean" gives no error and shows the correct result of "#check topological_space".
Many thanks for any feedback!
image.png

[Julian Berman]

Hi. It works for me yeah, though with some elbow grease -- are you in the right directory within vim? i.e. is :pwd the same directory you ran lean test.lean from?

[Julian Berman]

Probably sharing :!lean --path ran from within vim may help as well.

[Ao Decipher]

Hi Julian, thanks for such a prompt response. Yes, I think I'm in the right dir. See below:
image.png
image.png
I'm not in any venv. My vim version is 8.2.
I noticed that you are developing lean.nvim. I copied the whole of your nvim folder (commented out the key bindings), but when opened the test.lean using the latest nvim (NVIM v0.5.0-dev+1321-gc57a85d53), it gave me those same errors, both in mac and ubuntu. As mentioned above, in ubuntu vim 8.2 opened test.lean without error.
P.S. I'm not an expert in vim or in coding in general.
Thanks again.

[Ao Decipher]

running lean --path, first in terminal outside vim, then within vim. The output looks the same to me.
image.png

[Julian Berman]

If you're not specifically keen on vim you're probably going to have a ton of an easier time using one of the officially supported editors. Or with VSCode with its vim emulation. I spend a lot of time futzing with things that could instead be spent on actually writing Lean :), but I find both fun. And yeah that output looks fine.

[Julian Berman]

Have you installed lean-language-server?

[Ao Decipher]

yeah, i did consider just writing lean in vscode with its vim extension... but I do love vim and I kept thinking what if...
after all lean.vim did work on Ubuntu. so that answers the question about lean-language-server, yes I have that.
update: your nvim setup also works on Ubuntu, I probably missed a step or two there. here's the new screenshots for both vim and nvim on ubuntu
image.png
image.png
seems like I am that close to getting it working in vim.
for some reason the info view isn't showing anying?
If I can't get it to work in the next couple of hours, I'll just stick with vscode...

[Julian Berman]

Right, ok that's good!

So just importing from mathlib isn't working for you?

[Julian Berman]

Oh, no, in your screenshot that works too

[Ao Decipher]

those screenshots are from ubuntu

[Ao Decipher]

they work on ubuntu, but not on mac

[Julian Berman]

Ah got it. So the infoview is very basic right now (I'm working on some customization there but it's not done)

[Julian Berman]

Right now it just shows goal state

[Julian Berman]

So you won't see anything there for those lines

[Julian Berman]

(i.e. it doesn't collect all diagnostics and show those, I like those where they are by default, inline in the file)

[Ao Decipher]

ok, so it's normal, that's a relief. ok, i'll forget about macos for now and use it on ubuntu

[Ao Decipher]

thanks so much

[Julian Berman]

No problem. Feedback welcome of course, and yeah the macOS bit is odd, I'm on macOS myself.

[Ao Decipher]

haha, i probably can try it on a new account on macos, but for now i guess i should restrict myself, and write some lean code...

[Julian Berman]

Yes :) probably.

[Ao Decipher]

Your lean.nvim works really nice. Great work!
A question off topic: given that Lean already has an official emacs version, and you are surely more than capable of creating a satisfying vim-like environment on top of that in emacs, why do you still choose to spend the time and develop lean.nvim?
In general, I'm curious why you choose vim over emacs. Today I was questioning myself about this.

I read people saying emacs can do everything vim can do, but not vice versa. I have been using vim for about a year, and now the keybindings and modes are very natural to me. But I just found out sagemath has an official emacs version (i've been using vim-jupyter), and of course Lean also has an emacs version. I question whether starting to seriously learn vim script is worth it. I began learning vim because it is everywhere, but I don't really need to access slow remote devices everyday, and perhaps I already learned / adopt its best part, which I think is its modal design? With evil-mode in emacs, will it be more productive if I spend the time learning elisp instead of vimscript, if I want to pursue the goal of ultimately doing almost everything using only the keyboard, with only one set of custom keybindings?

Thanks as usual!
P.S. Not sure if it's ok to post this question here. Perhaps I should move it to private message or ask you on github?

[Julian Berman]

Hah, yes this is a topic people can and have argued about for hours, days and years :) so probably we can spare the Lean Zulip of it. The short answer is "any of the above are good tools so whichever suits your brain is the right one". But feel free to send me a private message :).