Unwanted Mathlib recompilation after adding as a dependency

Stream: lean4

[Mirek Olšák]

I have recently noticed a surprising "double mathlib compilation" in some cases. Steps to reproduce:

$ mkdir some-project
$ cd some-project
$ lake init

then add

[[require]]
name = "mathlib"
scope = "leanprover-community"

into lakefile.toml (before lean-lib), run

$ lake update

Then this is fine

$ lake build
Build completed successfully (8 jobs).

But if we change SomeProject/Basic.lean to

import Mathlib
def hello := "world"

then

$ lake lean SomeProject.lean
⣽ [8015/8016] Running SomeProject.Basic (+ 0 more)

is still quick, however

$ lake build
⣟ [8059/16020] Running Batteries.Control.Nondet.Basic:c.o (+ 7 more)

starts compiling a double of Mathlib, or how I should interpret the number 16020.

What happened? Is it a bug? Am I doing something fundamentally wrong?

[Notification Bot]

This topic was moved here from #lean4 > Recompiling Mathlib after adding as a dependency by Mirek Olšák.

[Jon Eugster]

That's often the case if your project has some exe (e.g. a Main.lean) floating around which some of the default projects create by lake do. Simply delete the executable from the lakefile if you don't need it or make sure it does not import Mathlib

[Mirek Olšák]

Ah, I see makes sense.