Lean 3立即挂起import语句

Question

我正在尝试使用精益的mathlib，但是在导入时失败。当我在没有任何导入语句的文件上编写#print notation时，它会执行；如果我在一个文件上包含相同的命令，即使只有一个import data.real.basic，程序也会挂起，而不会打印任何内容。任何帮助修复此错误的人都将不胜感激。

Answer 1

这是一个路径错误。

leanproject并不存在(或者我是这样想的，实际上它只是从来没有添加到$PATH中)，所以我尝试使用leanpkg添加mathlib。

每次我尝试执行任何文件并编译它(花费一个多小时)时，它都会从git中取出整个代码。