Zulip Chat Archive

Stream: general

Topic: API search less useful?


Adam Topaz (Jan 28 2022 at 18:50):

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 (Jan 28 2022 at 18:52):

Gabriel just did a big change to search.

Johan Commelin (Jan 28 2022 at 18:52):

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

Arthur Paulino (Jan 28 2022 at 18:53):

I'm trying to debug it right now

Adam Topaz (Jan 28 2022 at 18:54):

Johan Commelin said:

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

Why is this better?

Eric Rodriguez (Jan 28 2022 at 18:54):

it's faster, is the essence

Arthur Paulino (Jan 28 2022 at 18:55):

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

Eric Rodriguez (Jan 28 2022 at 18:55):

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 (Jan 28 2022 at 18:55):

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

Adam Topaz (Jan 28 2022 at 18:56):

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

Kyle Miller (Jan 28 2022 at 18:57):

Maybe whitespace can count as "match any character"

Gabriel Ebner (Jan 28 2022 at 18:57):

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 (Jan 28 2022 at 18:59):

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

Arthur Paulino (Jan 28 2022 at 18:59):

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

Kyle Miller (Jan 28 2022 at 18:59):

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 (Jan 28 2022 at 19:00):

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

Arthur Paulino (Jan 28 2022 at 19:03):

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 (Jan 28 2022 at 19:41):

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 (Jan 28 2022 at 19:42):

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 (Jan 28 2022 at 19:42):

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

Eric Rodriguez (Jan 28 2022 at 19:43):

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

Gabriel Ebner (Jan 28 2022 at 20:00):

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 (Jan 28 2022 at 20:55):

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

Adam Topaz (Jan 28 2022 at 20:56):

Nice!

Adam Topaz (Jan 28 2022 at 20:57):

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

Eric Rodriguez (Jan 28 2022 at 22:11):

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 (Jan 29 2022 at 01:29):

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 (Jan 29 2022 at 20:19):

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?


Last updated: Dec 20 2023 at 11:08 UTC