Zayden-Jung
d3555d9a52
Replaces the previous tree entirely. The pipeline is four separable pieces, each
testable on its own:
1. leanbench/llm.py provider-neutral OpenAI-compatible connector, stdlib only,
with retries, JSON coercion and a scripted client so the
rest of the code is testable without a network.
2. leanbench/detect.py per-page detection of formalizable mathematics. Case 1 is
mathematics asserted as fact (definition/theorem/lemma/...,
deliberately not sub-classified); case 2 is a problem left
open to the reader. Hits come back as spans -- start page
and index, end page and index -- so several per page is
normal. A hit cut off by the page end makes the detector
re-read that page together with the next, repeatedly, so an
item spread over three pages is found whole.
Offsets come from verbatim quotes resolved by
leanbench/anchors.py (exact -> whitespace-insensitive ->
fuzzy), because models quote well and count badly.
3. leanbench/formalize.py + leanbench/verify.py
each span becomes one Lean 4 declaration, judged by the real
compiler: full elaboration for case 1, statement legality
only for case 2, which has no proof to check. Lean's own
diagnostics feed back for a repair attempt. "verified" (Lean
accepted it) and "proved" (accepted with no sorry) are kept
strictly apart.
4. leanbench/db.py indexed SQLite plus JSONL export. Every item is indexed by
the types of its inputs, or by its own type when it is not a
proof, and records the source book (sha256) and the page it
starts on -- so `drop --source H --pages A-B` followed by a
re-ingest redoes exactly those pages and nothing else.
Also: lean/ Lake project pinned to Mathlib, docker/ image carrying Lean 4 and a
prebuilt Mathlib (the Mathlib revision and the toolchain are resolved against each
other at build time rather than both hardcoded), and .gitea/workflows for tests,
image build and push to the Gitea registry, and a manual "submit a book" run.
58 tests; they need neither network nor Lean.
63 lines
1.8 KiB
YAML
63 lines
1.8 KiB
YAML
name: ci
|
|
|
|
on:
|
|
push:
|
|
branches: [main]
|
|
pull_request:
|
|
workflow_dispatch:
|
|
|
|
jobs:
|
|
test:
|
|
runs-on: ubuntu-latest
|
|
steps:
|
|
- uses: actions/checkout@v4
|
|
|
|
- name: Ensure Python
|
|
run: |
|
|
set -eu
|
|
if ! command -v python3 >/dev/null; then
|
|
apt-get update
|
|
apt-get install -y --no-install-recommends python3 python3-pip python3-venv
|
|
fi
|
|
python3 --version
|
|
|
|
- name: Install
|
|
run: |
|
|
set -eu
|
|
PIP="python3 -m pip"
|
|
# Debian/Ubuntu mark the system Python as externally managed; this is a
|
|
# throwaway CI container, so installing into it is fine.
|
|
$PIP install --break-system-packages --upgrade pip \
|
|
|| $PIP install --upgrade pip
|
|
$PIP install --break-system-packages -e ".[dev]" \
|
|
|| $PIP install -e ".[dev]"
|
|
|
|
- name: Lint
|
|
run: python3 -m ruff check .
|
|
|
|
- name: Test
|
|
run: python3 -m pytest -q
|
|
|
|
- name: Pipeline smoke test (no network, no Lean)
|
|
run: python3 -m pytest -q tests/test_pipeline.py
|
|
|
|
- name: CLI is wired up
|
|
run: |
|
|
python3 -m leanbench.cli --help
|
|
python3 -m leanbench.cli doctor --skip-llm --env /dev/null
|
|
|
|
lean-project:
|
|
# Cheap guard: the Lean project's pins must at least resolve.
|
|
runs-on: ubuntu-latest
|
|
steps:
|
|
- uses: actions/checkout@v4
|
|
- name: Resolve the Mathlib / toolchain pair
|
|
run: |
|
|
set -eu
|
|
command -v curl >/dev/null || (apt-get update && apt-get install -y curl)
|
|
command -v git >/dev/null || (apt-get update && apt-get install -y git)
|
|
chmod +x docker/resolve-mathlib.sh
|
|
docker/resolve-mathlib.sh lean "${MATHLIB_REV:-auto}"
|
|
echo "toolchain: $(cat lean/lean-toolchain)"
|
|
grep -n 'rev' lean/lakefile.toml
|