Zulip Chat Archive

Stream: Zulip meta

Topic: links


view this post on Zulip Johan Commelin (May 08 2020 at 21:20):

Maybe it would be nice to also have #tpil #homepage #webeditor #tutorial #docs and such. Or is this asking too much?

view this post on Zulip Johan Commelin (May 08 2020 at 21:20):

@Rob Lewis @Patrick Massot what do you think?

view this post on Zulip Kevin Buzzard (May 08 2020 at 22:11):

#tpil would be brilliant, I have genuinely lost count of the number of times I've opened a new tab, googled theorem proving in Lean, and then cut and pasted the link

view this post on Zulip Bryan Gin-ge Chen (May 08 2020 at 22:25):

Who has the power to do this again? @Mario Carneiro and Rob?

view this post on Zulip Jalex Stark (May 08 2020 at 22:40):

Also @Sebastian Ullrich. It's linked to the admin role, and you find people with that role by clicking settings -> organization settings -> users and sorting by role

view this post on Zulip Mario Carneiro (May 09 2020 at 05:16):

give me a list of links please

view this post on Zulip Bryan Gin-ge Chen (May 09 2020 at 05:27):

view this post on Zulip Mario Carneiro (May 09 2020 at 05:35):

#tpil #homepage #webeditor #tutorials #docs

view this post on Zulip Johan Commelin (May 09 2020 at 05:36):

Thanks a lot!

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:23):

This is great! Many thanks all!

view this post on Zulip Jalex Stark (May 18 2020 at 21:27):

Bryan Gin-ge Chen said:

For completeness, here are the naming conventions. (Do we need #naming?)

view this post on Zulip Rob Lewis (May 20 2020 at 20:25):

Testing a few more: docs#manifold docs#nat.succ src#int.add src#vector_space

view this post on Zulip Rob Lewis (May 20 2020 at 20:27):

Ah, seems unhappy parsing dots in identifiers :/

view this post on Zulip Mario Carneiro (May 20 2020 at 20:38):

Rob Lewis said:

Testing a few more: docs#manifold docs#nat.succ src#int.add src#vector_space

view this post on Zulip Mario Carneiro (May 20 2020 at 20:39):

Rob Lewis said:

Testing a few more: docs#manifold docs#nat.succ src#int.add src#vector_space

view this post on Zulip Mario Carneiro (May 20 2020 at 20:39):

there we go

view this post on Zulip Mario Carneiro (May 20 2020 at 20:40):

wow that's a pretty nifty URL scheme. I might send myself PMs just to use this for lookup

view this post on Zulip Kevin Buzzard (May 20 2020 at 22:49):

Ha ha I had exactly that thought today but I thought better of it! It's certainly quicker than firing up a browser and opening up your bookmarks and navigating to the docs site and then searching for the function name and knowing that the search might not even work...

view this post on Zulip Jalex Stark (May 21 2020 at 00:07):

huh i just always have a browser instance with a mathlib docs tab (at least on my laptop where I write code, not on my phone)

view this post on Zulip Kevin Buzzard (May 21 2020 at 07:34):

But even with the docs tab open it can happen that search for a precise term name doesn't take you to the definition of that term

view this post on Zulip Mario Carneiro (May 21 2020 at 07:36):

Yeah, isn't the docs search just an elasticsearch or google search thing? It would be much better if we could have something more like vscode's #foo menu

view this post on Zulip Gabriel Ebner (May 21 2020 at 07:36):

FYI, @Rob Lewis has a student working on this.

view this post on Zulip Mario Carneiro (May 21 2020 at 07:38):

I guess the low effort version is an input field with no live feedback where you can type a name and it just uses the URL scheme

view this post on Zulip Rob Lewis (May 21 2020 at 08:29):

The low low effort version is, type https://leanprover-community.github.io/mathlib_docs/find/classical.em into the URL. But yes, I've been promised some movement on a real name/doc string search function soon.

view this post on Zulip Rob Lewis (May 21 2020 at 08:31):

You could even set up your browser to do something like Zulip linkification if you wanted. So docs classical.em in the URL bar would take you there.

view this post on Zulip Mario Carneiro (May 21 2020 at 08:48):

I've been using this "guess the URL" method for years with metamath, e.g. http://us.metamath.org/mpeuni/pnt.html . It is very slightly easier in that case because the URLs are not redirects, so I can just leave a page open and change the label portion of the URL to find a theorem. With the mathlib docs, it immediately redirects to something else, so the URL becomes a kind of magic incantation that you wouldn't know unless you stumble upon it in e.g. a linkifier (which is exactly what happened to me above).

view this post on Zulip Mario Carneiro (May 21 2020 at 08:52):

Perhaps we could provide a link to help people set up automatic linkification in the browser bar? Would a bookmarklet help?

view this post on Zulip Rob Lewis (May 21 2020 at 08:54):

We could, I'm not sure where to put it though. In Chrome I just went to Settings -> Search Engines and added a new search engine with keyword mathlib, query url https://leanprover-community.github.io/mathlib_docs/find/%s

view this post on Zulip Rob Lewis (May 21 2020 at 08:55):

Not sure exactly what a bookmarklet does compared to that.

view this post on Zulip Rob Lewis (May 21 2020 at 08:55):

You stumbled onto this a few hours after it went live btw, not like you were missing it for long!

view this post on Zulip Rob Lewis (May 21 2020 at 08:57):

I have so many search engines on this list. Chrome must add them automatically every time you search a site.

view this post on Zulip Mario Carneiro (May 21 2020 at 08:57):

Ideally there should be a link very close to the google search bar in the mathlib docs explaining this

view this post on Zulip Mario Carneiro (May 21 2020 at 08:59):

I expect that adding an actual input field there is about as much work as writing a page to explain how to set up the custom search mechanism in your browser

view this post on Zulip Mario Carneiro (May 21 2020 at 09:04):

Rob Lewis said:

You stumbled onto this a few hours after it went live btw, not like you were missing it for long!

I am rather more connected to daily goings-on than the average lean user, though. Also this stream is not a default stream so most people have not seen this discussion, even considering users that use Zulip. I suspect there are a lot of programmer types who don't read Zulip at all and are just looking at stuff that looks like documentation, and this feature needs to be discoverable for them

view this post on Zulip Rob Lewis (May 21 2020 at 09:16):

I'm well aware it can be better publicized, it's 12 hours old and I did it while I was procrastinating writing an exam. Something will land on the docs pages when I have time or if anyone else wants to make a PR :)

