内容
# 无模型本地MCP搜索，用于Lean仓库
无模型本地MCP搜索，用于Lean仓库。它使用`tree-sitter-lean`和SQLite FTS进行快速本地索引和语法定理搜索。
## 设置
```powershell
python -m venv .venv
.\.venv\Scripts\python.exe -m pip install -U pip
.\.venv\Scripts\python.exe -m pip install -r requirements.txt
```
如果`tree_sitter_lean`绑定丢失，请重建或将本地`tree-sitter-lean`包安装到此venv中。
## Codex MCP
```powershell
codex mcp add lean-local-search -- <mcp-repo>\.venv\Scripts\python.exe <mcp-repo>\tools\lean_local_search_mcp.py --repo <lean-project>
codex mcp get lean-local-search
```
服务器还识别项目别名，如`provider`、`highdimprob`、`main`和`mathlib`，当这些兄弟仓库存在于此仓库旁边时。
## 主要工具
- `index_repository`：使用`topic`、`path_prefix`、`path_filter`和`batch_size`进行增量/可恢复的索引。
- `index_visibility`：跟踪/未跟踪状态、过时文件和根导入暴露。
- `search_theorems` / `search_shape`：按名称、符号、结论和类型形状搜索定理。
- `theorem_card`：语句、导入、命名空间、源位置、类型类提示和最小`#check`。
- `proof_probe`：写入临时Lean文件并运行`lake env lean`；默认为紧凑输出，`verbose: true`用于完整打印。
- `consumer_fit` / `cross_repo_lookup`：提供者/main/Mathlib API可见性和迁移检查。
- `search_graph`、`search_code`、`get_context`、`cache_status`、`remove_project`。
## 典型调用
```json
{"name":"index_repository","arguments":{"project":"provider","mode":"full"}}
{"name":"index_repository","arguments":{"project":"mathlib","topic":"Matrix","mode":"resume"}}
{"name":"search_theorems","arguments":{"project":"mathlib","query":"cfc_eq eigenvalues diagonal IsHermitian","limit":5,"cards":true}}
{"name":"search_shape","arguments":{"project":"mathlib","shape":"Matrix.trace (cfc f A) = _","limit":5}}
{"name":"theorem_card","arguments":{"project":"mathlib","qualified_name":"Matrix.IsHermitian.trace_eq_sum_eigenvalues"}}
{"name":"proof_probe","arguments":{"project":"mathlib","run_project":"provider","checks":["Matrix.IsHermitian.trace_eq_sum_eigenvalues"]}}
{"name":"index_visibility","arguments":{"project":"provider","details":true,"detail_limit":10}}
```
## 验证
```powershell
.\.venv\Scripts\python.exe -m py_compile tools\lean_local_search_mcp.py tools\fuzz_mcp.py
.\.venv\Scripts\python.exe tools\fuzz_mcp.py --iterations 300 --seed 1700201
.\.venv\Scripts\python.exe tools\fuzz_mcp.py --iterations 80 --seed 1700202 --include-existing
```
