processing links to declarations

[robertylewis]

This is also discussed in some comments on #9 .

We already have an "API" for linking to and displaying declarations: there's a json file hosted with the docs page that maps declaration names to their locations in docs and source, and a pretty-printed, linkified display of the declaration's type. This is used, for instance, in the 100 theorems page.

It might make sense to use this in the blog too, in at least two scenarios:

• If you display a declaration inline, like absolutely_continuous_iff_with_density_radon_nikodym_deriv_eq, we could print it as in the 100 theorems page. Unfortunately the API won't print declaration bodies, nor is this easy to do, so things like def measure.singular_part above would be harder.
• If you refer to a declaration by name without displaying it, like "In Lean, this is shown by absolutely_continuous_iff_with_density_radon_nikodym_deriv_eq and can be found in measure_theory/decomposition/radon_nikodym.", we could automatically link to the updated location in docs and/or source. This is not robust to name changes though.

Moreover, every blog build would check for links broken by name changes.

How to implement this though? I'm not sure how much control we get over Nikola's markdown processing. I couldn't tell after glancing at the docs what md processor it uses. We need something triggered by a particular regex pattern, more involved than a linkifier.

This also doesn't address the concern that as declarations change in mathlib over time, blog posts could become out of date.

[gebner]

This also doesn't address the concern that as declarations change in mathlib over time, blog posts could become out of date.

I'd be much more comfortable if we quoted the definitions and lemma statements in the blog posts. A blog post is not a living document, I expect it to describe the state of mathlib at the time of it's publication.

[robertylewis]

This also doesn't address the concern that as declarations change in mathlib over time, blog posts could become out of date.

I'd be much more comfortable if we quoted the definitions and lemma statements in the blog posts. A blog post is not a living document, I expect it to describe the state of mathlib at the time of it's publication.

Agreed. Mostly I was missing the linkification that you see in the declarations on the 100 theorems page. But I'm not sure how to conveniently do that with a static post. I guess we could have a separate page that generates linkified code to copy-paste in.