CI build builds all of mathlib

Stream: general

[Shreyas Srinivas]

Currently I understand that on a math project, lake build will only build that part of mathlib which is directly in the dependency of the project. But on the CI (at least in lean blueprint), the entirety of mathlib and mathlib docs seems to be getting built. Is there a way to restrict CI to build binaries and docs just for the dependency tree?

[Notification Bot]

This topic was moved here from #lean4 > CI build builds all of mathlib by Eric Wieser.

[Eric Wieser]

This sounds like a question about a particular CI setup, which is hard to answer without seeing that setup. Can you link to a job where this happens?

[Shreyas Srinivas]

It’s the default lean blueprint setup. We had the same thing happen in equational theories.

[Jireh Loreaux]

Some things that CI tests are global though. So only testing on the pieces that need to be rebuilt does not mean everything is fine. The canonical example is the simpNF linter.

[Eric Wieser]

@Shreyas Srinivas, please link to the actual job doing the "building all of mathlib"

[Shreyas Srinivas]

This one my friend set up just now : https://github.com/Shreyas4991/DGAlgorithms/actions/runs/13923235440/job/38961202690

[Shreyas Srinivas]

This one : https://github.com/teorth/equational_theories/actions/runs/13884571087/job/38847545038

[Shreyas Srinivas]

In all cases, mathlib is "built" by fetching the entire cache.

[Shreyas Srinivas]

And the docs are built for all of mathlib.

[Shreyas Srinivas]

In the second one, I am specifically looking at this line : https://github.com/teorth/equational_theories/actions/runs/13884571087/job/38847545038#step:9:1

[Eric Wieser]

So this is separate questions of:

• "how can I fetch less with lake exe cache get" (answer: there is a PR in the works for this)
• "how can I build docs for less than all of mathlib" (answer: probably something to do with how you are asking the docs to be generated in your CI)

[Ruben Van de Velde]

I'm not sure I've seen a solution for (2) yet. Maybe @Yaël Dillies knows

[Yaël Dillies]

Yeah, it's easy: don't import Mathlib, doc-gen already knows not to generate documentation for files that aren't imported

[Ruben Van de Velde]

Okay, but I was thinking more about reusing the docs that mathlib already builds rather than having fewer docs - though that also helps

[Yaël Dillies]

Oh, that's theoretically possible, but the docs are currently not cached anywhere. It's also unclear to me that all the mathlib commits your project could depend on have ever had docs built for them (because docs are only built for the head commits)

[Ruben Van de Velde]

Yeah, there's that (and on a timer, too)