leanprover-community / leanprover-community/LeanSearchClient
Inconsistency between #loogle command and web interface when parsing Set notation with wildcards
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 36
- Forks
- 13
- Avg merge
- 3m
- Merged PRs (30d)
- 4
Description
I encountered a parsing error when using the #loogle command in VS Code with a search pattern involving Set notation and wildcards (_). The same query works perfectly on the Loogle web interface, indicating a discrepancy in how the LeanSearchClient parses or validates arguments before sending them to the backend.
#loogle Ideal.span {_, _}
The command fails with message:
The command fails with the following error in the Info View: Loogle search failed with error: Cannot search for _. Did you forget to put a term pattern in parentheses?
Workaround using parentheses: #loogle (Ideal.span {_, _}) executes aswell as #loogle (Ideal.span ({_, _})) but returns different results compared to the web version (even with the parenthesis in the web version).
I am on some current, yet not the very newest version of mathlib (can check if relevant).
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start with the #loogle command's parsing or argument-validation path in LeanSearchClient and reproduce #loogle Ideal.span {_, _} in VS Code. Compare the client behavior and results with the Loogle web interface; done means Set notation with wildcards is accepted consistently and produces matching search behavior.
Written by the indexing model from the issue text.
Assessment
- Domain
- tooling
- Issue type
- Bug
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 45/100