[环境配置]关于使用国内镜像安装 Mathlib/Lean4思考
之前按照https://zhuanlan.zhihu.com/p/680690436文章安装lean4非常方便，但是现在发现这个文章已经失效了，而且那个glean看起来就是个鸡肋，怎么都是安装不了，里面安装方法还有个问题就是上海交大的那个源地址变了，glean还是用的以前地址，导致根本无法下载。因此搞懂安装流程，窥探里面安装技巧十分重要，甚至可以不用他的安装流程就能安装成功。
（1）glean作用是什么？
看安装流程glean似乎就是exe文件只是为了下载elan，因此手动下载elan就可以解决问题，所以你有科学工具完全可以扔掉这个glean.exe
（2）elan作用是什么？
elan-init.exe下载后会有个powershell脚本进行安装，如果选择default安装，可以看到在C:\Users\用户名\.elan生成一些文件，而且打开查看有部分文件明显是lean4里面的东西，但是需要科学上网所以没法正常使用elan-init.exe这个命令行工具。不难想到这个就是为了安装lean4而已，其实你可以不用elan-init.exe安装
可见上面2个exe都是辅助工具，其实你懂背后安装原理只是为了照顾初学者让他们更快安装上lean4
可见其实都是可以手动下载文件进行解决，希望能帮到安装lean4的困扰的童鞋。
原文地址：https://blog.csdn.net/FL1623863129/article/details/143033556
免责声明：本站文章内容转载自网络资源，如本站内容侵犯了原著者的合法权益，可联系本站删除。更多内容请关注自学内容网（zxcms.com）！