Integrate `leanproject get` into VS Code?

Stream: general

[Yury G. Kudryashov]

Is there a way to download a lean project from github from VS Code without opening a terminal?

[Eric Wieser]

Presumably there's a github extension for vscode?

[Eric Wieser]

https://code.visualstudio.com/docs/editor/github

[Arthur Paulino]

Alternatively, if you just want to avoid the terminal but are open to other git GUI's, many people are fond of the GitHub Desktop App

[Johan Commelin]

Eric Wieser said:

Presumably there's a github extension for vscode?

That wouldn't grab oleans for you, right.

[Eric Wieser]

No, but I think it makes more sense to teach vscode-lean to grab oleans through the UI than it does to teach it how to use git

[Eric Wieser]

It already knows how to run leanpkg configure, it could ask to run leanproject get-mathlib-cache too

[Eric Wieser]

It's probably easier not to have vscode-lean try to install mathlibtools, and just have it detect (via a config option or $PATHby default) and use it

[Yury G. Kudryashov]

The student downloaded the project using command line. @Kevin Buzzard Could you please explicitly write in the README of https://github.com/ImperialCollegeLondon/formalising-mathematics that users should not download the code using "download zip file" or "git clone"?

[Kevin Buzzard]

I updated it