FindFacts drill down facets

Stream: mathlib4

[Johan Commelin]

I just learned about Isabelle's FindFacts. It has this "drill down facets". That seems like a very useful feature. Would that be something for mathlib docs search as well?

Example: https://search.isabelle.in.tum.de/#search/default_Isabelle2024_AFP2024?q=%7B%22term%22%3A%22bigo%22%2C%22facets%22%3A%7B%22Kind%22%3A%5B%22Constant%22%5D%7D%7D

E.g. we might want to be able to "drill down" into one top-level folder.

Maybe not just mathlib-docs. Other search tools could have this as well.

[Jireh Loreaux]

I'm not sure I understand what's going on here. Can you give a brief explanation?

[Johan Commelin]

Well, you search for something on mathlib docs, or moogle, or whatever, and then maybe you want to apply extra filters on top of the search results. For example: $n_1$ results in Algebra/ and $n_2$ results in Topology/ etc... and you want to filter for only the results in a certain folder, once you know how many results there are in each folder.

[Jireh Loreaux]

okay, so basically it's just query filters. Yes, that would be lovely. Even just filtering out theorem vs def vs structure vs class etc. would be nice.

[Joachim Breitner]

Loogle inherently supports filtering by theorem or lemma, using |- (?a : Prop) resp. |- (?a : Type _). Nicer syntax to be added eventually. (https://github.com/nomeata/loogle/issues/9)

[Joachim Breitner]

Using something like "List." you can approximate filtering by namespace rather well.

Something similar to filter by defining module might be useful. As usual, the syntax design is the hardest part :-)

[Mario Carneiro]

I wonder whether loogle could take some design inspiration from coq's Search tactic? It seems most structurally similar to that tactic (indeed the original #find was based on it), but it has a more expressive syntax than loogle currently supports

[Johan Commelin]

Joachim Breitner said:

Loogle inherently supports filtering by theorem or lemma, using |- (?a : Prop) resp. |- (?a : Type _). Nicer syntax to be added eventually. (https://github.com/nomeata/loogle/issues/9)

That's nice!

[Johan Commelin]

One benefit of the "drill down" feature in FindFacts is discoverability. It gives suggestions of which filters you can apply. And it already tells you how many results satisfy a certain filter. So you can guesstimate whether it is useful to "drill down" in that direction.