neovim - recompile dependencies

Stream: general

[Antoine Chambert-Loir]

I quickly browsed through the neovim config files of @Julian Berman and @Patrick Massot but didn't find the answer there: how is it possible, from within neovim, to ask Lean to recompile the modified dependencies?
— Or do you simply launch lake build in a separate window?

(Side remark: it is annying to have to change / directory separators to . in order to compile a given lean file in lake build: maybe there's a way to do that? — Or I can make my own make command that'll adjust the syntax.)

[Matthew Ballard]

:LeanRefreshDependencies ?

[Patrick Massot]

You can see at https://github.com/PatrickMassot/neovim_config/blob/master/lua/keymaps.lua#L34 that I even reproduced the VSCode keybinding for it since it was so present in my muscle memory.

[Patrick Massot]

Antoine Chambert-Loir said:

(Side remark: it is annying to have to change / directory separators to . in order to compile a given lean file in lake build: maybe there's a way to do that? — Or I can make my own make command that'll adjust the syntax.)

See lean4#2756

[Matthew Ballard]

Also very popular :)

[Matthew Ballard]

@Julian Berman had a script also I think

[Julian Berman]

This zsh completion script: https://github.com/Julian/dotfiles/blob/main/.config/zsh/completions/_lake which basically converts / to . on tab complete.