Vscode extension ignore toolchain location override

Stream: new members

[Roman]

Hello, I can't set the vscode extension to use my toolchain:
placing the content of lean-4.22.0-windows.tar.zst\lean-4.22.0-windows.tar\lean-4.22.0-windows\ (containing src, share, lib, etc) inside .elan/toolchain\4-22, make it appear as installed and is selected successfully when clicking on the inverted A icon -> Version Management... -> Select default Lean version... -> and selecting 4-22 (installed).

However, doing New project -> Create standalone project output No Lean version for release channel 'leanprover/lean4:stable' is installed. and installing it give me https://github.com/leanprover/elan/issues/176

This :

PS C:\Users\Roman BIS> .\.elan\bin\elan.exe toolchain uninstall 4-22
info: no toolchain installed for 'leanprover/lean4:v4-22'
PS C:\Users\Roman BIS> .elan/bin/elan toolchain link 4-22 .\.elan\toolchains\4-22\
error: '4-22' is already installed

let me believe I had to extract it somewhere else in order for elan to create a symlink successfully and perhaps saving it in its config or something however it behaved exactly the same way :

PS C:\Users\Roman BIS> .elan/bin/elan toolchain link 4-22 .\.elan\4-22\
PS C:\Users\Roman BIS> elan show
4-22 (default)
Lean (version 4.22.0, x86_64-w64-windows-gnu, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05, Release)
PS C:\Users\Roman BIS> elan override set 4-22
info: override toolchain for 'C:\Users\Roman BIS' set to '4-22'
# Select default Lean version and create standalone project -> fail

Any help ? I tried to use mitmproxy but it started to check for certificate revocation stuff etc and I stopped there

[Marc Huisinga]

Out of curiosity: why are you trying to manually install toolchains?

[Roman]

Because I can't download it, see the Github link I posted, others create a https proxy on their system to workaround it.
By the way the same issue is found on Firefox and I had to download using Jdownloader

[Marc Huisinga]

Ah, thanks.

Creating new projects with a specific toolchain that isn't the most recent stable toolchain (as set by leanprover/lean4:stable) unfortunately currently isn't supported by the VS Code extension, but you should be able to use the command-line to create the project instead.

First confirm that your custom Lean version is correctly set up by running lean --version. Then, run lake init in the directory where you want your project to be created (or lake new <project name> if you want to create a new project directory).