Inconsistency between #loogle command and web interface when parsing Set notation with wildcards
Valutazione
- Difficoltà
- 3/5
- Tempo stimato
- 1-2 giorni
- Idoneità per principianti
- 45/100
- Tipo di issue
- Bug
- Chiarezza
- Abbastanza chiara
- Stato di attività
- Ferma
- Ambito
- tooling
Direzione di ricerca
Inizia dal percorso di parsing o di convalida degli argomenti del comando #loogle in LeanSearchClient e riproduci #loogle Ideal.span {_, _} in VS Code. Confronta il comportamento e i risultati del client con l’interfaccia web di Loogle; il lavoro è completato quando la notazione degli insiemi con caratteri jolly viene accettata in modo coerente e produce un comportamento di ricerca corrispondente.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
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).
- Lingua principale
- Lean
- Stelle
- 37
- Fork
- 14
- Merge medio
- 2m
- PR unite (30g)
- 5
Preparare l'ambiente
Questo progetto non fornisce container di sviluppo, Dockerfile né guida per i contributori, quindi l'ambiente è a tuo carico: parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di leanprover-community/LeanSearchClient
-
HTTP 405: Leansearch down?Aperta
Difficoltà 4/5 3-5 giorni Idoneità per principianti 25/100
leanprover-community/LeanSearchClient#21 · 1 commento · 1 reazione ·
-
can this be run locally?Aperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
leanprover-community/LeanSearchClient#18 · 2 commenti ·
-
`#loogle` command's unexpected behavior when used with `#guard_msgs`Forse già presa @josaum l’ha presa 19 giorni fa. Aperta
Difficoltà 3/5 1-2 giorni Idoneità per principianti 35/100
Tutte le issue di leanprover-community/LeanSearchClient
Issue simili
-
needs-area-label
Difficoltà 2/5 1-3 ore Idoneità per principianti 66/100
I maintainer di solito rispondono entro 2 giorni
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
gitbutlerapp/gitbutler#16982 ·
I maintainer di solito rispondono entro 1 giorno
-
bug
Difficoltà 2/5 1-3 ore Idoneità per principianti 83/100
I maintainer di solito rispondono entro 2 giorni
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 76/100
TransformerLensOrg/TransformerLens#1980 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 79/100