feedback on LeanSearch

Stream: general

[Kim Morrison]

I've been having trouble with leansearch.net recently --- and I'm getting suspicious that it never returns results from the standard library!

e.g.

https://leansearch.net/?q=If%20two%20lists%20are%20permutations%20of%20each%20other%2C%20the%20counts%20of%20each%20term%20in%20those%20lists%20are%20equal.

should surely show List.perm_iff_count, but everything it mentions is from Mathlib, nothing from the standard library!

@Jiang Jiedong?

[Jiang Jiedong]

@Kim Morrison Thank you for your feedback! The standard library isn't currently included in the database.

I've been discussing this issue with the current maintainer @Tony Beta Lambda of LeanSearch, as there are varying user needs:

• Some want Mathlib-only searches (more presicely, mathematical declarations only, excluding things like tactic parsers)
• Others want broader searches including metaprogramming and other libraries

Our current consideration is to:

1. Expand the database coverage (but a simple expansion may affect the searching quality)
2. Add configurable toggles for showing different declaration groups in searching results (these declaration groups could be: metaprogramming-related, Batteries library, instances, etc.)

We'd greatly appreciate any suggestions on:

• What toggles would be most useful
• Any alternative solutions beyond toggles

Thanks for bringing this up!

[Jiang Jiedong]

@Evgenia Karunus also discussed some related ideas with me.

[Eric Wieser]

If you want to exclude things like tactic parsers / metaprogramming, then probably dropping (or rather, filtering) things in the Lean namespace is a reasonable approximation. Dropping based on which folder things are in probably isn't a good heuristic.

[Kim Morrison]

Yes, you certainly want to index and return everything from Init.Data and Std.Data!

[Siddhartha Gadgil]

As a concrete example, for "If n is less than or equal to m, then $n+1$ is less than or equal to $m+1$" the result Nat.succ_le_succ does not show up and is the result I usually want. This is in the Lean core.

[Kim Morrison]

(Well, you want by omega, but sure. :-)

[Alok Singh]

Well, _I_ as a user want Std and Batteries to be searched.

[Kim Morrison]

LeanSearch is down.

[Adam Topaz]

I think it's also safe to say that any proposition no matter where it comes from should be indexed.

[Yaël Dillies]

Really? What about the lemmas internal to eg linarith?

[Tony Beta Lambda]

It is apparent that everyone has different needs, so instead of deciding it for everyone, how about we discuss and find out what set of filter options should be available to the user? Right now I can figure: packages to include, namespace, kind (tactic/prop/def).

[Kim Morrison]

I don't think there's that much variation asked for above.

Everyone wants everything that isn't internal to a tactic, or internal to Lean. (e.g. filter just by having .Tactic. in the namespace, or Lean.)

No one wants "auxiliary declarations", e.g. things starting with _.

I think just a single "metaprogramming" filter, and including the repositories upstream of Mathlib, would get most of the way.