Avoiding all command line actions through VC Code menus

Stream: general

[Hunter Monroe]

I suggest finding a way to avoid all need for command line actions adding new Lean-specific menus to the Lean VS Code extension, in particular: everything related to managing lean projects ("leanproject get tutorials" and other leanproject commands), installing mathlib when the extension is first installed (check if python is available or send to web page, pip3 install mathlibtools), contributing to mathlib ("leanproject get -b mathlib:shiny_lemma", "git push origin"). This may require some effort to get it to work on all OSs but would be more user friendly.

[Scott Morrison]

The counter-argument here is that having "the one true way" to install also results in less confusion. Multiple supported options just seems to encourage people to improvise. :-)

[Alex J. Best]

I quite like the idea of hooking in some leanproject commands (Like "ctrl+shift+P Lean: Get cache" would be great), but as for the git side there are a lot of git gui plugins (with support for the PR process and more) available in vscode already.