FLT docs missing mathlib declarations

Stream: FLT

[Thomas Browning]

I noticed that the FLT docs contain mathlib declarations (e.g., https://imperialcollegelondon.github.io/FLT/docs/Mathlib/Data/Nat/Prime/Infinite.html#Nat.exists_infinite_primes), but don't let you search for mathlib declarations (e.g., type "Nat.exists_infinite_primes" in the search box). Whereas this works fine on the sphere eversion project (e.g., type "Nat.exists_infinite_primes" in the search box here: https://leanprover-community.github.io/sphere-eversion/docs/). I think this is problematic if we want upstreamed theorems in the FLT blueprint to point to mathlib.

[Rémy Degenne]

Same issue in the Brownian motion project, although it's not consistent. Sometimes it suddenly works again after a commit, and then breaks again after a few more (but I haven't seen it work in a while).

[Henrik Böving]

We believe that this could be due to an issue with the way that doc-gen output is cached in CI. The search functionality is powered by declarations-data.bmp which is one of the outputs of doc-gen. I've unfortunately not yet been able to figure out what exactly is causing caching to fail here. The reason you are observing the issue only transiently is that at some point something will actually trigger the declaration-data to be rebuild properly and then everything works again.

[Kevin Buzzard]

(FWIW this is very low-priority for me personally: I never use the FLT docs at all, but obviously other people and other projects might well care about this)

[Kim Morrison]

I investigated this. The issue is in docgen-action's caching logic.

The cache saves doc/Mathlib/*.html etc, but not doc-data/*.bmp (per-module declaration data). When cache hits, Lake sees HTML exists and skips doc-gen4 single, so the .bmp files aren't regenerated. The index then only contains project-specific declarations.

The issue only appears transiently because dependency bumps change lake-manifest.json, which invalidates the cache key, triggering fresh builds that work correctly.

Fixed in https://github.com/leanprover-community/docgen-action/pull/17

[Ruben Van de Velde]

What were the two hardest problems in software engineering again? :sweat_smile: