Zulip Chat Archive
Stream: general
Topic: Searching the docs is fast now
Bolton Bailey (Jan 26 2022 at 19:04):
I just noticed that the search function on the docs page is much faster now (no more dancing octopi). This is great! Whoever made this happen, good on you.
Yaël Dillies (Jan 26 2022 at 19:04):
Is it not that you have a second tab of the docs open?
Eric Rodriguez (Jan 26 2022 at 19:05):
no, Gabriel made a change
Yaël Dillies (Jan 26 2022 at 19:05):
Oh okay!
Eric Rodriguez (Jan 26 2022 at 19:05):
it's very exciting
Jireh Loreaux (Jan 26 2022 at 20:22):
This is absolutely amazing. I have no words.
Kevin Buzzard (Jan 26 2022 at 22:52):
Floris van Doorn (Jan 27 2022 at 13:35):
@Gabriel Ebner I have the feeling the search suggestions have degraded. There are a lot less suggestions, and a lot more frequently I get 0 suggestions.
For example, searching for docs#is_compact_of_closed_subset doesn't find docs#compact_of_is_closed_subset, and I think that worked before.
Gabriel Ebner (Jan 27 2022 at 13:52):
Right, that's kind of intentional. The characters in the search query now need to occur in the declaration name in the same order, which is closer to how the search works in vscode. Try shorter queries, e.g. docs#compclosub has the lemma as the first hit.
Floris van Doorn (Jan 27 2022 at 15:13):
Ok, I'll try shortening my search queries.
Arthur Paulino (Jan 27 2022 at 15:16):
Maybe offtopic, but would it be nice to have some weaker results with fuzzy matches?
Last updated: Dec 20 2023 at 11:08 UTC