Imports are out of date and must be rebuilt

Stream: new members

[Matthew Bouyack]

Hi, all! I'm just getting started with Lean and trying to work through the "Mathematics in Lean" exercises. I've followed the recommended setup instructions, but my Lean infoview seems to always indicate that my imports are out of date and must be rebuilt.

If I click "Restart File" and wait ~2 hours it will finish building and the problem goes away. But if I close and reopen VS Code the problem returns. I've tried using the command "lake exe cache get" which seems to complete successfully, but has no effect on the error message. I've tried both running the command from VS Code and then restarting VS Code, and from Git Bash while VS Code is not open and then launching VS Code. In both cases the error persists.

Any suggestions?

[Ruben Van de Velde]

The cache get command should fix that. I need to step out, but probably someone can help debug

[Ruben Van de Velde]

But you're definitely not expected to build mathlib yourself

[Nicolas Rolland]

sometimes running rm -rf .lake then a fresh lake exe cache get solves some issues.

Also if you have a branch, tracking the master's head and rebasing your change might be a good idea (I dont know if it is but I do as I dont know how that cache works exactly ...)

[Matthew Bouyack]

Thanks! I'll try that the next time I need to restart VS Code or my computer. For now everything seems to be working (after taking the time to do a full local build).

[Ruben Van de Velde]

I imagine that as long as the version of mathlib doesn't change, you'll be able to keep using the build you have right now (unless you remove .lake)

[Michael Rothgang]

For me, lake exe cache get usually works like a charm, but sometimes doesn't (then I see lots of rebuilding). In these cases, I often close vs code, ensure all lean processes are stopped, and run lake exe cache get!.
This will re-download the entire cache, so use sparingly - but sometimes, having a really big hammer helps.