Zulip Chat Archive

Stream: general

Topic: tweets mentioning the docs

Kevin Buzzard (Sep 19 2020 at 18:30):

Now we have the docs, I am slowly getting into the habit of using them to direct new users to Lean theorems or definitions. But when I tweet a link to the docs, I don't get some cute little graphic and to the right of it a little bit of text saying "leanprover-community.io" and then maybe either a snippet from the docs or a generic "The Lean Community Website, featuring documentation, how to get started and a description of mathlib" or whatever. I don't know what it's called but I know that if I tweet about the source code I get a little github logo

Alex Peattie (Sep 19 2020 at 18:39):

I think they're called Tweet cards. I'm happy to make a PR for them on doc-gen next week if someone else doesn't get there first :smile:

Alex J. Best (Sep 19 2020 at 18:43):

Adding some meta tags to doc-gen would be great, it might help with search engine visibility too!
Also leanprover-community.io isn't a real web address but perhaps it could be, or leanprover.community .

Alex J. Best (Sep 19 2020 at 18:43):

only $44 a year !

Kevin Buzzard (Sep 19 2020 at 18:44):

https://leanprover-community.github.io/ is of course what I meant to say :-) That's what I've been tweeting, just to be clear!

Alex J. Best (Sep 19 2020 at 18:47):

Yeah I also checked your tweets :wink:. but its an interesting idea anyway. Maybe its not worth the expense but being able to direct people to leanprover.community would be kinda fun.

Johan Commelin (Sep 19 2020 at 18:47):

it doesn't get auto-linkified though

Johan Commelin (Sep 19 2020 at 18:51):

Why is .lib not yet a TLD? math.lib would be cool

Jalex Stark (Sep 21 2020 at 12:13):

Getting a nice domain name is definitely a worthwhile expense. It would be kind of nice if there was mathlib legal entity that could do things like accept donations, pay for web hosting and olean cloud storage, etc.

Chris Wong (Sep 21 2020 at 13:35):

lean.community is available on namecheap for AUD 38
leanprover.io and leanprover.dev are similar
lean.io and lean.dev are enticing but pricey ("make an offer" and AUD 1158 respectively)
(ironically, leanprover.vip is one of the cheaper options)

Rob Lewis (Sep 21 2020 at 13:37):

I think .github.io URLs are considered reasonably professional. Buying a domain name is cheap but it introduces the recurring question of who's paying, who has control, etc.

Rob Lewis (Sep 21 2020 at 13:38):

I see little benefit and medium hassle moving away from the current URL.

Rob Lewis (Sep 21 2020 at 13:39):

On the other hand, "tweet cards" or whatever they're called for the website and docs would be welcome.

Gabriel Ebner (Sep 21 2020 at 14:28):

Rob Lewis said:

I see little benefit and medium hassle moving away from the current URL.

IMHO the main benefit would be to shorten the url. leanprover-community.github.io is a quite a lot to type (or include in footnotes, etc).

Yakov Pechersky (Sep 21 2020 at 14:48):

If only the .er TLD was widely available, then lean.prov.er

Alex J. Best (Sep 23 2020 at 02:37):

Johan Commelin said:

it doesn't get auto-linkified though

Not that I really care that much (I do agree with Rob that github is really fine right now), but I made a PR to zulip and it ended up as https://github.com/zulip/zulip/pull/16388 so at somepoint in the future versions of zulip leanprover.community will linkify.

Alex Peattie (Sep 24 2020 at 09:20):

This should be live now :smile:. Here's how the cards should look:

tweet.png

Scott Morrison (Sep 24 2020 at 10:09):

These are really nice!

Kevin Buzzard (Sep 24 2020 at 10:31):

https://twitter.com/XenaProject/status/1309077807956455424?s=20

Kevin Buzzard (Sep 24 2020 at 10:31):

It works! When I look at that on Twitter I get bc.png

Kevin Buzzard (Sep 24 2020 at 10:33):

I link specifically to measure_theory.measure_limsup_eq_zero (here) but the words in the cute box are "Measure spaces. Given a measurable space alpha, a measure on alpha is a function that send measurable sets to the extended..."

Alex Peattie (Sep 24 2020 at 10:34):

Kevin Buzzard said:

I link specifically to measure_theory.measure_limsup_eq_zero (here) but the words in the cute box are "Measure spaces. Given a measurable space alpha, a measure on alpha is a function that send measurable sets to the extended..."

Yeah unfortunately the metadata is per page (not per section), so not really an easy way around it - unless we ever got to the point of having an individual page per theorem

Kevin Buzzard (Sep 24 2020 at 10:36):

Well it's much much better than it was -- thanks so much!

Last updated: Dec 20 2023 at 11:08 UTC