feat: local Lean project search + CSLib search tools

[KrystianNowakowski]

What

Adds two project-local search tools the remote Mathlib LeanSearch doesn't cover, plus the declaration-parsing robustness they need:

• search_lean_local — searches the project's own .lean files for declarations by name (namespace-qualified, modifier/attribute-aware), with a body-search fallback for identifiers that aren't declaration names (e.g. where/let rec helpers, constructors).
• search_cslib — searches the vendored CSLib dependency under .lake/packages/cslib, which local search excludes and Mathlib search doesn't index.
• Shared lean_parsing.py improvements: modifier/attribute prefixes (private, @[simp], …), namespace-qualified names, and per-simple-name occurrence disambiguation.
• Proposer-prompt routing: pick the search tool by the file's imports — Mathlib.* → search_lean_search_tool, Cslib.* → search_cslib_tool, other/local imports → search_lean_local_tool.

Code-review fixes included

This branch also carries the search/parsing fixes from the experiment-branch review:

• DECL_NAME_END accepts universe-polymorphic names (theorem foo.{u}).
• extract_function_from_content keeps a leading open … in (and other … in) command prefix instead of dropping it.
• Comment-stripping vs raw-content occurrence misalignment fixed (comment_spans/non_comment_matches): a declaration keyword inside a comment no longer shifts occurrence indices.
• _format_results always shows at least the first match (truncated with a marker) instead of returning zero bodies when the only match exceeds max_chars.
• Local/CSLib search reads each .lean file once per query (single walk shared with the body fallback) instead of twice on a name-miss.
• TemporaryProposal resolves the target's namespace-qualified occurrence (resolve_target_occurrence) instead of always extracting occurrence 0.

Tests

Full unit suite passes on the branch; ruff clean. Includes dedicated tests for both tools (isolation, namespaces, duplicate names, modifiers, body fallback, edge cases) and for each fix above.

🤖 Generated with Claude Code

---

Note

Medium Risk
Changes the default prover tool set and proposer context (verbatim definition injection) plus shared Lean parsing used when applying proposals; broad surface area but covered by extensive unit tests and bounded caching behavior.

Overview
Adds local Lean search (search_lean_local) over the project’s own .lean files and CSLib search (search_cslib) under .lake/packages/cslib, both built on a shared _search_root pipeline: exact name match, then body-identifier fallback (e.g. where helpers), then fuzzy name suggestions when still empty.

Prover integration: default config registers both tools; create_tool can pass base_folder into scoped searchers. The proposer is told to pick search by imports (Mathlib vs CSLib vs local). WS1 caching records what local search returned, intersects with identifiers used in the latest proposal, stores append-only used_definitions on graph state, and injects a bounded <local-definitions> block so the agent need not re-query the same defs each iteration.

Parsing/build fixes supporting search and apply: declaration prefixes (private, @[simp], …), qualified names and occurrence disambiguation, comment-aware matching, open … in prefixes in extracted blocks, universe .{u} name boundaries, single file read per query, and resolve_target_occurrence when applying proposals.

Also adds Claude Opus 4.7/4.8 LLM configs and ablation YAMLs, pins langchain-anthropic via a git rev in pyproject.toml, plus design/implementation docs for the search workstreams.

^{Reviewed by Cursor Bugbot for commit b9e7989. Bugbot is set up for automated code reviews on this repo. Configure here.}

[cursor]

Cursor Bugbot has reviewed your changes and found 2 potential issues.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit a33b203. Configure here.}