CI inefficiency?

Stream: mathlib4

[Michael Stoll]

I've just added a space in a (almost) leaf file in a Mathlib PR. Looking at the build step in CI, as expected it only builds the file and the one file that imports it, together with Mathlib.lean. But then it seems to build a lot of Archive and Counterexamples and also many tests. Why is that? Unless there is an import Mathlib at the top of a file (which I don't think is the case), no rebuild should be necessary, as no dependency has changed. (The relevant material is so new that no downstream files in Archive/Counterexamples/Test uses it.)

(Caveat: there are currently problems with github that make all CI steps except building fail. But the cache from the previous build (before adding the space) should still be available.)

[Michael Rothgang]

If I remember correctly, CI only gets the cache from the base of the PR - not of intermediate PR commits (even if this cache was uploaded). @Bryan Gin-ge Chen mentioned changing this, at some point in the past.

[Michael Rothgang]

Working on new syntax linters occasionally makes me encounter the extreme version of this: modifying the linter naturally rebuilds all of mathlib (as the linter needs to check all files), but then a merge of master also rebuilds evefything - as opposed to just the new files.

[Bryan Gin-ge Chen]

The ping happened to remind me that I should get back to #33044. I guess that may be a different issue though?

[Michael Rothgang]

That issue (or perhaps some extension, also looking at intermediate commits) might be it!

[Michael Stoll]

A further data point: I just submitted a PR that only changes the name of a leaf file. The "build" step in CI still seems to build all the files in MathlibTest (but did not build anything in Archive or Counterexamples). Does this step not check whether the files depend on something that has changed?

[Michael Stoll]

Another thing I noticed is that every time CI runs, it seems to build all the tools from scratch. Would it be possible to make it use precompiled versions (as long as the PR does not change anything in the tooling)?