установить lean из расширения в vscode чтобы работала команда leanpkg: source $HOME/.elan/env строит зависимости leanpkg build