Blueprint not compiling in repo despite passing CI

Stream: PrimeNumberTheorem+

[Terence Tao]

In the last few PRs, CI checks (including building the blueprint) have passed, but when the PR is merged, the building of the blueprint returns a bunch of warnings followed by the following technical-looking error:

✖ [7373/7373] Building PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:docs (8.8s)
info: Documentation indexing
trace: .> /home/runner/work/PrimeNumberTheoremAnd/PrimeNumberTheoremAnd/.lake/packages/doc-gen4/.lake/build/bin/doc-gen4 index --build /home/runner/work/PrimeNumberTheoremAnd/PrimeNumberTheoremAnd/docbuild/.lake/build
error: no such file or directory (error code: 2)
  file: /home/runner/work/PrimeNumberTheoremAnd/PrimeNumberTheoremAnd/docbuild/.lake/build/doc/references.bib
error: build failed
Some required targets logged failures:
- PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:docs

This does not seem to be a LaTeX issue but something to do with the repository file system perhaps? Is this something that will resolve itself, or does it need debugging?

[Alex Kontorovich]

Yes, I remember several occasions when CI built with a checkmark, but then when I merged, the build failed. Presumably this means I've set up CI in the wrong way? I'll ask @Pietro Monticone to help with this, too, when we meet tomorrow...

[Pietro Monticone]

No, the setup is fine. You’re not seeing docs-related issues on PR events simply because the relevant job step does not build the docs for pull requests for obvious time reasons.

[Pietro Monticone]

Oh, it's due to this recent change in docgen-action https://github.com/leanprover-community/docgen-action/pull/15.

Let me fix it.

[Pietro Monticone]

@Chris Henson Is this the intended behaviour?

[Pietro Monticone]

Fixed btw https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/actions/runs/20838759059/job/59868700298

[Chris Henson]

Not intentional, sorry! I'm not sure I understand exactly caused the error here. What I added to the action should just copy references.bib, if it exists, to the location docgen expects. Is there some logic I missed, maybe an interaction with the blueprint?

[Pietro Monticone]

What happens if there isn't any references.bib anywhere?

[Pietro Monticone]

The "fix" was to specify a path...

[Chris Henson]

There is a check in the action to see if the file exists, the intent is that nothing happens in this case.

[Pietro Monticone]

It doesn't seem to behave as expected, but I couldn't look into it carefully

[Chris Henson]

I'll look into it closer, sorry for the trouble!

[Pietro Monticone]

Thanks. No problem.