view this post on Zulip Rob Lewis (May 21 2020 at 09:17):

But ultimately this is just a placeholder for better search.

view this post on Zulip Jalex Stark (May 22 2020 at 17:07):

chore: change #mwe to link to https://leanprover-community.github.io/mwe.html

view this post on Zulip Bryan Gin-ge Chen (Jun 01 2020 at 21:46):

Another request: make #file-not-found point to https://leanprover-community.github.io/file-not-found.html

view this post on Zulip Rob Lewis (Jun 01 2020 at 22:28):

#file-not-found ?

view this post on Zulip Bryan Gin-ge Chen (Jun 03 2020 at 01:24):

#mil should link to https://leanprover-community.github.io/mathematics_in_lean/

view this post on Zulip Sebastian Ullrich (Jun 03 2020 at 08:24):

Ooh, I also want to give this a try for once. #mil

view this post on Zulip Johan Commelin (Jun 03 2020 at 08:26):

@Sebastian Ullrich Great! You levelled-up. You now have +5xp in the "zulip-admin" skill.

view this post on Zulip Sebastian Ullrich (Jun 03 2020 at 08:28):

Skills have individual XP?? This system sounds harder than I thought...

view this post on Zulip Johan Commelin (Jun 03 2020 at 08:29):

Ooh well. You shouldn't complain. You're already level 99 in "lean 4". Most of us haven't even started that one.

view this post on Zulip Patrick Massot (Jun 03 2020 at 08:33):

I don't think this is the right link. It encourages people to read this book in their web browser when it's designed to be read in VSCode.

view this post on Zulip Patrick Massot (Jun 03 2020 at 08:34):

But maybe it's ok since https://leanprover-community.github.io/mathematics_in_lean/introduction.html#getting-started starts by explaining that point.

view this post on Zulip Bryan Gin-ge Chen (Jun 07 2020 at 16:16):

I think #install should redirect to https://leanprover-community.github.io/get_started.html#regular-install instead of the mathlib repo.

view this post on Zulip Rob Lewis (Jun 07 2020 at 16:21):

#install ?

view this post on Zulip Bryan Gin-ge Chen (Jun 07 2020 at 16:23):

It works, though we may want to add extra whitespace at the end of the file so it's more obvious that we're linking the last section.

view this post on Zulip Jalex Stark (Aug 22 2020 at 23:16):

branch#fincard

view this post on Zulip Eric Wieser (Oct 02 2020 at 10:25):

Can we adjust the linkifier to not consume trailing .? At the moment docs#exterior_algebra. and branch#fincard. give invalid links, as the . is interpreted as part of the link.

