give more detail in search bar

Stream: general

[Yaël Dillies]

I'm thinking we could add their paths next to the names of the declarations that come up when searchin the doc. This could be in grey and italic, to avoid obscuring the window. Typical polymorphism
It would help distinguish some synonyms.

[Eric Rodriguez]

this is in the beta docs, https://leanprover-community.github.io/mathlib_docs_demo/, but it sadly hasn't been updated for a while :(

[Eric Rodriguez]

for reference image.png

[Eric Wieser]

Right, that's https://github.com/leanprover-community/doc-gen/pull/131

[Yaël Dillies]

Wow! That's amazinger than what I ought to dream!

[Bryan Gin-ge Chen]

I was planning on reviewing that PR in more detail, but I haven't had time yet. So please try out the PR; if enough folks are mostly happy with it, I think we can merge it as is.

[Bryan Gin-ge Chen]

For now, I'll re-deploy it so that it's more up to date with current mathlib.

[Eric Rodriguez]

FWIW, Bryan, it seemed really good when it was up-to-date. No teething issues (apart from wishing search was faster :b )

[Eric Rodriguez]

I'll try it again now

[Eric Wieser]

That PR probably makes it much slower, since the search index grows from 2mb to 15mb