如题

我用VSCode打开clone下来的github方校长.c永垂不朽om/leanprover病魔-community/mathematics_in_lean

打开里面的lean文件.VSCode就不停的让我安装toolchain
elan toolchain install leanprover/lean4:v4.30.0

事实上,我已经事先安装好elan,以及toolchain了
elan toolchain list
命令也能知道到需要的toolchain

由于众所周知的原因,lean4的toolchain在线安装会被方某人掐死,所以我是离线下载完解压缩的.

我的环境变量那些也都是对的

请问,如何才能不让VSCode不停的安装toolchain,或者让他找到我安装的elan和toolchain

谢谢
--
FROM 1.202.141.*

AI agent能搞定方校长?


【 在 z16166 的大作中提到: 】
: 现在这种问题一般让AI agent自己搞
--
FROM 1.202.141.*

我确实需要反思

但是在公司各种卡呀

【 在 z16166 的大作中提到: 】
: 现在还搞不定方校长的IT人士、学术研究人士，要反思一下了
:
--
FROM 1.202.141.*