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.
115 lines
4.0 KiB
YAML
115 lines
4.0 KiB
YAML
name: docker
|
|
|
|
# Builds the Lean 4 + Mathlib image and pushes it to this Gitea's container
|
|
# registry, so `docker pull gitea.entroia.com/<owner>/lean-bench` is all anyone
|
|
# needs in order to submit a book.
|
|
|
|
on:
|
|
push:
|
|
branches: [main]
|
|
tags: ["v*"]
|
|
workflow_dispatch:
|
|
inputs:
|
|
mathlib_rev:
|
|
description: "Mathlib revision (tag, branch, commit, or 'auto')"
|
|
required: false
|
|
default: "auto"
|
|
push_image:
|
|
description: "Push to the registry (false = build only)"
|
|
required: false
|
|
default: "true"
|
|
|
|
env:
|
|
REGISTRY: gitea.entroia.com
|
|
IMAGE_NAME: lean-bench
|
|
|
|
jobs:
|
|
image:
|
|
runs-on: ubuntu-latest
|
|
steps:
|
|
- uses: actions/checkout@v4
|
|
|
|
- name: Check the runner can build images
|
|
run: |
|
|
set -eu
|
|
if ! command -v docker >/dev/null; then
|
|
echo "::error::No docker CLI on this runner. Give the act_runner the host"
|
|
echo "::error::docker socket (-v /var/run/docker.sock:/var/run/docker.sock)"
|
|
echo "::error::or run it with the docker-in-docker image."
|
|
exit 1
|
|
fi
|
|
docker version
|
|
|
|
- name: Work out the tags
|
|
id: meta
|
|
run: |
|
|
set -eu
|
|
owner="$(echo "${{ github.repository_owner }}" | tr '[:upper:]' '[:lower:]')"
|
|
image="${REGISTRY}/${owner}/${IMAGE_NAME}"
|
|
ref="${GITHUB_REF_NAME:-main}"
|
|
sha="$(echo "${GITHUB_SHA:-unknown}" | cut -c1-12)"
|
|
case "${GITHUB_REF:-}" in
|
|
refs/tags/*) version="${ref}" ;;
|
|
*) version="${ref//\//-}" ;;
|
|
esac
|
|
{
|
|
echo "image=${image}"
|
|
echo "tags=${image}:${version} ${image}:sha-${sha}$([ "${ref}" = "main" ] && echo " ${image}:latest" || true)"
|
|
} >> "$GITHUB_OUTPUT"
|
|
echo "building ${image}:${version}"
|
|
|
|
- name: Log in to the registry
|
|
if: ${{ github.event_name != 'workflow_dispatch' || inputs.push_image == 'true' }}
|
|
run: |
|
|
set -eu
|
|
token='${{ secrets.GITEA_TOKEN }}'
|
|
[ -n "$token" ] || token='${{ secrets.GITHUB_TOKEN }}'
|
|
if [ -z "$token" ]; then
|
|
echo "::error::No token available to log in to ${REGISTRY}."
|
|
echo "::error::Add a GITEA_TOKEN secret with package:write scope."
|
|
exit 1
|
|
fi
|
|
echo "$token" | docker login "${REGISTRY}" -u '${{ github.actor }}' --password-stdin
|
|
|
|
- name: Build
|
|
run: |
|
|
set -eu
|
|
args=""
|
|
for tag in ${{ steps.meta.outputs.tags }}; do args="$args -t $tag"; done
|
|
docker build \
|
|
-f docker/Dockerfile \
|
|
--build-arg "MATHLIB_REV=${{ inputs.mathlib_rev || 'auto' }}" \
|
|
$args .
|
|
|
|
- name: Check the image actually works
|
|
run: |
|
|
set -eu
|
|
image="$(echo '${{ steps.meta.outputs.tags }}' | awk '{print $1}')"
|
|
docker run --rm "$image" doctor --skip-llm
|
|
docker run --rm --entrypoint bash "$image" -lc \
|
|
'cd $LEANBENCH_LEAN_PROJECT && printf "import Mathlib\ntheorem ci_smoke (n : Nat) : n + 0 = n := by simp\n" > /tmp/CI.lean && lake env lean /tmp/CI.lean && echo "lean+mathlib ok"'
|
|
|
|
- name: Push
|
|
if: ${{ github.event_name != 'workflow_dispatch' || inputs.push_image == 'true' }}
|
|
run: |
|
|
set -eu
|
|
for tag in ${{ steps.meta.outputs.tags }}; do
|
|
echo "pushing $tag"
|
|
docker push "$tag"
|
|
done
|
|
|
|
- name: Summary
|
|
if: always()
|
|
run: |
|
|
{
|
|
echo "### lean-bench image"
|
|
echo ""
|
|
for tag in ${{ steps.meta.outputs.tags }}; do echo "- \`$tag\`"; done
|
|
echo ""
|
|
echo "Pull and submit a book:"
|
|
echo '```'
|
|
echo "docker run --rm -e DASHSCOPE_API_KEY -v \$PWD/books:/books -v \$PWD/data:/data \\"
|
|
echo " ${{ steps.meta.outputs.image }}:latest ingest /books/your-book.pdf --pages 1-40"
|
|
echo '```'
|
|
} >> "$GITHUB_STEP_SUMMARY"
|