Files
codex-bot 16e49df764
ci / python (pull_request) Successful in 17s
ci / lean (pull_request) Successful in 1m21s
ci / image (pull_request) Has been skipped
fix(pilot): preserve partial results and stop on provider billing errors
2026-10-28 19:04:43 +08:00
..
2026-09-22 17:56:09 +00:00

__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 数值类型标准化。
  • 属性和注释处理。
  • 模型补充类型合并。
  • 无法解析时返回空结果。