install leanprover/lean4 again and again

hi,

I have installed lean4 manually using elan-init.sh.

And I have set enviroment variable on linux

export ELAN_HOME=/opt/elan
export PATH=$ELAN_HOME/bin:$PATH

And I also downloaded toolchains from lean4, including version 4.33 and 4.30. Both the 2 versions are un-archeived to /top/elan/toolchains. And I can see they can be found by elan toolchain list:

It seems that my env-var and installation are successful.

However, when I open VSCode with Lean 4 extension installed, and open the cloned mathematics_in_learn. it start to down load and install lean-4.30.0-linux.tar.zst again. The log is shown below:

/home/schoenberg/work/study/lean/mathematics_in_lean> curl --version
curl 7.81.0 (x86_64-pc-linux-gnu) libcurl/7.81.0 OpenSSL/3.0.2 zlib/1.2.11 brotli/1.0.9 zstd/1.4.8 libidn2/2.3.2 libpsl/0.21.0 (+libidn2/2.3.2) libssh/0.9.6/openssl/zlib nghttp2/1.43.0 librtmp/2.3 OpenLDAP/2.5.18
Release-Date: 2022-01-05
Protocols: dict file ftp ftps gopher gophers http https imap imaps ldap ldaps mqtt pop3 pop3s rtmp rtsp scp sftp smb smbs smtp smtps telnet tftp 
Features: alt-svc AsynchDNS brotli GSS-API HSTS HTTP2 HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM NTLM_WB PSL SPNEGO SSL TLS-SRP UnixSockets zstd

/home/schoenberg/work/study/lean/mathematics_in_lean> git --version
git version 2.34.1

> elan toolchain install leanprover/lean4:v4.30.0
warning: could not check for elan self-update: error during download
info: downloading https://releases.lean-lang.org/lean4/v4.30.0/lean-4.30.0-linux.tar.zst
error: could not download file from 'https://releases.lean-lang.org/lean4/v4.30.0/lean-4.30.0-linux.tar.zst' to '/opt/elan/tmp/k_4b23rp_oa1f5f__file'
info: caused by: error during download
info: caused by: [60] SSL peer certificate or SSH remote key was not OK
=> Operation failed. Exit code: 1.

It is failed due to my bad network.

However, I have installed elan and lean on my PC already, why it comes out to download and install again?

Start with the VS Code extension's toolchain setup for the mathematics_in_lean project and the elan toolchain install leanprover/lean4:v4.30.0 command shown in the log. Trace why the existing /opt/elan/toolchains installation is not reused, then reproduce the behavior and confirm that the project opens without an unnecessary download or clearly reports the remaining prerequisite.