VSCode install Lean4 Stable

Stream: new members

[Daniel Patterson]

With elan, I can select the "leanprover/lean4:stable" toolchain, which right now is the 4.0.0-m5 release. Is there any way to have the nice one-click inside VSCode install select that toolchain? I have a class that'll be installing it quite soon, and the idea that they might all be on slightly different nightly versions is a _nightmare_, but also, being able to just have VSCode install is nicer than dealing with commandline stuff.

[Daniel Patterson]

I'm assuming the lack of response means this isn't possible! That was what I thought, but thought I'd check in case there was something undocumented!

[Mario Carneiro]

Perhaps some of the folks who teach with lean can chime in, but if you use a lean-toolchain file, then elan will automatically select the right version, so if you distribute a lean project for students to work in which has the lean-toolchain file already set then this will not be an issue even if you are on nightly

[Mario Carneiro]

this is true even if you use the vscode one-click install, since this installs elan which downloads the right version of lean

[Mario Carneiro]

(Also, lean 4 isn't really stable. Those are release candidates, and the last one was some time ago and I wouldn't really recommend it. Lean 4 is still working toward the stable release.)

[Kevin Buzzard]

I teach with lean 3 but I just tell my class "download the course repo" and they're then all on the same lean

[Patrick Massot]

Daniel, I recommend you provide autonomous archives, similar to what you can find at Maybe a couple of nights. You can see what's inside at https://github.com/leanprover-community/azure-scripts/blob/master/mk_bundle.py. If your users are more experts and VSCode is already installed then you can prepare a shell script to download and execute.