Long compilation of mathlib

Stream: general

[Vasily Ilin]

It takes about 2 hours to build mathlib on my computer. I just (re)cloned MIL, and it has been 90 minutes, and I am ~75% done. Is this expected? Seems annoyingly long.
image.png

[Kyle Miller]

Did you do lake exe cache get like the instructions in the book say to do? (Maybe it's not super clear that it's telling you to do this, since it's in the paragraph about git pull, but it's in the linked instructions here)

[Kyle Miller]

(It looks like this is a continuation of this thread?)

[Vasily Ilin]

image.png
I had forgotten to run it. Now that I did, I get a bunch of errors. I suspect it's because my laptop is still trying to compile mathlib in the background

[Kyle Miller]

Yeah, it doesn't work during a build of mathlib. Turn off VS Code and try again.

[Kevin Buzzard]

It takes about 2 hours to build mathlib on my computer. I just (re)cloned MIL, and it has been 90 minutes, and I am ~75% done. Is this expected? Seems annoyingly long.

I think for many people, the answer to this question is "I have no idea how long it takes to build mathlib, because we have the necessary infrastructure in place which means we never have to do this". That is certainly my answer!

[Yaël Dillies]

At the rate I use mathlib, I would need two hours of mathlib building every 5min!

[Michael Rothgang]

I'm glad there's multi-threading :see_no_evil:

[Vasily Ilin]

I don't quite understand these answers. What is the infrastructure that can help me with this? I had to turn off my laptop before it finished the compilation and now I am stuck waiting almost from the start.

[Vasily Ilin]

To be clear, I now ran lake exe cache get but it did not seem to do anything (downloaded 4000 files and that's it, compilation still needs to happen, it seems)

[Kyle Miller]

lake exe cache get downloads pre-built lean modules so that you don't have to compile anything. It should Just Work.

What are the details of your system? Did do anything else to the repository? (Like, for example, don't do lake update.)

[Kim Morrison]

In particular, if git status reports no changes relative to master, VS Code is closed, and you've just run lake exe cache get, and then lake build does any work, then this is a bug we want to fix urgently.

(Well, maybe after asking you delete .lake and try again to make sure nothing really weird has happened.)

(If VS Code is open as well this should work if VSCode is not actively building something, but this can be hard to tell so some people close VS Code every time. I don't, and just restart the server using cmd+shift+p.)

For non-master branches, lake exe cache get should work as well, but it may take up to an hour after the most recent push to that branch for the .oleans to be available: but the output of lake exe cache get will explain if they are not available.

[María Inés de Frutos Fernández]

Vasily Ilin said:

To be clear, I now ran lake exe cache get but it did not seem to do anything (downloaded 4000 files and that's it, compilation still needs to happen, it seems)

Try running lake exe cache get! (this worked for some participants of LftCM that were having this same issue yesterday).