MathlibDoc cache

Stream: mathlib4

[Sam van G]

At CIRM I managed to get CI for Lean blueprint to work, see here.
I just noticed that it fully re-builds Mathlib docs every time. For example, in this job, and all previous ones, there is an attempt to find a cache for the docs but it fails ... Does anyone know how to fix this?

[Sam van G]

Update: I just did
lake update
and
lake update -R -K doc=on
and
lake update -R -K env=dev doc-gen4
and copied Mathlib's lean-toolchain into the repo.
Now the CI build fails entirely already during the "Update docgen4" step...
So perhaps the above question is outdated, but then my question becomes: What did I do wrong when bumping mathlib? Any ideas on how to get the blueprint to build again?

[Utensil Song]

For failing entirely, probably you need to wait until https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20docs.20are.20broken is fixed. (The error in the log is the same.)

[Utensil Song]

An official Mathlib doc cache would be really nice, I spent little time rebuilding Mathlib thanks to olean cache, but quite some time rebuilding Mathlib doc (at least the part the formalization project depends on) since using lean4 blueprint which jumps to the doc generated by docgen4.

[Utensil Song]

Ah, the doc cache step in the CI was set up by me, but the cache will miss every Mathlib bump, that's expected.

[Utensil Song]

But I just recalled that it was designed to fall back to the previous Mathlib doc cache, and lake will pick up the outdated part and only rebuilds them. So a total cache miss is not expected as long as CI has built the doc recently and the cache hasn't been cleared by Github.

[Utensil Song]

Just noticed that your last build was a month ago.

GitHub will remove any cache entries that have not been accessed in over 7 days. https://docs.github.com/en/actions/using-workflows/caching-dependencies-to-speed-up-workflows

[Floris van Doorn]

I have noticed the same behavior in
https://github.com/fpvandoorn/BonnAnalysis/
and
https://github.com/fpvandoorn/carleson
even when the last few commits didn't change any Lean files, and even if the last few commits were hours/days ago.

[Floris van Doorn]

E.g. this run is from a commit from this morning:
https://github.com/fpvandoorn/BonnAnalysis/actions/runs/8931698445/job/24534250156

Run actions/cache@v3
  with:
    path: .lake/build/doc/Mathlib
    key: DocGen4-ebb92e4b5a3e8836555c5ce18c2b1ff5e08a6fd829e51a675df2f1966e798dfb
    restore-keys: DocGen4-

    enableCrossOsArchive: false
    fail-on-cache-miss: false
    lookup-only: false
Cache not found for input keys: DocGen4-ebb92e4b5a3e8836555c5ce18c2b1ff5e08a6fd829e51a675df2f1966e798dfb, DocGen4-

[Floris van Doorn]

and there were multiple commits yesterday that succesfully built the docs.

[Sam van G]

Utensil Song said:

For failing entirely, probably you need to wait until https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20docs.20are.20broken is fixed. (The error in the log is the same.)

Thanks, looks like I chose the wrong day to bump Mathlib, but I can wait

[Sam van G]

Utensil Song said:

Just noticed that your last build was a month ago.

GitHub will remove any cache entries that have not been accessed in over 7 days. https://docs.github.com/en/actions/using-workflows/caching-dependencies-to-speed-up-workflows

Ah! That explains at least this cache issue. Thank you.

[Utensil Song]

@Floris van Doorn For BonnAnalysis and carleson, the path to cache doesn't exist

[Utensil Song]

72D24EDA-D8EA-416C-A792-900F9036DFAD.jpg

[Utensil Song]

Because the CI has moved the doc for deployment but didn't put it back

[Utensil Song]

B4B9C39D-1523-4FF2-9C08-5872C8DC3DE8.jpg

My setup moved it back so it would be ok. Is your project generated by the new leanblueprint cli that Patrick wrote after last Christmas?

[Utensil Song]

https://github.com/PatrickMassot/leanblueprint/blob/master/leanblueprint/templates/blueprint.yml

The step is still there even though Patrick or someone also modified the workflow in one of the formalization projects changed it to cp, and mv is no longer necessary.

[Utensil Song]

BA8B09D4-33F3-4638-9A22-590313644F80.jpg

[Utensil Song]

Can you follow blueprint.yml to fix it? Sorry I'm on mobile for the next few days of vacation.

[Floris van Doorn]

Ok, thanks. That is very helpful, with this help I can fix it. Thanks!
I didn't use Patrick's leanblueprint command, but copied it from another repo, so it's my fault.