Importing

Stream: mathlib4

[Ryan Buchanan]

"Imports are out of date and must be rebuilt; use the "Restart File" command in your editor." Why am I getting this and what do I do? Edit: I see. I have successfully imported Mathlib and am waiting for everything to build. #check (x) says "loading" when I hover over it for x \in Mathlib. Hopefully this works when it's all built!

[Josha Dekker]

Ryan Buchanan said:

"Imports are out of date and must be rebuilt; use the "Restart File" command in your editor." Why am I getting this and what do I do? Edit: I see. I have successfully imported Mathlib and am waiting for everything to build. #check (x) says "loading" when I hover over it for x \in Mathlib. Hopefully this works when it's all built!

Instead of building it locally, you can try ‘lake exe cache get’ to get built files!