Lake build progress numbers

Stream: lean4

[Anne Baanen]

(I'm sure this has been discussed before but my search-fu has failed me!)

What is the precise meaning of the numbers in the Lake progress line? For example:

[2478/4006] Building Mathlib.LinearAlgebra.QuotientPi

The second one seems to be the number of files that the build depends on (starting off lower until Lake has finished scanning all dependencies?)

For the first one I can't really offer an explanation: it increases but not strictly monotonically, so it's not quite the index into the compilation queue. Is it something like total dependencies - file dependencies?

[Yaël Dillies]

The second one is the number of discovered files that the build depends on. It's not quite all the files at the start because not all imports have been explored.

[Kevin Buzzard]

Here's Antoine asking here and me answering, and I think my answer was informed by the fact that I'd asked the same question at some earlier stage...

[Anne Baanen]

Aha, it doesn't increase strictly because it measures the number of completed builds, not scheduled builds. Thanks :D

[Kevin Buzzard]

Here's me asking the same question (after answering Antoine but when I realised I didn't know why the denominators were going up)

[Anne Baanen]

Actually I'm still not sure I understand the numbers correctly. For example:

error: stdout:
./././Mathlib/LinearAlgebra/LinearIndependent.lean:1065:2: error: simp made no progress
error: external command `/home/arch/arb/.elan/toolchains/mattrobball--lean4---redEta/bin/lean` exited with code 1
[2596/4006] Building Mathlib.LinearAlgebra.AffineSpace.Pointwise
[2596/4006] Building Mathlib.LinearAlgebra.AffineSpace.Restrict
[2596/4006] Building Mathlib.Analysis.Normed.Group.AddTorsor
[2596/4006] Building Mathlib.LinearAlgebra.AffineSpace.Combination
^C
$ vim Mathlib/LinearAlgebra/LinearIndependent.lean # Fix error
$ lake build
[1189/1566] Building Mathlib.LinearAlgebra.LinearIndependent
[1194/1585] Building Mathlib.Algebra.Star.NonUnitalSubalgebra
[1472/2210] Building Mathlib.LinearAlgebra.AffineSpace.Combination
[1911/3276] Building Mathlib.Topology.Algebra.Module.Basic
[2574/4006] Building Mathlib.CategoryTheory.Abelian.ProjectiveResolution

Why do we lose 25 built files in between? I thought dependencies of erroring files don't get built, so once everything is scanned we should have the same number again.

[Mauricio Collares]

I think discovering that a file exists in the dependency tree happens earlier than discovering it is already built (which only happens just when you're about to build it).

[Mauricio Collares]

So if you have X CPU cores and the first X scheduled builds correspond to files that need to be rebuilt, then the already-built files will need to wait their turn for the counter to find out they're in fact done.

[Patrick Massot]

The real question is: is there anything that could be printed here that wouldn't be utterly confusing?

[Eric Wieser]

Having separate discovery and build phases would reduce the confusion

[Mauricio Collares]

lake#169 is the relevant discussion

[Mauricio Collares]

The tl;dr is that a refactor is planned but doing it properly takes time, and I'm sure there are many other features competing for developer time.