Lean4 解决‘导入已经过时’的好方法

Question

我按照官方文档创建了一个项目。但如果我写

import Mathlib

在

my_project/Basic.lean

中，我收到警告：在 vscode 中

Imports are out of date and must be rebuilt; use the "Restart File" command in your editor

。

如果我单击“重新启动文件”并等待一个世纪，它确实修复了警告。单击“重新启动文件”后到底发生了什么？

Imports are out of date

是什么意思？这是否意味着我没有使用最新版本或其他版本？

有什么办法可以避免等待一个世纪来重建包裹？

Answer 1

在命令行上运行

lake exe cache get

以下载 Mathilb 预编译的

olean

文件。