lake exe cache getting from another project

Stream: mathlib4

[Tomaz Mascarenhas]

Hi,
I understand that if I clone mathlib and run lake exe cache get I will download all the library files and won't have to spend a lot of time compiling them. This works fine, but if I start a new project, add a dependency to mathlib and run lake exe cache get then it seems I still need to build mathlib. For instance, if I create a new blank project depending on mathlib with just this in Main.lean:

import Mathlib.Data.Real.Basic

#check Real

and run lake exe cache get and then lake build it builds all necessary files, instead of downloading them. Am I doing somehting wrong or is it expected?

[Aaron Liu]

if you're on VSCode you can fetch the imports for just the file you're looking at

[Tomaz Mascarenhas]

I see, thanks! But I am building a project that needs to be run through the command line...

[Ruben Van de Velde]

Tomaz Mascarenhas said:

Hi,
I understand that if I clone mathlib and run lake exe cache get I will download all the library files and don't have to spend a lot of time compiling them. This works fine, but if I start a new project, add a dependency to mathlib and run lake exe cache get then it seems I still need to build mathlib. For instance, if I create a new blank project depending on mathlib with just this in Main.lean:

import Mathlib.Data.Real.Basic

#check Real

and run lake exe cache get and then lake build it builds all necessary files, instead of downloading them. Am I doing somehting wrong or is it expected?

No, something unexpected is happening here. The cache should be sufficient that you don't need to compile the mathlib you depend on

[Kim Morrison]

Could you give us a commit of your project to look at, that demonstrates this issue?

[Tomaz Mascarenhas]

here: https://github.com/tomaz1502/cache-get-bug
after running lake update and lake exe cache get, lake build goes up to 7000 files instantaneously and then starts to compile another 7000 files

[Mauricio Collares]

Because your project produces an executable, Lean builds platform-dependent object files (compiled versions of computable functions you might want to use at runtime) for every Mathlib file. These build steps correspond to lines in the lake log starting with "Running" (previously "Compiling"), and are currently not cached. There was an earlier thread which mentioned core devs wanted to improve this situation, I will try to find it.

The platform-independent oleans (corresponding to lines in the log starting with "Building") are still reused, so the cache fetched with "lake exe cache get" is still useful.

[Tomaz Mascarenhas]

Oh, that makes sense! Thanks!

[Mauricio Collares]

Older relevant threads:
#mathlib4 > error building windows exe proj
#mathlib4 > mathlib cache works for lean_lib but not for lean_exe?