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)