Generating an olean cache locally

Stream: general

[Frédéric Dupuis]

Does anyone know if it's possible to generate an olean cache locally? I would like to be able to generate the tar.gz file that leanproject get-cache downloads from github without having to wait for CI. leanproject mk-cache looks like it should be able to do this, but if so I have no idea where the file ends up. Any ideas?

[Eric Wieser]

Is this for mathlib itself or for another project depending on mathlib?

[Eric Wieser]

mk-cache is the right tool for the job; in the former case the file ends up in ~/.mathlib, in the latter case in :/_cache.

[Frédéric Dupuis]

This is for mathlib itself. Somehow mk-cache didn't do this when I tried it. I'll try again next time I compile locally.

[Eric Wieser]

I think it's just very slow

[Frédéric Dupuis]

Well, the command took a few seconds to complete, but then later when I tried to use leanproject get-cache to restore those oleans, it failed to find them.

[Eric Wieser]

Did you make any commits in between?

[Frédéric Dupuis]

No! It must have been some kind of error on my part -- I'll just try it again next time I'm done compiling something locally.

[Frédéric Dupuis]

Now I see the problem: I have a version of leanproject that generates a tar.bz2 version of the cache but where get-cache only looks for a tar.xz file.

[Eric Wieser]

I assume it was an old version, and the latest release is fine?