API search less useful?

Stream: general

[Adam Topaz]

Is it just my imagination, or has the API search on our webpage
https://leanprover-community.github.io/mathlib_docs/
become less useful recently?

IIRC, we used to be able to type, for example, add monoid hom and have add_monoid_hom appear in the automatically populated list.
This is no longer the case.

Am I just misremembering?

[Yaël Dillies]

Gabriel just did a big change to search.

[Johan Commelin]

It seems that you should now do substrings. So addmonhom should work

[Arthur Paulino]

I'm trying to debug it right now

[Adam Topaz]

Johan Commelin said:

It seems that you should now do substrings. So addmonhom should work

Why is this better?

[Eric Rodriguez]

it's faster, is the essence

[Arthur Paulino]

Gabriel said that it's not intended. I'm trying to understand why whitespaces are making the queries return nothing

[Eric Rodriguez]

you can sort of game it to your advantage, too, for example I can type nfringofinteger for docs#number_field.ring_of_integers

[Yaël Dillies]

Yeah, just tried what Eric said and it's indeed very nice!

[Adam Topaz]

Maybe I'm just a gumpy mathematician, but I would still like to be able to write ring of integers

[Kyle Miller]

Maybe whitespace can count as "match any character"

[Gabriel Ebner]

I think the most useful interpretation of whitespace would be conjunction. That is, ring of integers would require all of ring and of and integers to match the declaration name. Which is kind of what was happening before.

[Gabriel Ebner]

The new search finds all declaration where the letters of the pattern occur in the declaration in the same order.

[Arthur Paulino]

What if we strip whitespaces from the user's input?

[Kyle Miller]

As a regular expression, right now ring int seems like it searches for .*r.*i.*n.*g.* .*i.*n.*t.*, but it could search for `.*r.*i.*n.*g.*..*i.*n.*t.* instead and perhaps make grumpy mathematicians happy, so long as you get the right order.

Conjunction makes sense, too.

[Gabriel Ebner]

The idea was to bring the search closer to how it works in vscode in Lean 4 (with ctrl+p #).

[Arthur Paulino]

Hmm, feels a bit weird because a search field in a browser and a development environment are very different contexts (maybe this is because it's causing some strangeness)

[Arthur Paulino]

Elaborating a bit further, we expect that hitting the space bar (or ESC) closes/cancels out search queries in dev environments. But we also (unconsciously?) expect that white spaces don't crash the query altogether in web browsers.
What do you guys think? https://github.com/leanprover-community/doc-gen/pull/155

[Yury G. Kudryashov]

BTW, would it be hard to search in docstrings too? E.g., I want to type "pigeonhole" and see the list of pigeonhole principle lemmas in mathlib.

[Yury G. Kudryashov]

Currently I use git grep (more precisely, Emacs's vc-git-grep)

[Eric Rodriguez]

I go for VSCode search 50% of the time, honestly

[Gabriel Ebner]

BTW, would it be hard to search in docstrings too?

There's another thread discussing a PR implementing that https://github.com/leanprover-community/doc-gen/pull/131 but it's horribly slow. You can try it out at http://leanprover-community.github.io/mathlib_docs_demo

[Arthur Paulino]

@Adam Topaz you can try add monoid hom again :+1:

[Adam Topaz]

Nice!

[Adam Topaz]

And with rng f ntgrs, we get number_field.ring_of_integers as well!

[Eric Rodriguez]

I think something that would be nice would be to prioritize defs over lemmata, because right now, finding (for example) number_field.ring_of_integers the way you usually would (ring of integers) prioritizes all of the function_field.ring_of_integers lemmas.

[Heather Macbeth]

Eric Rodriguez said:

I think something that would be nice would be to prioritize defs over lemmata, because right now, finding (for example) number_field.ring_of_integers the way you usually would (ring of integers) prioritizes all of the function_field.ring_of_integers lemmas.

I've noticed this many times when searching for the definition of the integral (!),
docs#measure_theory.integral
which doesn't turn up anywhere on the list of things when you type "integral" into the API search box.

[Stuart Presnell]

The first link at the 404 page for docs#convert is https://leanprover-community.github.io/mathlib_docs/find/convert, which just links back to the same 404 page. Is this intended or unavoidable behaviour?