backend: report query failures instead of encoding them

[dingf3ng]

Why

CoqInterface.search() is behind every Search / Print / Locate / About / Check / Print Assumptions query. It always returned a str, and encoded its failures as ordinary text:

aux_file not accessible · Query error: … · Empty query · No search term provided · Error executing print: … · Unsupported query type: …

_extract_search_results() went further and swallowed its exception entirely, returning whatever partial list it had — usually [] — as if the search had completed.

The consequence

Nothing downstream could tell "found nothing" from "broke".

CoqCommandSearch._create_search_result scores a result 1.0 unless its text contains the literal phrase "No results found". So a dead aux_file, or an LSP error mid-extraction, reached the LLM as a confident, high-relevance search hit whose content was an error message — and the agent reasoned over it.

What changed

search() and _run_aux_query() now return Optional[str]:

• success → the output
• failure → None, with the reason on self.last_error, read back via get_last_error()

That's the signal the class already uses for apply_tactic and reset_by_step. No new convention.

An empty result is a success, not a failure — it still returns "No results found.".

Keeping those apart in the Search path takes care, because _extract_search_results runs in a polling loop and must keep returning its partial list so retries still work. It now records the exception on last_error instead of dropping it, and the Search branch clears last_error before polling, then:

outcome	returns
results found	the results
empty + error recorded	None
empty, no error	"No results found."

skip_prefixes is deliberately untouched — it filters proof-goal noise out of legitimate hits, including lines Rocq itself emits starting with Error:. Separate, more ambiguous question.

One judgment call

The None case is handled in _create_search_result rather than at each of the eight CoqCommandSearch call sites, since all eight funnel through it — one place to get right instead of eight. A failed query becomes relevance_score=0.0 with metadata['failed'] set and content "Query failed: <reason>". interactive_session prints that content, so the reason still reaches a human.

Tests

tests/test_search_failures.py — no Rocq needed, runs in 2 seconds:

• extraction failure → None, cause on last_error
• genuinely empty search → still "No results found.", last_error unset
• every malformed-query path → None with the right reason
• all 8 CoqCommandSearch methods score a failure 0.0; a success stays 1.0