Reuse mathlib compiled files in another project

Stream: new members

[Arshak Parsa]

I have a project called pr1, and it has lean and mathlib working correctly without any problem. Now, I want to create a new project (let's call it pr2), and I want to use mathlib in it. So, it seems like I have two options :

1) Just run lake build, and it downloads about 300mb and takes a lot of time to compile mathlib files (uses all of cpu cores!!)

2) Run lake exe cache get before lake build so it downloads cache files (I have not run this command, so I don't know how much it downloads)

So my question is, how can I use my pr1 mathlib files for pr2 ? instead of re-building or re-downloading mathlib again.

I have another question, Is there any way to build mathlib locally on gpu? because I have gtx gpu on my computer that has 700 cores in it and building mathlib uses all 4 cores of my cpu, so I think it would take less time if it could instead use my gpu to build it. (and I know , writing a code for gpu is much harder)

[Ruben Van de Velde]

You should use lake exe cache get

[Eric Wieser]

If your lakefile and lakemanifest versions of mathlib are identical between the two projects, then you could probably symlink pr2/.lake/packages/mathlib to pr1/.lake/packages/mathlib

[Arshak Parsa]

@Ruben Van de Velde Well, lake exe cache get tries to clone mathlib. I want to do it offline.

[Eric Wieser]

If you already have a cache from a previous download, you can use lake exe cache unpack