links

Stream: Zulip meta

[Johan Commelin]

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

[Johan Commelin]

@Rob Lewis @Patrick Massot what do you think?

[Kevin Buzzard]

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

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

[Jalex Stark]

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

[Mario Carneiro]

give me a list of links please

[Bryan Gin-ge Chen]

• #tpil - https://leanprover.github.io/theorem_proving_in_lean/
• #homepage - https://leanprover-community.github.io
• #webeditor - https://leanprover-community.github.io/lean-web-editor
• #tutorials - https://github.com/leanprover-community/tutorials
• #docs - https://leanprover-community.github.io/mathlib_docs

[Mario Carneiro]

#tpil #homepage #webeditor #tutorials #docs

[Johan Commelin]

Thanks a lot!

[Kevin Buzzard]

This is great! Many thanks all!

[Jalex Stark]

Bryan Gin-ge Chen said:

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

[Rob Lewis]

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

[Rob Lewis]

Ah, seems unhappy parsing dots in identifiers :/

[Mario Carneiro]

Rob Lewis said:

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

[Mario Carneiro]

Rob Lewis said:

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

[Mario Carneiro]

there we go

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Rob Lewis]

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]

Not sure exactly what a bookmarklet does compared to that.

[Rob Lewis]

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

[Rob Lewis]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

But ultimately this is just a placeholder for better search.

[Jalex Stark]

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

[Bryan Gin-ge Chen]

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

[Rob Lewis]

#file-not-found ?

[Bryan Gin-ge Chen]

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

[Sebastian Ullrich]

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

[Johan Commelin]

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

[Sebastian Ullrich]

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

[Johan Commelin]

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]

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]

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]

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

[Rob Lewis]

#install ?

[Bryan Gin-ge Chen]

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.

[Jalex Stark]

branch#fincard

[Eric Wieser]

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.

[Rob Lewis]

(deleted)

[Rob Lewis]

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

[Anne Baanen]

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

[Anne Baanen]

(Untested)

[Rob Lewis]

docs#exterior_algebra.

[Anne Baanen]

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

[Rob Lewis]

That's weird...

[Eric Wieser]

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

[Kevin Buzzard]

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]

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]

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

[Sebastian Ullrich]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Sebastian Ullrich]

Sure, even better!

[Scott Morrison]

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

[Scott Morrison]

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

[Bryan Gin-ge Chen]

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]

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]

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]

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

[Bryan Gin-ge Chen]

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

[Eric Wieser]

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

[Scott Morrison]

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]

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.

[Mario Carneiro]

tactic#ring?

[Bryan Gin-ge Chen]

tactic#norm_num!

[Bryan Gin-ge Chen]

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