lake is printing "build" lines even when oleans are present?

Stream: nightly-testing

[Kim Morrison]

lake appears to be printing "build" lines for some initial segment of files, even when all oleans are present.

See https://github.com/leanprover-community/mathlib4/actions/runs/8892841920/job/24421612621 as an example.

[Kim Morrison]

It's running fast, so I think it is successfully noticing and reusing the olean. Just printing unnecessarily. One doesn't notice this on the command line because the build lines are now being overwritten.

[Kim Morrison]

@Mac Malone, do you see what is going on?

[Ruben Van de Velde]

rss-bot said:

refactor: lake: --wfail & track jobs & logs & simplify build monads (lean4#3835)

This is a major refactor of Lake's build code. The key changes:

• Job Registration: Significant build jobs are now registered by
  build functions. The DSL inserts this registration automatically into
  user-defined targets and facets, so this change should require no
  end-user adaption. Registered jobs are incrementally awaited by the main
  build function and the progress counter now indicates how many of these
  jobs are completed and left-to-await. On the positive side, this means
  the counter is now always accurate. On the negative side, this means
  that jobs are displayed even if they are no-ops (i.e., if the target is
  already up-to-date).

Is this it? ^

[Kim Morrison]

Oh, yes. I didn't read that last sentence. Yes, that sounds pretty bad. It is going to be hell diagnosing people's cache problems.

[Kim Morrison]

I don't mind if those jobs are included in the total counter. I just don't want lines printed.