search

leanprover / doc-gen4

Document Generator for Lean 4
Apache License 2.0
62 stars 41 forks source link

Implement references / bibliography #147

Closed alexjbest closed 2 months ago

alexjbest commented 1 year ago

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 commented 12 months ago

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

acmepjz commented 3 months ago

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 commented 3 months ago

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 commented 3 months ago

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

acmepjz commented 3 months ago

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 commented 3 months ago

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

acmepjz commented 3 months ago

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.