leanprover-community / doc-gen

Generate HTML documentation for mathlib and Lean

https://leanprover-community.github.io/mathlib_docs/

Apache License 2.0

21 stars 20 forks source link

Add opengraph tags to `/find/` urls #162

Closed eric-wieser closed 2 years ago

eric-wieser commented 2 years ago

The idea here is to be able to share a find-style URL as generated by zulip, and have it show a social preview.

This also corrects the wonky existing meta tags; the og:* fields belong in property not name, and twitter says we do not need the twitter ones too once we have those correct.

Demonstration of this working:

https://www.opengraph.xyz/url/https%3A%2F%2Fleanprover-community.github.io%2Fmathlib_docs_demo%2Ffind%2Falgebra%2F/

https://developers.facebook.com/tools/debug/?q=https%3A%2F%2Fleanprover-community.github.io%2Fmathlib_docs_demo%2Ffind%2Falgebra

Note we can't test with https://cards-dev.twitter.com/validator, as robots.txt blacklists the doc demo site.

eric-wieser commented 2 years ago

deploy

github-actions[bot] commented 2 years ago

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

eric-wieser commented 2 years ago

deploy

eric-wieser commented 2 years ago

deploy

eric-wieser commented 2 years ago

deploy

github-actions[bot] commented 2 years ago

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

eric-wieser commented 2 years ago

deploy

gebner commented 2 years ago

The change looks good to me, feel free to merge once you're satisfied with it.

github-actions[bot] commented 2 years ago

This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!

eric-wieser commented 2 years ago

It looks like facebook unfortunately just follows the redirect, but maybe twitter will be better behaved.

eric-wieser commented 2 years ago

Seems to work on discord and twitter: