doc-gen not finding Mathlib declarations

Stream: general

[Patrick Massot]

@Henrik Böving do you understand why searching for CategoryTheory.LaxMonoidalFunctor on https://emilyriehl.github.io/infinity-cosmos/docs finds nothing despite the existence of https://emilyriehl.github.io/infinity-cosmos/docs/Mathlib/CategoryTheory/Monoidal/Functor.html#CategoryTheory.LaxMonoidalFunctor? It looks like the index does not contain Mathlib stuff.

[Patrick Massot]

Note this is the documentation of a project depending on Mathlib, and this declaration is in Mathlib.

[Henrik Böving]

Not obvious to me at first glance no

[Yaël Dillies]

Does lake build in your project build CategoryTheory.LaxMonoidalFunctor?

[Henrik Böving]

I'll think about it

[Yaël Dillies]

doc-gen only builds the files that are imported by your library

[Henrik Böving]

Yaël Dillies said:

Does lake build in your project build CategoryTheory.LaxMonoidalFunctor?

Well yes otherwise the docs page wouldn't exist

[Yaël Dillies]

Oh sorry, I misread the second link

[Yaël Dillies]

Ah yeah, so I have noticed the same bug in APAP. It's unclear to me where it comes from

[Patrick Massot]

It would be nice to understand this because it causes issues for blueprints which refer to Mathlib declarations.

[Pietro Monticone]

Very interested to know the answer to this one!

It would be crucial to allow Mathlib declarations in blueprint dependency graphs. The workaround for me has always been to have a local Project/Mathlib folder but it's very far from convenient.

[Henrik Böving]

I'm a bit surprised this happens at all given that it just works for mathlibs own deps

[Henrik Böving]

Okay I can give a few insights into this. I tried to just build the docs locally and I noticed :

1. The important one: Everything just works when built locally, I can lookup LaxMonoidalFunctor and Quiver and whatever else in the search bar and it finds things, so this is not doc-gen's fault, it is the fault of whatever it is that is talking to doc-gen.
2. If you check the declaration data storage in the javascript in the browser for the hosted version you can indeed observer that the mathlib parts are missing. That means that when this command is run in your build: https://github.com/leanprover/doc-gen4/blob/main/lakefile.lean#L223 this code here: https://github.com/leanprover/doc-gen4/blob/1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0/DocGen4/Output.lean#L139-L157 does not find the mathlib declaration-data files anymore and thus fails to index them. Why they are not there I cannot tell you as they are evidently president when just building locally. I know that blueprint does some caching for doc builds? My conjecture for this would be that you are not caching enough.
3. I did observe one notable thing which is that in InfinityCosmos.ForMathlib.AlgebraicTopology.HomotopyCat there seem to exist 5 declarations that trip doc-gen up to the point where it panics, congrats, nobody has managed to produce a Lean file that does this in a long time^^ I'll fix that but it is evidently not at fault here as the code is still working

[Henrik Böving]

Okay the panic is because you are doing something that I thought is impossible. This code here:
https://github.com/emilyriehl/infinity-cosmos/blob/main/InfinityCosmos/ForMathlib/AlgebraicTopology/HomotopyCat.lean#L430C48-L430C61

instance Δ.ι.op.fullyFaithful (k) : (Δ.ι k).op.FullyFaithful :=
  FullyFaithful.ofFullyFaithful (ι k).op

declares an instance of FullyFaithful but FullyFaithful is a structure not a class: https://github.com/leanprover-community/mathlib4/blob/4da4503a07ff4172bedf40581927cd691573d512/Mathlib/CategoryTheory/Functor/FullyFaithful.lean#L121-L125. I had thought that Lean would reject such an instance outright. @Sebastian Ullrich is this a bug or intended?

[Patrick Massot]

Henrik Böving said:

Okay I can give a few insights into this. I tried to just build the docs locally and I noticed :

1. The important one: Everything just works, I can lookup LaxMonoidalFunctor and Quiver and whatever else in the search bar and it finds things, so this is not doc-gen's fault, it is the fault of whatever it is that is talking to doc-gen.

Really? On https://emilyriehl.github.io/infinity-cosmos/docs/? It certainly doesn’t work here.

[Henrik Böving]

Yes check 2.

[Jireh Loreaux]

Patrick, I think you missed the key phrase before Henrik's (1): "... build the docs locally ..."

[Patrick Massot]

Oh I’m sorry, I read too quickly.

[Pietro Monticone]

Fixed it by caching .lake/build/doc/declarations/declaration-data-InfinityCosmos*.

[Utensil Song]

Coming from PatrickMassot/leanblueprint#47 where Patrick asked if there was a motivation for the line

!.lake/build/doc/declarations/declaration-data-{| lib_name |}*

I can recall that the motivation was to only cache the declaration data for Mathlib and its deps, but rebuild for the project itself every time to prevent stale cache, because rebuilding Mathlib docs is time-consuming and not worth it if Mathlib is not bumped, but the project itself is relatively small, and it's more important to ensure it's up-to-date without cache hassles.

I don't know how it ends up causing this issue.

[Patrick Massot]

Thanks Utensil. So I am still confused by this issue. I’d like to merge a fix that both actually fixes the issue and is explainable. I am afraid that the fixing effect that Pietro is observing may be random and not reproducible.

[Pietro Monticone]

The reason behind the change I made was primarily based on point 2 of @Henrik Böving’s comment here.

[Patrick Massot]

The link does not seem to work.

[Pietro Monticone]

Henrik Böving said:

Okay I can give a few insights into this. I tried to just build the docs locally and I noticed :

1. The important one: Everything just works when built locally, I can lookup LaxMonoidalFunctor and Quiver and whatever else in the search bar and it finds things, so this is not doc-gen's fault, it is the fault of whatever it is that is talking to doc-gen.
2. If you check the declaration data storage in the javascript in the browser for the hosted version you can indeed observer that the mathlib parts are missing. That means that when this command is run in your build: https://github.com/leanprover/doc-gen4/blob/main/lakefile.lean#L223 this code here: https://github.com/leanprover/doc-gen4/blob/1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0/DocGen4/Output.lean#L139-L157 does not find the mathlib declaration-data files anymore and thus fails to index them. Why they are not there I cannot tell you as they are evidently president when just building locally. I know that blueprint does some caching for doc builds? My conjecture for this would be that you are not caching enough.
3. I did observe one notable thing which is that in InfinityCosmos.ForMathlib.AlgebraicTopology.HomotopyCat there seem to exist 5 declarations that trip doc-gen up to the point where it panics, congrats, nobody has managed to produce a Lean file that does this in a long time^^ I'll fix that but it is evidently not at fault here as the code is still working

Here.

[Utensil Song]

I'm baffled by how could having a cached declaration data for InfinityCosmos* would help to solve the issue of declaration data of Mathlib.

[Henrik Böving]

(I agree)

[Patrick Massot]

Yes, this is precisely why I’m asking.