69 lines
2.6 KiB
YAML
69 lines
2.6 KiB
YAML
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]
|
||
workflow_dispatch:
|
||
|
||
jobs:
|
||
test:
|
||
if: gitea.ref == 'refs/heads/main'
|
||
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
|