Blueprint Lean links 404'ed

Stream: Carleson

[Terence Tao]

Just a heads up: the links to lean code in the blueprint (either from the dependency graph or the latex) are 404'ed for some reason: e.g., to pick something at random, the Lean link from https://florisvandoorn.com/carleson/blueprint/sect0003.html#Dirichlet-kernel points to https://fpvandoorn.github.io/carleson/docs/find/#doc/dirichletKernel_eq and https://fpvandoorn.github.io/carleson/docs/find/#doc/partialFourierSum_eq_conv_dirichletKernel which both return a 404 message (instead of resolving to (presumably) https://florisvandoorn.com/carleson/docs/Carleson/Classical/DirichletKernel.html#dirichletKernel_eq and https://florisvandoorn.com/carleson/docs/Carleson/Classical/DirichletKernel.html#partialFourierSum_eq_conv_dirichletKernel respectively). Presumably it's some misconfiguration of the "find" URL...

EDIT: strangely, some links still work. For instance https://florisvandoorn.com/carleson/blueprint/sect0003.html#real-Carleson points to https://fpvandoorn.github.io/carleson/docs/find/#doc/rcarleson which correctly resolves to https://florisvandoorn.com/carleson/docs/Carleson/Classical/CarlesonOnTheRealLine.html#rcarleson . Not sure what is going on. Maybe some of the docs files are not being indexed?

[Yaël Dillies]

Indeed, dirichletKernel_eq doesn't appear in the Carleson docs. Why this is, I have no idea... Well I had several ideas, but none of them turned out to be correct

[Yaël Dillies]

• dirichletKernel_eq is in the root namespace, so it's not a namespace issue.
• dirichletKernel_eq is in Carleson.Classical.DirichletKernel which is imported by Carleson, so it is not an import issue.
• The docs are invalidated whenever the lake manifest changes: https://github.com/fpvandoorn/carleson/blob/e39ecc926ec5159e20af1716d7bcbdda08aa9523/.github/workflows/push.yml#L63. So it is not a caching issue.
• Recent commits to Carleson did indeed trigger CI, so it's not a disabled CI issue.

[Pietro Monticone]

Let me try the usual thing of cleaning up the cache and rerun the latest job. https://github.com/fpvandoorn/carleson/actions/runs/14796902479/job/41589985214

Let’s wait an hour or so…

[Pietro Monticone]

Now it's fixed. Thanks for the report and sorry for the inconvenience.

[Yaël Dillies]

The ways of CI... :smile:

[Floris van Doorn]

The cache seems to regularly break. I've also cleared the cache & restarted the latest job a few times myself. If someone wants to investigate how this can be solved more robustly, that would be very helpful!

(Do other projects, like FLT/LeanCamCombi have the same issue?)

[Pietro Monticone]

I can do it later today or in the next few days. I have some idea about how to fix this.

[Terence Tao]

Floris van Doorn said:

(Do other projects, like FLT/LeanCamCombi have the same issue?)

I have found a possibly related issue with Moogle. If I search for, say, commutative group,

https://moogle-morphlabs.vercel.app/search/raw?q=commutative%20group

