references.bib with docgen-action

Stream: general

[Chris Henson]

Does docgen-action support providing a references.bib file? I couldn't find any mention of this in the docs or code.

[Malvin Gattinger]

I think doc-gen4 itself has the hardcoded path docs/references.bib and does not need any additional arguments to pick it up, as long as it is in the right place. I recently got it working for my project as discussed here.

[Chris Henson]

Thanks, we'll try that!

[Chris Henson]

@Anne Baanen would a PR be welcome that adds an optional references input to the action? It would take a path and copy it to the appropriate location.

[Malvin Gattinger]

Wouldn't the "right" place to add such an option be a cli argument or config setting for doc-gen4 itself? Or why do you not want to put the file in docs/references.bib? Is it because you have other things (latex documents) using the file too?

(Part of my reasoning here is that I like to be able to build docs locally too, not only in github actions CI.)

[Chris Henson]

Yes it could be set higher up, I had just thought of configuration of the action as a good first step. Regardless of where it is set, it is undesirable for a user to need hardcoded paths from two tools (docbuild from the action, then docs/references.bib from from doc-gen4) to make this work.

I had hoped to eliminate having a directory for the docs at all in the repo and it just be made in CI, with references.bib copied over from the root of the repo. I don't like the maintenance of having an extra toolchain/manifest/lakefile. For our project (CSLib), I considered the tradeoff of needing to make that directory yourself to build docs locally acceptable.

[Malvin Gattinger]

Oh, that makes sense, I also often forgot to update stuff inside docbuild when updating to a newer lean, and it would be great if this could be autogenerated.

[Chris Henson]

Yeah I consider the action making the docs lakefile for you a big advantage. It seems in line that it should be able to (by whatever mechanism) do the equivalent for the references file.

[Anne Baanen]

I think this is a good idea, I am very much against hardcoding paths. Since the bibliography processing passes are being run from the docgen lakefile, it seems somewhat hard to modify this directly. So instead I think the right thing to do is for the action to copy a user-specified path to docbuild/docs/references.bib.

Would you like to open a PR implementing this?

[Henrik Böving]

There've been several requests to funnel options into doc-gen over the years but its still unclear to me how/if that's possible. @Mac Malone is there a recommended way to pass options into a facet?

[Chris Henson]

Anne Baanen said:

I think this is a good idea, I am very much against hardcoding paths. Since the bibliography processing passes are being run from the docgen lakefile, it seems somewhat hard to modify this directly. So instead I think the right thing to do is for the action to copy a user-specified path to docbuild/docs/references.bib.

Would you like to open a PR implementing this?

I have opened https://github.com/leanprover-community/docgen-action/pull/15 to do this.

[Chris Henson]

(While this is an improvement, I do agree that it would be nice if we could pass an option to the facet)

[Aayush Rajasekaran]

Small bug (I think) with the implementation of the references: https://github.com/leanprover-community/docgen-action/issues/18

[Aayush Rajasekaran]

And (hopefully) the fix https://github.com/leanprover-community/docgen-action/pull/19 cc @Chris Henson

[Bryan Gin-ge Chen]

The fix looks reasonable to me. I'll let @Anne Baanen take a look before merging though.

[Bryan Gin-ge Chen]

BTW, while we wait for Anne to have time to take a look, note that you should be able to test the fix out by changing the workflow file that uses docgen-action to point to leanprover-community/docgen-action@b1386934261c959c460288378384ce7ade57298e (the commit from your PR).

[Christian Merten]

On my proetale repository the docgen-action CI is failing with the following error message:

info: Documentation indexing
trace: .> /home/runner/work/proetale/proetale/.lake/packages/doc-gen4/.lake/build/bin/doc-gen4 index --build /home/runner/work/proetale/proetale/docbuild/.lake/build
error: no such file or directory (error code: 2)
  file: /home/runner/work/proetale/proetale/docbuild/.lake/build/doc/references.bib
error: build failed
Some required targets logged failures:
- proetale/Proetale:docs

(full log).
I have tried to add an empty references.bib, which temporarily gave a green check (see the run https://github.com/chrisflav/proetale/actions/runs/21187436972/job/60945688230), but on the next commit it started failing again.
Could this be related to the changes discussed in this thread?

[Jireh Loreaux]

This has been discussed elsewhere, but there is currently a bug in docgen-action. The temporary fix is to downgrade to a commit from October.

leanprover-community/docgen-action@deed0cdc44dd8e5de07a300773eb751d33e32fc8 # 2025-10-26

Is the one I have in my GitHub workflow now and it succeeds.

[Anne Baanen]

I was not aware that this is a bug with docgen-action! Not sure exactly what is going on here, though, based on the log line it is happening outside of any code that docgen-action added...

[Pietro Monticone]

Yes, I've encountered the same issue in PNT+, FLT, etc. (e.g. see #PrimeNumberTheorem+ > CI issues @ 💬)

[Kim Morrison]

https://github.com/leanprover/doc-gen4/pull/354

[Aayush Rajasekaran]

I think we also need to have docgen-action actually cache references -- opened a PR here.