Searching text of reference manual

Stream: general

[David Loeffler]

What's the simplest and quickest way to find a given text string in the reference manual (including doc string text, not just names of theorems)?

I assumed the "Google site search" button would do this, but apparently it doesn't: e.g. searching for "hahn banach" fails to find the theorem exists_extension_norm_eq, even though that name does appear prominently in the docstring of that theorem.

(This seems to be a regression from mathlib3 – in the mathlib3 manual, the default search box searched docstring content too – and it is a little annoying, since the mathlib name of a theorem is often quite different from the familiar real-world name, as in this example.)

Also, a separate issue also related to reference-manual search: there are lots of auto-generated instance names which are horrible pile-ups like AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionULocallyRingedSpaceInstCategoryLocallyRingedSpaceToGlueDataToLocallyRingedSpaceGlueDataGluedHasColimitOfHasColimitsOfShapeWalkingMultispanLDiagramRFstFromSndFromInstSmallCategoryWalkingMultispanHasColimitsOfShapeOfHasColimitsOfSizeInstHasColimitsLocallyRingedSpaceInstCategoryLocallyRingedSpaceMultispanι; and these tend to appear as spurious matches in search results for unrelated things, since the search doesn't require matching characters to be consecutive, so there's a high probability of any random short text string appearing as a match for one of these monsters. Is there a way of excluding these automatic instance names from the search results (and perhaps from the ref-manual text as well)?

[Kevin Buzzard]

The instance names issue is lean4#2343 . To search the docs for strings in lean 3 there was a "Google" button -- is that not still there? There's also moogle.ai .

[Johan Commelin]

I would run git grep -i "hahn.*banach"

[David Loeffler]

Kevin Buzzard said:

The instance names issue is #2343 . To search the docs for strings in lean 3 there was a "Google" button -- is that not still there? There's also moogle.ai .

There's a "Google site search" button but it appears to be broken – whatever you search for, it returns an error like "Your search - hahn banach site:https://leanprover-community.github.io/mathlib4_docs - did not match any documents".

Moogle works better, but it still doesn't seem to find exists_extension_norm_le; and it's slightly annoying to have to switch to a different page to search the ref manual when you already have the ref manual open.

[Henrik Böving]

image.png
it definitely finds stuff but not all stuff, no idea what google is doing here.

Searching the doc-string on the normal search functionality is something that we used to have but due to the sheer size of mathlib it slows down the responsiveness of the search and load time of the page noticably. People asked for a real-time ish search feeling faster load times so that's what I optimized for.