the first hit (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Defs.html#CommGroup) resolves correctly, but the second hit (https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Subgroup/Basic.html#Subgroup.IsCommutative.commGroup) leads to a 404. Here though the "find" function is not being directly used, so this could be a more moogle-specific issue.

[Yaël Dillies]

Floris van Doorn said:

Do other projects, like FLT/LeanCamCombi have the same issue?

I never noticed it breaking, but I rarely use the docs of my project (because they are not too big and I know them by heart)

[Floris van Doorn]

@Terence Tao I think that is unrelated, and caused by the fact that Moogle uses a very old version of Mathlib, and the file where this result was has been moved. I recommend using https://leansearch.net/ instead of Moogle for natural language search of Mathlib.

[Pietro Monticone]

I believe that caching only the relevant subdirectories of docbuild/.lake/build/doc, rather than the entire path, combined with a cache key that accurately reflects the inputs affecting the documentation, should be sufficient to avoid this stale cache issue.

I tend to believe that this issue is simply due to a combination of too broad doc caching and excessively permissive cache restore-key, which allows outdated artifacts to be reused.

I’ll open a PR when I am back at my PC.

[Pietro Monticone]

Maybe we should completely avoid using restore-keys when caching API docs because it can restore outdated or mismatched artifacts from previous builds. Since the doc output depends closely on the current lean_decls, a partially matching cache can easily lead to problems like missing pages or broken links without triggering a rebuild. Using an exact cache key ensures that the documentation is only reused when it is guaranteed to be valid for the current state of the project.

[Pietro Monticone]

In short, I think we should cache only those files whose contents are fully determined by the key parameters.

[Floris van Doorn]

I agree. I didn't actually realize that we were caching docs from the Carleson project. I think most of the gains from caching are from caching Mathlib docs, and I think Carleson is small enough to rebuild that from scratch each time.

[Floris van Doorn]

Thanks for looking into this!

[Pietro Monticone]

Done https://github.com/fpvandoorn/carleson/pull/328

[Pietro Monticone]

@Patrick Massot I’ve just opened a PR upstreaming the fix to LeanBlueprint so it applies for all future projects using the template.

[Pietro Monticone]

I also recommend avoiding exclusion patterns in actions/cache unless the excluded paths are at the same directory depth as the included ones since deeper exclusions are unreliable due to limitations in the underlying globbing behavior (see this issue for more details).

[Kevin Buzzard]

Similarly I never really use the FLT docs; I just tried some random links and some worked and some didn't, although this might be incompetence on my part.

[Pietro Monticone]

Fixed in FLT too (FLT#469).

[Patrick Massot]

Thanks Pietro. @Floris van Doorn and @Kevin Buzzard, could you confirm this patch fixes the issue for you?

[Floris van Doorn]

I don't know how to test that, other than waiting for a commit changing a bunch of lemmas, and then searching for random things in the docs. All the links in Terry's original message work again, but that might be just because of the clearing of the cache + rerun.

[Pietro Monticone]

In theory, given how actions/cache is supposed to work, I believe this conservative change should resolve the issue.

To “test” (narrowly enough) this in practice, I could:

1. Open a dedicated PR branch which will not be merged.
2. Introduce minor modifications to certain declaration names.
3. Enable the website deployment for pull_request events as well.
4. Check whether the resulting documentation reflects those name changes accordingly using links in the blueprint HTML.

I could perform this “test” on both the FLT and Carleson repos, although FLT currently offers a slightly more convenient setup since it uses a single workflow file in which the event conditions can be easily commented out.

[Pietro Monticone]

I have just run the "test" mentioned above on FLT, more precisely:

1. FLT#470
2. GLn.IsSmooth to GLn.IsSmooth' and GLn.IsSlowlyIncreasing to GLn.IsSlowlyIncreasing'.
3. FLT#470-diff
4. GLn.IsSmooth' (https://imperialcollegelondon.github.io/FLT/blueprint/sect0004.html#AutomorphicForm.GLn.IsSmooth' and https://imperialcollegelondon.github.io/FLT/docs/find/#doc/AutomorphicForm.GLn.IsSmooth') and GLn.IsSlowlyIncreasing' (https://imperialcollegelondon.github.io/FLT/blueprint/sect0004.html#AutomorphicForm.GLn.IsSlowlyIncreasing' and https://imperialcollegelondon.github.io/FLT/docs/find/#doc/AutomorphicForm.GLn.IsSlowlyIncreasing')

Results:
:check: The cache has been restored successfully (see here).
:check: Step 4. above has worked as expected.

[Kevin Buzzard]

Thanks as ever Pietro for keeping the show on the road!

[Patrick Massot]

Ok, this is good enough to merge. Thanks!