View Compute Progress in VS Code

Stream: general

[Bumv]

image.png

Hello. I would like to know what LEAN is doing while it is displaying "Loading messages...",
I managed to do it before where it displayed -> "Loading Mathlib.Tree.A 456/712" (For example) but I can't seem to replicate it. Does anyone know how to do this?

[Sebastian Ullrich]

Is there a message in the first line of the file? If so, does it show you more?

[Sebastian Ullrich]

Note that compiling unchanged mathlib4 files should not be necessary after retrieving the cache as described in the mathlib readme

[Bumv]

image.png
Is this the info I am looking ofr?

[Bumv]

I think that's it, thank you for helping!

[Sebastian Ullrich]

Addressing lean4#2367 will make sure it is displayed in All Messages as well

[Kevin Buzzard]

Yeah you're compiling mathlib, which you don't need to do if you've got an internet connection: try lake exe cache get on the command line