Zulip Chat Archive

Stream: new members

Topic: VSCode install Lean4 Stable

Daniel Patterson (Jan 25 2023 at 18:10):

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 (Jan 27 2023 at 01:44):

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 (Jan 27 2023 at 02:23):

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 (Jan 27 2023 at 02:25):

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 (Jan 27 2023 at 02:26):

(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 (Jan 27 2023 at 08:27):

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 (Jan 27 2023 at 08:41):

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.

Last updated: Dec 20 2023 at 11:08 UTC