google site search in API docs

Stream: general

[Kevin Buzzard]

What is "google site search" even supposed to do? If I type mul_add into the mathlib API docs and hit "google site search" it sends me to Init.Data.Nat.Basic which is probably not what I want. I'm attempting to try and write a document explaining how to use various search facilities and I'm struggling to explain what this button does!

[Richard Copley]

The button acts as a link to <https://google.com/search?sitesearch=https%3A%2F%2Fleanprover-community.github.io%2Fmathlib4_docs&q=mul_add>. What happens after that is Google's secret, but Init.Data.Nat.Basic is the page that has mul_add on it.

[Henrik Böving]

Tbh we can also just remove that button I think, the vast majority of people is probably not using it

[Kevin Buzzard]

I would say that mul_add was a theorem about semirings and I'm surprised I'm not being directed to the "correct" mul_add but rather to far more specific Nat.mul_add. I wonder why it's not giving me the more general theorem?

[Henrik Böving]

Google doesn't have any semantic information about what's going on on the docs page. It is literally just asking google's algorithm "if i were to look for this keyword and limit my results to this domain,what would I get" What happens is entirely up to Google.

[Jason Rute]

I’m surprised no one has added a “search with Moogle” option. I find Moogle pretty good for Lean. (Of course it may go away at any time, but for now it is nice.)

[Shreyas Srinivas]

I don't think moogle offers any API to do that. When I asked them about one to integrate into my loogle extension, the lack of response was not encouraging

[Jason Rute]

Wait, can’t you just prepend https://www.moogle.ai/search/raw?q=. I assume the search with Google is basically the same sort of thing.