Repository navigation
autoform search refinements from the #171 review #200
Description
Four small items from the final review of #171 at 22d1c02. None gives a wrong result on an ordinary query.
--declarationrefuses a union when one kind is unused.autoform search foo --declaration theorem --declaration instanceon a blueprint with theorems and no instances exits 2 and returns none of the theorem hits. The skills tell agents that exit 2 means "do not add the article", so this blocks a legitimate query. Refuse only when every requested kind is unused, or warn on stderr and exit 0.- A primed name does not rank its owner first when the unprimed name also exists. With
Project.fooandProject.foo'both declared, the queryProject.foo'ranks the owner ofProject.foofirst on the node-ID tie-break. An exact match on the query word as typed, used as an extra tie-break, would fix it. - A space inside
«»turns a namespace into aleanmatch. Withlean: Project.«weird name».bar, the queryProject.weirdreturns the article withmatched_fieldsoflean; it should bequalified_names. The index joins names with a space; a separator that cannot occur in a name, such as a newline, fixes it. - The README's "Search contract" lists the filler words and stemming rules. That makes any later tuning a contract change. State that the JSON shape is the contract and the matching rules may change.
Activity
Deicyde commentedon Oct 13, 2026
Triage note: all four items look small (about 85 changed lines with tests), and nobody has claimed them. One coordination point first: draft #204 edits the same
_rankslookup insearch.py, and its newlibrary/search.pybuildslean_nameswith a trailing space. Item 3's fix ends each name with a newline instead, so whichever of the two lands second has to switch that separator, or library Lean-name matches quietly fall back to weaker fields. Folding these items into #204 would avoid that.A sketch, in case it helps:
--declaration theorem --declaration lemmma) is then dropped without a refusal.max(ranks), rank first an owner whose Lean name a query word spells in full, primes,?and!included. That needs an unquoting helper split out of_lean_name, because_QUOTINGstrips those marks.\ninlean_namesand in the_rankslookup, and also add the unquoted names toqualified_names; with the separator change alone,Project.weirdmatches nothing.Posted by issue triage
Deicyde commentedon Oct 15, 2026
@zibo-yang, a plan for the site search that touches the matching code this issue covers, and a question before anyone starts on it.
Context. #90 (the Canvas dependency explorer) has its own search box over
dependencies/index.json, which matches differently fromautoform search. #90 also shipped a title-only MkDocs search hook, which turned out to drop article titles from Material's header search. #90 will delete that hook, so header search works as it does onmain.Plan: a follow-up PR after #90, "Site search follows
autoform search".search.pybecomes the single definition of what matches, for both the CLI and the explorer.search.pyexposes its field builder as a public pure function, plus a small JSON spec of the matcher's rules (filler words, word endings, quoting, punctuation, casefolding). CLI output does not change, andlibrary/search.pymoves to the public names.search_blueprint's order.Question. Should the four fixes in this issue land first, so the port copies the final rules? Item 4 matters most here. If the README states that the JSON shape is the contract and the matching rules may change, the generated tables can follow the rules instead of freezing them. If you'd rather build the follow-up yourself, say so; it is your code.
Posted by PR swarm: Swarm Manager
Deicyde commentedon Oct 19, 2026
The site-search plan from the comment above now lives in #393, so it stays tracked after #376 closes this issue.