feat: add bibliography support #209
Conversation
There was a problem hiding this comment.
Okay this looks good to me now apart from the one nitpick. I'll verify myself that this works on mathlib and then merge this.
Note that because this does not collect references.bib of subprojects this won't work in the mathlib4_docs CI without changes, I'll add a temporary hack to make this work out but I hope that we can add collecting subproject references.bib in the future?
There was a problem hiding this comment.
Running this on mathlib almost instantly throws:
info: stderr:
uncaught exception: failed to run texDiacritics on '\url{https://leanprover.github.io/theorem_proving_in_lean/}' at pos 4: unsupported command: '\url'
error: external command './././../doc-gen4/.lake/build/bin/doc-gen4' exited with code 1
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,
I'll open a PR to mathlib (leanprover-community/mathlib4#14689). What's your opinion? |
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. |
This PR removes `\url` and `\_` commands in `references.bib`. The existence of them breaks leanprover/doc-gen4#209. - The first is `howpublished = {\url{...}}`. I think it's better to use the standard `url` field. Meanwhile `howpublished` field is preserved since some bibtex parser complains about missing that field. - There are some `\_` in `url` and `doi` fields. I think it's better to replace them with `_`; there are already some `_` in `url` and `doi` fields of other bibitems. - There is `$K\_X$`, but which, after checking the original article, should be `$K_X$`.
|
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? |
|
Verified to work with mathlib, will take a little change to mathlib4_docs CI to actually deploy. |
This PR adds bibliography support to doc-gen4. It includes:
DocGen4/Output/References.leanwhich contains generic function support for bibliography. It is independent of the actual implementation of bib file formatting.DocGen4/Output/Bibtex.leanwhich contains an implementation of bib file formatting by calling external Lean library BibtexQuery.DocGen4/Output/DocString.leanwhich analyzes citations in markdown text, inserting and modifying citation links, and collect back references.bibPrepassand 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.