lean, nvim and pynvim

Stream: lean4

[Antoine Chambert-Loir]

I am trying to do lean using neovimand the configuration files of @Patrick Massot which can be found there.
(I am on MacOS.)
This blocks almost immediately, with a one page error message whose most informative line could be

E319: No "python3" provider found. Run ":checkhealth provider"

It seems that I can't understand how to install pynvim. It is not distributed by brew, and python3 -m pip install --user --upgrade pynvim protests that python3 is externally managed.

[Julian Berman]

You got your neovim from running brew install neovim right?

[Antoine Chambert-Loir]

yes.

[Julian Berman]

I'm not in front of a computer so this will be from memory but the usual way to do this is you set vim.g.python3_host_prog = '/path/to/pythonvenv/with/pynvim/installed'

[Julian Berman]

E.g. I do that here: https://github.com/Julian/dotfiles/blob/9bc6a15e20137bde8baff244572da5577f215023/.config/nvim/init.lua#L293

[Julian Berman]

I'm not in front of a computer but a fuller recommendation would be run brew install uv and then uv venv ~/.local/share/nvim/venv && uv pip install --python ~/.local/share/nvim/venv/bin/python pynvim and then add vim.g.python3_host_prog = thatpythonpath`

[Julian Berman]

If that doesn't get you there I can write out fuller instructions in a few hours

[Antoine Chambert-Loir]

I followed your first instruction and it seems to work. Thanks a lot!