references page and links #117
Conversation
|
#deploy 🙏 |
|
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo! |
|
#deploy |
|
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo! |
|
Two problems at https://leanprover-community.github.io/mathlib_docs_demo/topology/sheaves/sheaf_condition/opens_le_cover.html#backref1
Unfortunately, these both seem to be related to the CSS hack that I don't fully understand yet. edit: I fixed both of these issues in Chrome and Firefox by using |
|
#deploy |
|
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo! |
|
#deploy |
|
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo! |
|
3 things I want to add before this is merged:
There's an active discussion about Stacks tags on Zulip, so that may be the next PR. |
|
#deploy |
|
#deploy |
|
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo! |
| # count will track number of times label has been finalized | ||
| count = Counter() | ||
|
|
||
| for key, data in bib.entries.items(): |
There was a problem hiding this comment.
The ordering of the bib entries here is whatever it is in mathlib's docs/references.bib. This could potentially lead to strange ordering of the a, b, c that are appended to labels.
| @@ -79,6 +81,63 @@ | |||
| # root directory of mathlib. | |||
| local_lean_root = os.path.join(root, cl_args.r if cl_args.r else '_target/deps/mathlib') + '/' | |||
|
|
|||
| bib = pybtex.database.parse_file(f'{local_lean_root}docs/references.bib') | |||
|
|
|||
| label_style = LabelStyle() | |||
There was a problem hiding this comment.
Using LabelStyle here is a bit of a hack since I couldn't figure out how to use pybtex's bibliography formatting classes here. (If someone can figure it out, feel free to fix this!)
|
#deploy |
|
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo! |
|
@bryangingechen this looks fantastic. I'm happy to merge if you are. @gebner ? |
|
Yeah, looks great, Bryan! |
|
Thanks! I'll merge this now then! |
Adds a
references.htmlpage, generated from mathlib'sdocs/references.biband creates links from all strings of the form "[bib_entry_key]" in docstrings to the entry on that page. The keys are replaced with auto-generated labels following the BibTeX "alpha" style.Also includes backrefs for both bib entries and library notes (links back from the bib / note entries to the pages that cite them). Some of the entries without backrefs correspond to links in
archive/(e.g.Hofstadter-1979) and some are truly missing (e.g.joyal1977, there's ajoyal1997inset_theory.pgamewhich is probably a typo).Finally, I added functionality that turns raw URLs in the markdown into links.
I did basically the bare minimum, copying as much as I could from leanprover-community.github.io, so any styling / formatting suggestions are welcome!
Zulip thread here.