-
Notifications
You must be signed in to change notification settings - Fork 20
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
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.html
page, generated from mathlib'sdocs/references.bib
and 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 ajoyal1997
inset_theory.pgame
which 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.