view this post on Zulip Rob Lewis (Oct 02 2020 at 10:30):

(deleted)

view this post on Zulip Rob Lewis (Oct 02 2020 at 10:32):

Hmm, the current regex is docs#(?P<decl>[a-zA-Z0-9_.'-]+), if you can suggest an improvement I'll change it

view this post on Zulip Anne Baanen (Oct 02 2020 at 10:33):

Maybe docs#(?P<decl>[a-zA-Z0-9_.'-]*[a-zA-Z0-9_'-])?

view this post on Zulip Anne Baanen (Oct 02 2020 at 10:33):

(Untested)

view this post on Zulip Rob Lewis (Oct 02 2020 at 10:35):

docs#exterior_algebra.

view this post on Zulip Anne Baanen (Oct 02 2020 at 11:03):

Interestingly, docs#37 does seem to be parsed by the linkifier but Zulip doesn't want to post it.

view this post on Zulip Rob Lewis (Oct 02 2020 at 11:15):

That's weird...

view this post on Zulip Eric Wieser (Oct 02 2020 at 12:22):

docs#37a is fine, but branch#37 has the same problem

view this post on Zulip Kevin Buzzard (Oct 02 2020 at 15:14):

I went to the Coq Zulip and they have a stackexchange bot. How hard is that to set up? Occasional Lean questions get asked on stackoverflow, and Scott has long observed that they have big google points

view this post on Zulip Rob Lewis (Oct 02 2020 at 15:33):

Looks like Zulip has a bot for it but it's not an outgoing webhook like GitHub so you need a server to run the bot on.

view this post on Zulip Rob Lewis (Oct 02 2020 at 15:34):

There's not exactly a flood of Lean questions: https://stackoverflow.com/questions/tagged/lean

view this post on Zulip Sebastian Ullrich (Oct 02 2020 at 16:18):

I could run it on my server, next to the RSS bot

view this post on Zulip Rob Lewis (Oct 02 2020 at 16:21):

Can you get an RSS feed of SO posts with a certain tag? Then you don't even need a new bot

view this post on Zulip Rob Lewis (Oct 02 2020 at 16:24):

https://stackoverflow.com/feeds/tag?tagnames=lean&sort=newest

view this post on Zulip Sebastian Ullrich (Oct 02 2020 at 17:36):

Sure, even better!

view this post on Zulip Scott Morrison (Oct 03 2020 at 00:32):

I don't seem to be able to link to branches...

view this post on Zulip Scott Morrison (Oct 03 2020 at 00:32):

It seems any message with branch # bell (remove the spaces) fails to post.

view this post on Zulip Bryan Gin-ge Chen (Oct 03 2020 at 00:34):

I was having trouble linking a tactic doc earlier too. I couldn't even preview tactic # norm_num (without the spaces).

view this post on Zulip Bryan Gin-ge Chen (Oct 03 2020 at 00:36):

If we haven't changed our linkifiers recently, we should see if this has been reported to Zulip already somewhere. I didn't see it in the open issues: https://github.com/zulip/zulip/issues

view this post on Zulip Rob Lewis (Oct 03 2020 at 10:34):

I did change the linkifiers yesterday (see earlier in this thread) but the new ones don't seem more dangerous than the old AFAICT

view this post on Zulip Bryan Gin-ge Chen (Oct 03 2020 at 16:17):

Bizarre, docs#norm_num works but I still can't get tactic#norm_num to work.

view this post on Zulip Bryan Gin-ge Chen (Oct 03 2020 at 16:17):

As far as I can tell the regexes are pretty much the same.

view this post on Zulip Eric Wieser (Oct 15 2020 at 10:25):

vscode-lean#227 goes to a nonexistant repo, it should be leanprover not leanprover-community

view this post on Zulip Scott Morrison (Oct 15 2020 at 21:27):

The linkifier doesn't have any logic that looks at the repo name to decide the organisation. You'll need to use leanprover/vscode-lean#227

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 21:40):

I don't know if the tactic linkifier was changed again, but it seems to be completely broken now. Looking again at the linkifier, the URL part says name but the regex group is named decl, which is suspicious.

view this post on Zulip Mario Carneiro (Oct 16 2020 at 19:00):

tactic#ring?

view this post on Zulip Bryan Gin-ge Chen (Oct 16 2020 at 19:03):

tactic#norm_num!

view this post on Zulip Bryan Gin-ge Chen (Oct 27 2020 at 15:51):

We have attr and tactic linkifiers, so we should have hole, cmd, and note for completeness.


Last updated: May 08 2021 at 21:09 UTC