lake build takes forever when updating mathlib

Stream: general

[shortc1rcuit]

I've been doing some work in the Compfiles project and I've found an annoyance whenever mathlib gets updated there. I have to rebuild the files using lake build, which causes my laptop to build over 4500 files. This takes over an hour and puts my laptop's CPU under a lot of strain. However, if I delete my .lake folder and then build, it builds a fraction of the files. Is there a way to build without deleting and redownloading everything?

[Henrik Böving]

You should be able to just run lake exe cache get to download mathlib's build cache

[shortc1rcuit]

I did make sure to do that. The same problem occurs.

[Henrik Böving]

That's unusual. Is your toolchain the same as the one from the mathlib commit you are using as well?

[shortc1rcuit]

I ran elan update and lake update.

[Henrik Böving]

That's not going to fix your toolchain to the one mathlib uses. Mathlib's master branch usually uses the latest stable version available (up to relese candidates), you can check their lean-toolchain file. Your lean-toolchain file must match that such that you can use mathlib's build cache.

[shortc1rcuit]

Ours are both leanprover/lean4:v4.10.0-rc2

[Henrik Böving]

Then it's not quite clear to me why the cache doesn't work I'm afraid

[Henrik Böving]

Maybe someone else who knows that part of the infra better can help.

[Kim Morrison]

@shortc1rcuit, could you provide a commit that someone could check out, at which lake exe cache get appears to work, but lake build still needs to recompile?

[shortc1rcuit]

Jumping to this commit (i.e. the one before this commit) seems to recreate the issue for me.

[shortc1rcuit]

Also it may be an issue with lake exe cache get

[shortc1rcuit]

What's the normal output for that command?

[Rida Hamadani]

When successful, it outputs a success message: Completed successfully!.

[shortc1rcuit]

Ok that all seems to work

[shortc1rcuit]

So if it's not getting the cache I'm not sure what is wrong

[Michael Rothgang]

Does running lake exe cache get! make your build fast? (To be clear: this is a band-aid fix, not a real solution. I'd rather use that than have to manually rebuild everything, though.)

[shortc1rcuit]

It does not seem to no

[shortc1rcuit]

Actually it does

[shortc1rcuit]

In fact everything seems to be working.

[shortc1rcuit]

Not sure what fixed that

[shortc1rcuit]

But now getting the cache normally doesn't mean the builds take forever.

[shortc1rcuit]

Yay?

[shortc1rcuit]

Sorry to anyone in the future who came here thinking this would contain the solution

[Notification Bot]

shortc1rcuit has marked this topic as resolved.

[Notification Bot]

shortc1rcuit has marked this topic as unresolved.

[Johan Commelin]

@shortc1rcuit Probably some file in the cache was corrupted (e.g. by an interrupted download) and lake exe cache get! forcefully redownloaded the file, thereby fixing the problem.