lake exe cache get hits, but mathlib files are still built

Stream: lean4

[Joachim Breitner]

I have created a new project that uses mathlib (at https://github.com/nomeata/loogle), and carefully made sure to use the same toolchain version and std4 and aesop revision as mathlib. This way, lake exe cache get hits and downloads >3000 files. But when I lake build, it still builds the modules from std4 and mathlib that are used by my executable (e.g. Mathlib.Tactic.ToExpr). Is that expected? Is it maybe because I use extern_lib in my project?

The repo above should reproduce it, if you have nix (to get the C library it uses), with

lake clean ; lake update; lake exe cache get; lake build

[Mauricio Collares]

Does it say Building or Compiling?

[Mauricio Collares]

Compiling is expected, Building isn't

[Joachim Breitner]

Compiling indeed! Thanks for bearing with my ignorance. Kinda makes sense :-)

[Mauricio Collares]

I think Compiling is for platform-dependent output (i.e. it runs leanc)