Lean Blueprint Compilation

Stream: general

[Vasily Ilin]

Why does the leanblueprint GH CI take 30+ minutes to build a single file? It seems to rebuild a large portion of Mathlib. Is there a way to tell it to just fetch cache, the way I would do locally, with lake exe cache get?
https://github.com/Vilin97/forward_euler/actions/runs/22011791786/job/63606964774

[Mac Malone]

In that CI run, the build of Mathlib is fetched. That is why the build & lint step only takes 4m20s. The reaosn the blueprint step takes so long is that it is building Mathlib docs (not the modules themselves). Unfortunately, there is no cache for this as far as I am aware. I am not familiar enough with blueprint to know if there are other ways to optimize its build.

[Vasily Ilin]

I don't actually need to build the mathlib docs since those are already published online. Would be nice to disable them, maybe even by default.

[Weiyi Wang]

I think you can disable the doc part using this option https://github.com/leanprover-community/docgen-action/blob/main/action.yml#L4

[Vasily Ilin]

But then I would not even get this page, would I? https://vilin97.github.io/forward_euler/docs/ForwardEuler/aristotle-1.html

[Weiyi Wang]

oh sorry, my bad. I misread it

[Weiyi Wang]

I don't think currently there is a way to build doc only for the part from your project

[Kevin Buzzard]

If you don't build mathlib docs then your own docs will be broken because they link to exactly the version of mathlib used by your project, which isn't cached anywhere.