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.

[Filippo A. E. Nuccio]

I am extremely late to the game, but I think I'm experiencing the same issue at

https://faenuccio-teaching.github.io/M1_ENS_26/docs/

FWIW, even locally the search bar does not return anything contained in Mathlib (observe that I don't have anything besides Mathlib in that project!)

[Anne Baanen]

You are probably experiencing an issue with caching of declaration data. If you're using docgen-action, please update to the latest commit and let me know if that still happens!

[Filippo A. E. Nuccio]

I think I'm using the latest commit, but it is still not working: the search bar only finds definitions in Core & the like, nothing in Mathlib. I should also ask how to allow for some tweaking to the linters that are not allowed and that I had to comment

[Anne Baanen]

Hmm, if I look at your actions, it seems they conflict in how they are supposed to work: the docgen-action.yml "Build project and documentation" action that you ran manually doesn't actually update the docbuild folder in the way that pages.yml "Deploy website + docs" expects. So in docgen-action.yml you can re-add the "Commit generated docs" step that you used to have:

      - name: Commit generated docs
        run: |
          git config user.name "github-actions"
          git config user.email "github-actions@github.com"

          git add docbuild/.lake/build/doc
          git commit -m "Update Lean documentation" || echo "No changes to commit"
          git push

Or if you want the whole process to be automatic, you can use docgen-action to build and deploy the site as part of pages.yml. Since docgen-action can run the Jekyll build for you, the whole file should end up looking something like (untested):

name: Deploy website + docs

on:
  push:
    branches: ["master"]
  workflow_dispatch:

# Cancel previous runs if a new commit is pushed to the same PR or branch
concurrency:
  group: ${{ github.ref }}  # Group runs by the ref (branch or PR)
  cancel-in-progress: true  # Cancel any ongoing runs in the same group

permissions:
  contents: read
  pages: write
  id-token: write

jobs:
  deploy:
    runs-on: ubuntu-latest
    environment:
      name: github-pages

    steps:
      - uses: actions/checkout@v4

      - uses: leanprover-community/docgen-action@main
        with:
          homepage: "."

[Filippo A. E. Nuccio]

I tried to update things (modulo a small git tweak) here but I've got the feeling that nothing happens, it seems it compiles the whole mathlib doc in 3 mins (and at any rate the search field is still not working) :sad:

[Filippo A. E. Nuccio]

Any more ideas @Anne Baanen ? I still believe that something should be strange if the whole build takes 2 mins
https://github.com/faenuccio-teaching/M1_ENS_26/actions/runs/21676134354/job/62496898239
and indeed nothing about Mathlib is found from the search field.

[Anne Baanen]

Oh huh, apparently docgen-action does nothing if the action wasn't caused by a push event, and your workflow is being triggered manually instead. Not sure what I was thinking when I wrote that condition!

[Anne Baanen]

Are you able to run your workflow on the branch I just PR'd? https://github.com/faenuccio-teaching/M1_ENS_26/pull/1/

[Filippo A. E. Nuccio]

Tried, but it failed
https://github.com/faenuccio-teaching/M1_ENS_26/actions/runs/21680046737/job/62511537660

[Anne Baanen]

Huh. error: external command 'git' exited with code 128 has a lot of causes. Given the context, maybe it's just a temporary network failure?

[Filippo A. E. Nuccio]

Let me check in 10 mins

[Anne Baanen]

If you're okay with giving me access to your repository, I would also be happy to try and debug the setup myself. (Or is it better for this knowledge to spread by practice?)

[Filippo A. E. Nuccio]

Done!