feat: add bibliography support

leanprover / doc-gen4

Document Generator for Lean 4

Apache License 2.0

62 stars 41 forks source link

feat: add bibliography support #209

Closed acmepjz closed 1 month ago

acmepjz commented 1 month ago

This PR adds bibliography support to doc-gen4. It includes:

DocGen4/Output/References.lean which contains generic function support for bibliography. It is independent of the actual implementation of bib file formatting.
DocGen4/Output/Bibtex.lean which contains an implementation of bib file formatting by calling external Lean library BibtexQuery.
Changes in DocGen4/Output/DocString.lean which analyzes citations in markdown text, inserting and modifying citation links, and collect back references.
Changes in various output files to add back references collecting feature.
Add a subcommand bibPrepass and change the build file accordingly.

This PR has all commit history squashed. To see more history, see the previous obsolete PR #200 which also includes an optional bibtex parser by calling external program pybtex.

Closes #147.

acmepjz commented 1 month ago

Please verify that your branch actually works on mathlib.

Ah, sorry for that. I forgot I have slightly local modifications for the test file. Specifically, \url and \_ are the commands in that which are not supported by current parser.

For the \url support an upgrade to the parser is necessary; I'll work on it later. Meanwhile I think it's better to use the standard url field of the bib file.
For the \_ it can be added quickly to BibtexQuery (for a proper fix it's best to upgrade to the parser). But In my opinion it's inappropriate to use this command in the url and doi field. In some other entries, there are also _ but which are not escaped.

I'll open a PR to mathlib (https://github.com/leanprover-community/mathlib4/pull/14689). What's your opinion?

acmepjz commented 1 month ago

I hope that we can add collecting subproject references.bib in the future?

I think it's possible, but I think this needs to be done mostly in build script. The build script collects all paths of bib files, feed them to the doc-gen4. I'm not familiar with that part.

acmepjz commented 1 month ago

The PR on mathlib was merged, so the current code should work on mathlib again. Meanwhile I'll submit a PR to BibtexQuery to refactor the TeX command processing. This will take some days. Do you think it's good to merge the current code to doc-gen4?

hargoniX commented 1 month ago

Verified to work with mathlib, will take a little change to mathlib4_docs CI to actually deploy.