radar: interpreting build/profile/interpretation

Stream: lean4

[Thomas Murrills]

What exactly is the meaning of the wall-clock time for build/profile/interpretation, and more importantly, how strongly should we avoid increasing it? It seems to take about 3h wall-clock, but the radar run itself is still around 13 minutes—so, I'm guessing it's what you get by adding up all the interpreter time in parallel.

An initial version of a linter I'm working on increases this metric's wall-clock submetric by 11 minutes (7%). Adding 11 minutes to the aggregate build time in CI is completely unacceptable—but given that we're somehow fitting 3 hours within 13 minutes, how bad is this, actually? Roughly how bad should we expect it to be on an ordinary mathlib CI runner that takes closer to 1 hr to build all of mathlib instead of 13 minutes?

(I'm asking in part because I can imagine improving one part of the linter fairly easily, but another more boilerplate part of the linter still adds 6 minutes wall clock to interpretation, and I'm wondering if that's still way too much.)

[Joscha Mennicken]

The build/profile/* metrics come from lean --profile (as documented here) and are just the sum over all individual modules as you suspected.

[Thomas Murrills]

Okay, good to know! Though, I'm still wondering how to interpret the actual impact of this metric going up on other machines, which is the real focus of my question. Maybe this is more a mathlib issue, but I'm not sure what a reasonable increase here is for this particular metric, or whether the wall-clock would even translate faithfully to the less-powerful machines we run CI on due to reduced parallelism (even within modules, since linters are run as async tasks).

All in all, the total build wall-clock only goes up by 0.7%, not 7%, and I'm wondering if this factor roughly translates to other machines, modulo noise. Counting instructions instead is indeed more stable, but I think actual wall-clock times for CI machines is probably what we care about at the end of the day.

[Joscha Mennicken]

I think you can compare build/profile/interpretation//wall-clock with build//task-clock to get a rough estimate for how much of the total build time is spent interpreting, though they're measuring time slightly differently (and I don't know how big the difference between the two methods is).