mathlib docs cache fails after upgrade to Lean v4.29.0

[dwrensha]

When we upgraded from Lean v4.28.0 to Lean v4.29.0 on the Noperthedron Project, CI builds started always rebuilding all of the mathlib docs, even when there was a cache hit. This meant more than 2 hours per CI run.

@jcreedcmu hypothesized that the problem could be related to this change in doc-gen4, which added new kinds of generated files. We tried applying this change to docgen-action, but it did not seem to help.

[david-christiansen]

I would generally expect that caching the doc-data directory and the DB were enough to keep docInfo facets from rebuilding.

I've definitely had success caching the entire .lake directory to avoid doc rebuilds. So I'm thinking that it's plausible that the .olean files are part of the trace, and that you not having them is keeping the cache from working. I'll see if things still work right if I take them out of the trace.

[acmepjz]

CI builds started always rebuilding all of the mathlib docs, even when there was a cache hit. This meant more than 2 hours per CI run.

Same problems here, what's worse, it complains about file not found error https://github.com/acmepjz/lean-iwasawa/actions/runs/24180129247

[marcelolynch]

Please note this subtlety about the GitHub action cache: if the path parameter changes, even if the key is the same, it will be a cache miss: see [1], [2]. So changing to these different versions of the action which are changing that parameter will result in a cache miss on the first run, no matter what.

[david-christiansen]

Interesting. I went in to the older versions, and in them, the docs also depended on the oleans, so this isn't new behavior. I'm a bit leery about adding this hack until we investigate a bit more.

@dwrensha - have you run it twice, in case it's the issue that @marcelolynch mentioned? And it looks like the action is also missing .lake/build/doc-manifest.json, which I suspect is causing @acmepjz's "file not found".

[dwrensha]

I was seeing a cache hit, but the docs were rebuilt on the actions runner anyway.

I'll try again today, in case anything has changed since then. It takes 2.5 hours for the full docs reload, so it will take a while before I have results.

[acmepjz]

In my project (https://github.com/acmepjz/lean-iwasawa/actions), a doc build without cache takes 2h30m, while a doc build with cache takes 1h50m. So it did cached something, but it didn't help much.

[marcelolynch]

FWIW, I saw cache hits in @dwrensha's builds after that first one he shared, my remark was just in general (and because David said "it did not seem to help" regarding that first build after switching the action)

[dwrensha]

Before updating to Lean v4.29.0, a typical build took under 20 minutes, including docs generation (taking advantage of cached Mathlib docs).

In my experiments today, starting with a clear docs cache, this is what has happened:

1. On jcreedcmu/Noperthedron@e0a714f, this action ran in 100 minutes and successfully built and published the docs.
2. On jcreedcmu/Noperthedron@2c095c3, this action ran in 80 minutes (with a docs cache hit) and errored with

error: no such file or directory (error code: 4294967294)
  file: /home/runner/work/Noperthedron/Noperthedron/docbuild/.lake/build/doc/style.css

I then re-purged the cache before the following events.

3. On jcreedcmu/Noperthedron@0656bc2, which updated the doc-gen action version to 7b5b9a1, this action ran in 118 minutes and successfully built and published the docs.
4. On jcreedcmu/Noperthedron@534a276, this action ran in 75 minutes (with a docs cache hit) and published the docs, but all of the project-specific doc pages gave a 404.
5. On jcreedcmu/Noperthedron@4a87754, this action had a docs cache hit, but is once again rebuilding mathlib docs. As of this writing it has not finished, but I expect it to take approximately 75 minutes again.

[dwrensha]

I believe the reason these times are less than my earlier estimate of 2.5 hours is that I recently removed an import of Mathlib.Tactic, which was causing docs to get built for a bunch of Mathlib that's actually irrelevant to this project.