Mathlib4 - check that caching works

Stream: new members

[Jonas Bayer]

Hi everyone!

I just started a Lean4 project that uses Mathlib4 as a dependency and I'm happy to have managed to set everything up so that it generally works. However, build times seem to be very long and I'm not sure that the caching has worked.

When I run lake exe cache getthe cache gets downloaded, I can see the progress in the terminal and afterwards there are files in the .cache folder. I then run lake build and assume that this starts the building process in the background. Is it possible to view the progress of building? Can one also abort the build process?

How long should it take to build mathlib4 on an average personal computer with/without cache files?

[Ruben Van de Velde]

lake build should have a line of output for every file

[Jonas Bayer]

Thanks for this answer. I think I might have not fully understood then what lake buildis meant to do when employed as in the mathlib readme instructions. Does it build my own project or does it build mathlib4 itself? Does the build include all .lean files or only those mentioned in lakefile.lean?

Currently, I'm writing code that imports files from Mathlib.Data. My principal concern for the moment is that every time I add new imports it takes very long before I can start working (e.g. this morning I wanted to use matrices and looked at "Loading messages" for 30 minutes).

[Ruben Van de Velde]

I cargo-culted a ProjectName.lean in the root of the repository that imports all other files from mathlib - not sure if that's a strict requirement

[Ruben Van de Velde]

After making a change, the output looks like this:

$ lake exe cache get && lake build
No files to download
Decompressing 1882 file(s)
Building Flt.Primes
Building Flt.Spts
Building Flt.Edwards
Building Flt.Euler
Building Flt

[Kevin Buzzard]

My understanding is that lake in project X only knows about files in X.lean.

If it's any help, I haven't updated mathlib4 in about a week or so, and I'm on a pretty slow internet connection right now. After a git pull (which took a while because of internet), lake exe cache get took 2 minutes 42 seconds of real time to run, and after that lake build did this:

$ time lake build
Building Mathlib.Algebra.Algebra.Subalgebra.Basic

real    0m27.650s
user    0m28.482s
sys     0m1.516s
$

[Jonas Bayer]

Yes, this is absolutely helpful, thanks Kevin Buzzard and Ruben Van de Velde . I ran lake build Mathlib yesterday which hadn't even finished after two hours. So there definitely must be an issue with the caching on my side. I made sure that the lean versions coincide and also checked my curl version which is higher than 7.69.

Do you know of anything else that I could I do to troubleshoot?

[Eric Wieser]

lake exe cache get often does not work properly if you are using lean elsewhere at the same time.

[Eric Wieser]

(notably including having a lean file open in vscode)

[Jonas Bayer]

Thanks for this hint @Eric Wieser, I'll have a try. For now I've always been running lake from the vscode terminal so there is a very high chance that a different file was open.

Perhaps this hint could also be mentioned in the the Mathlib4 readme instructions (I could also add it myself but have never contributed to mathlib4 and don't know the policy around these things)

[Ruben Van de Velde]

If you haven't yet, check if the quote4/std4/aesop hashes in lake-manifest.json match the ones in your mathlib version?

[Jonas Bayer]

I just checked and the hashes in my project's lake-manifest.json are the same as in lake-packages/mathlib/lake-manifest.json