Implement references / bibliography

[alexjbest]

trafficstars

In mathlib (3) we had a syntax for citing references stored in a .bib file and displaying them in a custom page https://leanprover-community.github.io/mathlib_docs/references.html.

We previously used the pybtex python library for obtaining the data from the bib file, this could be replaced by a call to a command line tool to convert to a more easily lean-parseable format (e.g. using pybtex)

[alreadydone]

Yeah, apparently links to bib entries are not rendered currently (compare mathlib3).

[acmepjz]

I'd like to working on it.

We previously used the pybtex python library for obtaining the data from the bib file, this could be replaced by a call to a command line tool to convert to a more easily lean-parseable format (e.g. using pybtex)

Could you give some information on this thing? I think it's the best if there are some tools converting bib file to markdown format (with LaTeX formulas in $ ... $), then the whole thing becomes straightforward.

[alexjbest]

Well doc-gen4 is written in lean, and the ideal situation IMO is that as much of the information is surfaced to Lean as possible so that we can do things like cross-links and sorting easily within doc-gen. So if I was implementing it I'd use some existing tool to convert to a structured plaintext format that is easy to parse in lean (json is probably the easiest afaict) and then write a renderer in Lean. as long at the latex is between the right brackets mathjax (which is included in doc-gen) should render that in the html output already.

[acmepjz]

Let me try to write a bibtex parser in lean using Parsec.

[acmepjz]

What should we do if the packages have their own bibliographies? I think maybe we should work out a first version which only considers bibliography in the docs directory, but not those in packages.

[hargoniX]

Generally speaking we should be able to discover .bib files of sub project shouldn't we?

[acmepjz]

Generally speaking we should be able to discover .bib files of sub project shouldn't we?

Ideally yes. But should we generate a reference page for each sub project, or combine all of them to get a single reference page?

In my opinion firstly we should implement an MVP which only reads bib file of root project. We can extend it later.