diff --git a/.gitea/scripts/prepare-mathlib.sh b/.gitea/scripts/prepare-mathlib.sh new file mode 100755 index 0000000..f407a58 --- /dev/null +++ b/.gitea/scripts/prepare-mathlib.sh @@ -0,0 +1,40 @@ +#!/usr/bin/env bash +# Keep a ready Lean + Mathlib project on the runner host, keyed by the project's +# toolchain and lakefile, so only the first job pays for the multi-GB cache fetch. +# +# prepare-mathlib.sh prints the cached project path +# +# The runner executes jobs on the host (no container), so /opt/lean-cache persists +# between jobs. A flock serialises concurrent jobs; .ready is written last, so an +# interrupted preparation is redone rather than trusted. +set -euo pipefail + +SRC="${1:?usage: prepare-mathlib.sh }" +ROOT="${LEAN_CACHE_ROOT:-/opt/lean-cache}" +KEY="$(cat "$SRC/lean-toolchain" "$SRC/lakefile.toml" | sha256sum | cut -c1-12)" +DIR="$ROOT/leanbench-$KEY" + +mkdir -p "$ROOT" +exec 9>"$ROOT/.lock" +flock 9 + +if [ -f "$DIR/.ready" ]; then + echo "prepare-mathlib: reusing $DIR" >&2 +else + echo "prepare-mathlib: building $DIR (first run on this toolchain/lakefile)" >&2 + rm -rf "$DIR" + cp -r "$SRC" "$DIR" + cd "$DIR" + elan toolchain install "$(cat lean-toolchain)" >&2 + timeout 1800 lake update >&2 + timeout 5400 lake exe cache get >&2 + start=$(date +%s) + timeout 1200 lake env lean LeanBench.lean >&2 || { + status=$? + [ "$status" -eq 124 ] && echo "prepare-mathlib: 'import Mathlib' timed out; check RAM (free -h)" >&2 + exit "$status" + } + echo "prepare-mathlib: import Mathlib elaborated in $(( $(date +%s) - start ))s" >&2 + touch .ready +fi +echo "$DIR" diff --git a/.gitea/workflows/ci.yml b/.gitea/workflows/ci.yml index 5cf5a16..7eb9322 100644 --- a/.gitea/workflows/ci.yml +++ b/.gitea/workflows/ci.yml @@ -1,33 +1,42 @@ name: ci +# Runs on the ubuntu24.04-x64-lean4.35 runner. That runner executes jobs directly on +# the host (no job container): Lean 4.35 lives in /root/.elan, Python 3.12 is the +# system Python, and there is no Node, so actions/checkout cannot run -- each job +# clones the commit with git instead. +# +# python lint + unit tests (LLM scripted, Lean faked), every push +# lean the real pipeline against real Lean + Mathlib (host-cached project) +# image only after both pass: build the Docker image, smoke-test it, keep it + on: push: - branches: [main] + branches: [main, "ci/**"] pull_request: workflow_dispatch: +env: + PIP_DISABLE_PIP_VERSION_CHECK: "1" + jobs: python: - runs-on: gitea-cicd-server-for-CODEX - container: node:22-bookworm - timeout-minutes: 30 + runs-on: ubuntu24.04-x64-lean4.35 + timeout-minutes: 20 steps: - - uses: actions/checkout@v4 + - name: Check out + run: | + set -eu + git init -q . && git remote add origin "${{ github.server_url }}/${{ github.repository }}.git" + git -c http.extraHeader="Authorization: token ${{ github.token }}" fetch -q --depth 1 origin "${{ github.sha }}" + git checkout -q FETCH_HEAD && git log --oneline -1 - # The runner label defaults to node:16-bullseye, whose Python 3.9 is too - # old and whose Debian repositories are retired. A Bookworm job image - # keeps Node available for JavaScript actions and provides Python 3.11. - name: Set up Python run: | set -eu - apt-get update -qq - apt-get install -y -qq python3-venv - python3 --version - python3 -m venv .venv + python3 -m venv .venv 2>/dev/null || { apt-get update -qq && apt-get install -y -qq python3-venv && python3 -m venv .venv; } + .venv/bin/python --version .venv/bin/python -m pip install --quiet --upgrade pip - - - name: Install - run: .venv/bin/python -m pip install -e ".[dev]" + .venv/bin/python -m pip install --quiet -e ".[dev]" - name: Lint run: .venv/bin/python -m ruff check . @@ -35,8 +44,97 @@ jobs: - name: Test run: .venv/bin/python -m pytest -q - - name: Check the CLI entry point + - name: CLI entry point run: | - set -eu .venv/bin/lean-bench --help > /dev/null .venv/bin/lean-bench doctor --skip-llm --env /dev/null + + lean: + needs: python + runs-on: ubuntu24.04-x64-lean4.35 + timeout-minutes: 150 + steps: + - name: Check out + run: | + set -eu + git init -q . && git remote add origin "${{ github.server_url }}/${{ github.repository }}.git" + git -c http.extraHeader="Authorization: token ${{ github.token }}" fetch -q --depth 1 origin "${{ github.sha }}" + git checkout -q FETCH_HEAD + + - name: Host environment + run: | + echo "host=$(hostname) cpus=$(nproc)"; free -h; df -h / + elan --version; lean --version; lake --version + + - name: Lean + Mathlib (cached on the host) + run: | + set -eu + dir="$(.gitea/scripts/prepare-mathlib.sh lean)" + echo "LEANBENCH_LEAN_PROJECT=$dir" >> "$GITHUB_ENV" + cd "$dir" && time lake env lean LeanBench.lean && echo "Mathlib OK in $dir" + + - name: End-to-end smoke (real Lean, scripted LLM) + run: | + set -eu + python3 -m venv .venv 2>/dev/null || { apt-get update -qq && apt-get install -y -qq python3-venv && python3 -m venv .venv; } + .venv/bin/python -m pip install --quiet . + .venv/bin/python docker/smoke.py + + image: + needs: [python, lean] + if: github.event_name != 'pull_request' + runs-on: ubuntu24.04-x64-lean4.35 + timeout-minutes: 180 + steps: + - name: Check out + run: | + set -eu + git init -q . && git remote add origin "${{ github.server_url }}/${{ github.repository }}.git" + git -c http.extraHeader="Authorization: token ${{ github.token }}" fetch -q --depth 1 origin "${{ github.sha }}" + git checkout -q FETCH_HEAD + + - name: Ensure Docker on the runner host + run: | + set -eu + if ! command -v docker >/dev/null; then + echo "Docker not installed; installing docker.io + docker-buildx from Ubuntu" + apt-get update -qq + DEBIAN_FRONTEND=noninteractive apt-get install -y -qq docker.io docker-buildx + systemctl enable --now docker + fi + docker version --format 'client {{.Client.Version}} / server {{.Server.Version}}' + docker info --format 'storage={{.Driver}} root={{.DockerRootDir}}' + + - name: Preflight (disk, memory) + run: | + set -eu + free_gb=$(df -BG --output=avail "$(docker info --format '{{.DockerRootDir}}' | xargs dirname)" | tail -1 | tr -dc 0-9) + mem_gb=$(awk '/MemTotal/ {print int($2/1048576)}' /proc/meminfo) + echo "free disk ${free_gb} GB, memory ${mem_gb} GB" + [ "$free_gb" -ge 30 ] || { echo "need >= 30 GB free for a ~16 GB image"; exit 1; } + [ "$mem_gb" -ge 7 ] || { echo "need >= 8 GB RAM to elaborate Mathlib"; exit 1; } + + - name: Build + run: | + set -eu + short="$(git rev-parse --short HEAD)" + echo "SHORT=$short" >> "$GITHUB_ENV" + DOCKER_BUILDKIT=1 docker build --progress=plain -f docker/Dockerfile \ + -t "lean-bench:sha-$short" -t "lean-bench:lean4.35" . + + - name: Smoke-test the image (real Lean inside) + run: docker run --rm -i --entrypoint python3 "lean-bench:sha-$SHORT" - < docker/smoke.py + + - name: Keep the image + run: | + set -eu + if [ "${{ github.ref }}" = "refs/heads/main" ]; then + docker tag "lean-bench:sha-$SHORT" lean-bench:latest + docker tag "lean-bench:sha-$SHORT" lean-bench:main + fi + docker images lean-bench --format 'table {{.Repository}}:{{.Tag}}\t{{.ID}}\t{{.Size}}\t{{.CreatedSince}}' + { + echo "### lean-bench image kept on $(hostname)" + echo + docker images lean-bench --format '- `{{.Repository}}:{{.Tag}}` {{.ID}} ({{.Size}})' + } >> "${GITHUB_STEP_SUMMARY:-/dev/null}" diff --git a/lean/lakefile.toml b/lean/lakefile.toml index de43134..49480db 100644 --- a/lean/lakefile.toml +++ b/lean/lakefile.toml @@ -6,7 +6,7 @@ defaultTargets = ["LeanBench"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" -rev = "v4.33.1" +rev = "v4.35.0" [[lean_lib]] name = "LeanBench" diff --git a/lean/lean-toolchain b/lean/lean-toolchain index a8afa7d..a6aff06 100644 --- a/lean/lean-toolchain +++ b/lean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.1 +leanprover/lean4:v4.35.0