diff --git a/tests/README.md b/tests/README.md new file mode 100644 index 0000000..722bf71 --- /dev/null +++ b/tests/README.md @@ -0,0 +1,107 @@ +[__init__.py](lean-bench/tests/__init__.py) +将测试目录标记为 Python package,本身为空。 + +[conftest.py](lean-bench/tests/conftest.py) +共享测试工具: +- 创建临时两页教材。 +- 构造检测 JSON 回复。 +- 构造形式化 JSON 回复。 +- 提供 fake Lean checker。 +- 提供其他 pytest fixtures。 + +[test_anchors.py](lean-bench/tests/test_anchors.py) +测试: +- 精确匹配。 +- 空白差异匹配。 +- 模糊匹配。 +- 首尾 span 组合。 +- 从 cursor 之后继续搜索。 +- 无法匹配时不猜测。 + +[test_config.py](lean-bench/tests/test_config.py) +测试 .env 行为: +- 文件不存在。 +- 注释、空行和引号。 +- 未设置变量从文件加载。 +- 真实环境变量优先。 +- 空环境变量不会遮蔽文件值。 + +[test_db.py](lean-bench/tests/test_db.py) +测试: +- 稳定 item ID。 +- 数据库存取。 +- upsert 不产生重复。 +- 更新条目时清除旧类型。 +- 按类型和角色搜索。 +- 查询跨页条目。 +- 删除页段和来源。 +- JSONL 导出。 +- 数据统计。 + +[test_detect.py](lean-bench/tests/test_detect.py) +测试: +- 单页检测和字符位置。 +- 跨页窗口扩展。 +- 达到窗口上限时标记 truncated。 +- 锚点无法解析时记录 unresolved。 +- 某页失败不会结束整批。 + +[test_document.py](lean-bench/tests/test_document.py) +测试: +- 页码从 1 开始。 +- 文本规范化。 +- 页面 checksum。 +- 跨页 slice。 +- 全局偏移与页内偏移相互转换。 + +[test_formalize.py](lean-bench/tests/test_formalize.py) +测试: +- 生成 Lean 与类型索引。 +- problem 只做 statement verification。 +- 真实 proof 如何计入 proved。 +- 编译失败后的修复重试。 +- 修复次数耗尽。 +- 模型主动跳过无法形式化内容。 +- 单条失败不影响批处理。 +- 清除代码正文中的 imports。 + +[test_llm.py](lean-bench/tests/test_llm.py) +测试: +- 解析纯 JSON。 +- 解析 fenced JSON。 +- 从额外说明文字中提取 JSON。 +- 无 JSON 时明确报错。 +- 提取 Lean 代码块。 +- ScriptedClient 回复耗尽时明确失败。 + +[test_ocr.py](lean-bench/tests/test_ocr.py) +测试量最大的模块,覆盖: +- 正常文本与乱码评分。 +- 特殊乱码字符。 +- 伪装成 ASCII 的损坏操作符。 +- 普通数字不被误判。 +- text、auto、ocr 模式。 +- OCR 页范围。 +- OCR 失败回退。 +- 全部 OCR 失败时报错。 +- 缓存读取、关闭和 cache key。 +- markdown fence 清理。 +- 视觉模型图片消息格式。 + +[test_pipeline.py](lean-bench/tests/test_pipeline.py) +测试完整流水线: +- 两页文档端到端入库。 +- 检测结果能按类型查询。 +- 局部重跑只替换指定起始页的记录。 +- 没有 Lean 时仍可存储,但不会声称 verified。 + +[test_typeindex.py](lean-bench/tests/test_typeindex.py) +测试: +- theorem 输入类型。 +- definition 自身类型。 +- structure 类型。 +- instance binder。 +- Unicode 数值类型标准化。 +- 属性和注释处理。 +- 模型补充类型合并。 +- 无法解析时返回空结果。 \ No newline at end of file