Documentation autosearch is not very good

[BoltonBailey]

Here is a screenshot of the result when I search for list.map

As you can see list.map is a real function, but for some reason it is not the first result - I have to look almost to the bottom of the list of hits to find it. When I type in the exact name of the function I'm looking up the docs for, it should be the first hit on the drop down.

[robertylewis]

There are plans to overhaul the docs search, but I wouldn't expect changes in the immediate future.

[BoltonBailey]

Just another thing I've found to try to convince people this issue is important: In a discussion on the zulip, someone brought up "big_operators" and I didn't know what it was. I searched for it, and got no result. It finally had to be linked to me by someone in the chat.

[bryangingechen]

One thing which is very far from obvious at the moment is that clicking the search button does something totally unrelated to the choices in the drop down menu -- it performs a google search on leanprover-community.github.io/mathlib_docs. In this example, it does find a bunch of big_operators hits.

Making that feature more discoverable from the UI somehow could be an easy PR with a decent impact on usability.