lean-bench/tests/README.md

__init__.py 将测试目录标记为 Python package，本身为空。

conftest.py 共享测试工具：

• 创建临时两页教材。
• 构造检测 JSON 回复。
• 构造形式化 JSON 回复。
• 提供 fake Lean checker。
• 提供其他 pytest fixtures。

test_anchors.py 测试：

• 精确匹配。
• 空白差异匹配。
• 模糊匹配。
• 首尾 span 组合。
• 从 cursor 之后继续搜索。
• 无法匹配时不猜测。

test_config.py 测试 .env 行为：

• 文件不存在。
• 注释、空行和引号。
• 未设置变量从文件加载。
• 真实环境变量优先。
• 空环境变量不会遮蔽文件值。

test_db.py 测试：

• 稳定 item ID。
• 数据库存取。
• upsert 不产生重复。
• 更新条目时清除旧类型。
• 按类型和角色搜索。
• 查询跨页条目。
• 删除页段和来源。
• JSONL 导出。
• 数据统计。

test_detect.py 测试：

• 单页检测和字符位置。
• 跨页窗口扩展。
• 达到窗口上限时标记 truncated。
• 锚点无法解析时记录 unresolved。
• 某页失败不会结束整批。

test_document.py 测试：

• 页码从 1 开始。
• 文本规范化。
• 页面 checksum。
• 跨页 slice。
• 全局偏移与页内偏移相互转换。

test_formalize.py 测试：

• 生成 Lean 与类型索引。
• problem 只做 statement verification。
• 真实 proof 如何计入 proved。
• 编译失败后的修复重试。
• 修复次数耗尽。
• 模型主动跳过无法形式化内容。
• 单条失败不影响批处理。
• 清除代码正文中的 imports。

test_llm.py 测试：

• 解析纯 JSON。
• 解析 fenced JSON。
• 从额外说明文字中提取 JSON。
• 无 JSON 时明确报错。
• 提取 Lean 代码块。
• ScriptedClient 回复耗尽时明确失败。

test_ocr.py 测试量最大的模块，覆盖：

• 正常文本与乱码评分。
• 特殊乱码字符。
• 伪装成 ASCII 的损坏操作符。
• 普通数字不被误判。
• text、auto、ocr 模式。
• OCR 页范围。
• OCR 失败回退。
• 全部 OCR 失败时报错。
• 缓存读取、关闭和 cache key。
• markdown fence 清理。
• 视觉模型图片消息格式。

test_pipeline.py 测试完整流水线：

• 两页文档端到端入库。
• 检测结果能按类型查询。
• 局部重跑只替换指定起始页的记录。
• 没有 Lean 时仍可存储，但不会声称 verified。

test_typeindex.py 测试：

• theorem 输入类型。
• definition 自身类型。
• structure 类型。
• instance binder。
• Unicode 数值类型标准化。
• 属性和注释处理。
• 模型补充类型合并。
• 无法解析时返回空结果。