lean-agent/.gitea/workflows/ci.yml

name: ci

# Runs on the ubuntu24.04-x64-lean4.35 runner: jobs execute on the host, Lean 4.35
# comes from /root/.elan, and there is no Node, so the commit is cloned with git
# instead of actions/checkout.

on:
  push:
    branches: [main, "ci/**"]
  pull_request:
  workflow_dispatch:

jobs:
  test:
    runs-on: ubuntu24.04-x64-lean4.35
    timeout-minutes: 20
    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 && git log --oneline -1

      - name: Lean
        run: |
          lean --version
          echo "project toolchain: $(cat lean-toolchain)"

      - name: Install
        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 --disable-pip-version-check -e .
          .venv/bin/lean-agent --help > /dev/null

      - name: Unit tests (real Lean verifier)
        run: .venv/bin/python -m unittest discover -s tests -v

      - name: CLI end to end (scripted provider, real Lean)
        run: |
          set -eu
          printf '%s\n' '{"id":"refl","statement":"∀ n : Nat, n + 0 = n"}' > task.json
          cat > provider.py <<'PY'
          import sys
          sys.stdin.read()
          print("intro n\nrfl")
          PY
          .venv/bin/lean-agent task.json --provider-command '["python3","provider.py"]' --attempts 2 | tee out.json
          grep -q '"success": true' out.json

      - name: With Mathlib (uses lean-bench's host cache, if present)
        run: |
          set -eu
          dir="$(ls -d /opt/lean-cache/leanbench-*/ 2>/dev/null | while read d; do [ -f "$d/.ready" ] && echo "$d"; done | tail -1)"
          if [ -z "$dir" ]; then
            echo "No ready Mathlib project on this host yet (lean-bench CI builds it); skipping."
            exit 0
          fi
          printf '%s\n' '{"id":"m","statement":"(2 : ℕ) + 2 = 4","prelude":"import Mathlib"}' > mtask.json
          cat > mprovider.py <<'PY'
          import sys
          sys.stdin.read()
          print("norm_num")
          PY
          .venv/bin/lean-agent mtask.json --provider-command '["python3","mprovider.py"]' \
            --lean-project "$dir" --lean-command '["lake","env","lean"]' --lean-timeout 300 | tee mout.json
          grep -q '"success": true' mout.json