lean - Lean4 good way to solve `imports are out of date` - Stack Overflow

I created a project following the official document. But if I write

import Mathlib

In my_project/Basic.lean, I get a warning: Imports are out of date and must be rebuilt; use the "Restart File" command in your editor in vscode.

It does fix the warning if I click "Restart File" and wait for a century. What exactly is happening after clicking "Restart File"? What does Imports are out of date mean? Does it mean I'm not using the newest version or something else?

Is there any way to avoid waiting a century to rebuild the package?

I created a project following the official document. But if I write

import Mathlib

In my_project/Basic.lean, I get a warning: Imports are out of date and must be rebuilt; use the "Restart File" command in your editor in vscode.

It does fix the warning if I click "Restart File" and wait for a century. What exactly is happening after clicking "Restart File"? What does Imports are out of date mean? Does it mean I'm not using the newest version or something else?

Is there any way to avoid waiting a century to rebuild the package?

• lean

Share Improve this question Follow asked yesterday SSSSSS 5133 bronze badges

Add a comment  | 

1 Answer 1

Sorted by: Reset to default 0

Run lake exe cache get on the command line to download pre-compiled olean files for Mathilb.

(You can also do this without the command line in VSCode: Click the "forall" icon, then "Project actions", then "Fetch Mathlib Build Cache".)