-
Notifications
You must be signed in to change notification settings - Fork 36
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Implement references / bibliography #147
Comments
Yeah, apparently links to bib entries are not rendered currently (compare mathlib3). |
I'd like to working on it.
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 |
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. |
Let me try to write a bibtex parser in lean using |
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 |
Generally speaking we should be able to discover .bib files of sub project shouldn't we? |
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.
|
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. usingpybtex
)The text was updated successfully, but these errors were encountered: