## Stream: Zulip meta

#### 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?

#### Johan Commelin (May 08 2020 at 21:20):

@Rob Lewis @Patrick Massot what do you think?

#### 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

#### Bryan Gin-ge Chen (May 08 2020 at 22:25):

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

#### 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

Thanks a lot!

#### Kevin Buzzard (May 09 2020 at 07:23):

This is great! Many thanks all!

#### Jalex Stark (May 18 2020 at 21:27):

Bryan Gin-ge Chen said:

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

#### Rob Lewis (May 20 2020 at 20:25):

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

#### Rob Lewis (May 20 2020 at 20:27):

Ah, seems unhappy parsing dots in identifiers :/

#### 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

#### 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

there we go

#### 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

#### 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...

#### 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)

#### 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

#### 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

#### Gabriel Ebner (May 21 2020 at 07:36):

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

#### 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

#### 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.

#### 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.

#### 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).

#### 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?

#### 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

#### Rob Lewis (May 21 2020 at 08:55):

Not sure exactly what a bookmarklet does compared to that.

#### 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!

#### 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.

#### 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

#### 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

#### 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

#### 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 :)

#### Rob Lewis (May 21 2020 at 09:17):

But ultimately this is just a placeholder for better search.

#### Jalex Stark (May 22 2020 at 17:07):

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

#### 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

#### Sebastian Ullrich (Jun 03 2020 at 08:24):

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

#### Johan Commelin (Jun 03 2020 at 08:26):

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

#### Sebastian Ullrich (Jun 03 2020 at 08:28):

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

#### 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.

#### 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.

#### 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.

#### 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.

#### 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.

branch#fincard

#### 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.

(deleted)

#### 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

#### Anne Baanen (Oct 02 2020 at 10:33):

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

(Untested)

#### 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.

That's weird...

#### Eric Wieser (Oct 02 2020 at 12:22):

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

#### 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

#### 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.

#### Rob Lewis (Oct 02 2020 at 15:34):

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

#### Sebastian Ullrich (Oct 02 2020 at 16:18):

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

#### 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

#### Sebastian Ullrich (Oct 02 2020 at 17:36):

Sure, even better!

#### Scott Morrison (Oct 03 2020 at 00:32):

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

#### Scott Morrison (Oct 03 2020 at 00:32):

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

#### 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).

#### 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

#### 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

#### 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.

#### Bryan Gin-ge Chen (Oct 03 2020 at 16:17):

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

#### Eric Wieser (Oct 15 2020 at 10:25):

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

#### 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

#### 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.

#### 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