Zulip Chat Archive

Stream: general

Topic: browser extension for Lean

Kevin Buzzard (Jul 22 2020 at 08:56):

If I want to see (in a browser) the API documentation for the term free_abelian_group.lift, which I know is defined in mathlib but have no idea where, is there a way I can be one click away from the link #free_abelian_group.lift without having to bother the chat with the "hashtag" message? Is there a way to add a search of this nature as some sort of browser extension? Maybe all the fancy links you can do here, but within the browser?

Johan Commelin (Jul 22 2020 at 08:57):

We needs a command #docs free_abelian_group.lift inside Lean, and it will print the docs link in the infoview, and then ctrl-click on that link opens in in your browser.

Johan Commelin (Jul 22 2020 at 08:57):

Maybe if you click on a term in the infoview, the widget with type info could also have a little icon that takes you to the docs page?

Rob Lewis (Jul 22 2020 at 08:59):

I added a custom search engine in Crome that maps a search term t to https://leanprover-community.github.io/mathlib_docs/find/t. So I just type "mathlib nat.succ" in the url box and it takes me right there.

Rob Lewis (Jul 22 2020 at 08:59):

(deleted)

Rob Lewis (Jul 22 2020 at 09:00):

You can do the same to go to source on GitHub with the url https://leanprover-community.github.io/mathlib_docs/find/t/src

Rob Lewis (Jul 22 2020 at 09:09):

FWIW, in Chrome: image.png

Rob Lewis (Jul 22 2020 at 09:10):

(no extension needed)

Kevin Buzzard (Jul 22 2020 at 10:07):

Where are the Zulip docs for what you can do with # again? My search is failing me today. #123 and docs#simp and what have you? Sorry to have to ask again.

Rob Lewis (Jul 22 2020 at 10:10):

https://leanprover.zulipchat.com/#organization/filter-settings

Jalex Stark (Jul 22 2020 at 12:14):

The # things are called linkifiers in case a name is helpful

Scott Morrison (Aug 05 2020 at 22:39):

Just repeating Rob's suggestion above in text instruction forms, rather than an image:

  • In google chrome, open settings
  • enter "search engines" in the search bar, select "manage search engines",
  • click "add"
  • enter mathlib docs, or whatever you like in "search engine box"
  • enter mathlib or ml whatever prefix you like in the "keyword box"
  • enter https://leanprover-community.github.io/mathlib_docs/find/%s in the URL box
  • now you can just enter mathlib PresheafedSpace in the chrome search bar

Bryan Gin-ge Chen (Aug 05 2020 at 22:42):

I'm sad that Firefox doesn't seem to let users do anything like this easily.

Jannis Limperg (Aug 06 2020 at 11:57):

Firefox apparently wants websites to provide an OpenSearch description of their search engine. Bit annoying (and surprising) that there's no manual alternative.

Gabriel Ebner (Aug 06 2020 at 12:14):

PRs welcome

Reid Barton (Aug 06 2020 at 12:39):

I got it to work in Firefox by trying to add a search keyword using the contextual menu, and then when this produced a nonworking keyword, editing the bookmark URL to the same thing https://leanprover-community.github.io/mathlib_docs/find/%s above

Rob Lewis (Aug 06 2020 at 12:43):

I feel like I did this kind of thing 15 years ago in Firefox without much trouble, heh.

Last updated: Dec 20 2023 at 11:08 UTC