Skip to content
Checks

Switch proof verification from SafeVerify to Comparator #95

Sign in to view logs

Switch proof verification from SafeVerify to Comparator

Switch proof verification from SafeVerify to Comparator #95

Workflow file for this run

.github/workflows/checks.yml at 50abda6
name: Checks
on:
pull_request:
push:
branches:
- main
jobs:
# The CI image tags (LeanOpenProblems_*_<version>) are keyed on
# apn.__version__, while the wheel build uses pyproject.toml's version. The two
# must stay in lockstep (scripts/bump_version.py edits both) -- this guards
# against a bump that touches only one of them.
check-version:
runs-on: ubuntu-24.04
steps:
- uses: actions/checkout@v4
- name: Install uv
uses: astral-sh/setup-uv@v5
with:
enable-cache: true
cache-dependency-glob: uv.lock
- name: Set up Python
uses: actions/setup-python@v5
with:
python-version-file: pyproject.toml
- name: Check apn.__version__ matches pyproject.toml
run: |-
version_from_init="$(python -c "import apn; print(apn.__version__)")"
echo "Version from apn/__init__.py: $version_from_init"
version_from_pyproject="$(uv version --short)"
echo "Version from pyproject.toml: $version_from_pyproject"
if [ "$version_from_init" != "$version_from_pyproject" ]; then
echo "Version mismatch between apn/__init__.py and pyproject.toml"
exit 1
fi
mypy:
runs-on: ubuntu-24.04
steps:
- uses: actions/checkout@v4
- name: Install uv
uses: astral-sh/setup-uv@v5
with:
enable-cache: true
cache-dependency-glob: uv.lock
- name: Set up Python
uses: actions/setup-python@v5
with:
python-version-file: pyproject.toml
- name: Install dependencies
run: uv sync
- name: Run mypy
run: uv run mypy
# The gold-proof sweep (~2h), the isolation suites (~55m compiling every
# committed spec in-container), and the comparator container tests (each
# single-file check builds+exports Challenge and Solution against Mathlib, so
# the suites run tens of minutes) each dwarf the fast pure-Python + mocked
# tests (~7m), so they run as their own jobs for early signal. All the
# container jobs build the Lean sandbox image from the Dockerfile in-test; a
# stock runner's ~14GB disk cannot hold that build.
tests:
runs-on: epoch-research-x64-64core-256GB-2040GB
steps:
- uses: actions/checkout@v4
- name: Install uv
uses: astral-sh/setup-uv@v5
with:
enable-cache: true
cache-dependency-glob: uv.lock
- name: Set up Python
uses: actions/setup-python@v5
with:
python-version-file: pyproject.toml
- name: Install dependencies
run: uv sync
- name: Run tests
run: >-
uv run pytest
--ignore=tests/test_gold_proofs.py
--ignore=tests/test_oeis_isolation.py
--ignore=tests/test_erdos_isolation.py
--ignore=tests/test_fc100_isolation.py
--ignore=tests/test_singlefile_proof.py
--ignore=tests/test_lean_vuln_e2e.py
--ignore=tests/test_comparator_security.py
--ignore=tests/test_comparator_primitives.py
# The comparator container tests: single-file acceptance, the vulnerability
# battery, the cross-attempt/disproof-shape security checks, and the
# primitive-constants invariant. Each check runs the real Comparator against
# the built image; split out so the fast `tests` job stays quick. (The pure-
# Python drift-candidate guard, tests/test_comparator_drift.py, stays in
# `tests` -- it needs no container.)
comparator-tests:
runs-on: epoch-research-x64-64core-256GB-2040GB
steps:
- uses: actions/checkout@v4
- name: Install uv
uses: astral-sh/setup-uv@v5
with:
enable-cache: true
cache-dependency-glob: uv.lock
- name: Set up Python
uses: actions/setup-python@v5
with:
python-version-file: pyproject.toml
- name: Install dependencies
run: uv sync
- name: Run the comparator container tests
run: >-
uv run pytest
tests/test_singlefile_proof.py
tests/test_lean_vuln_e2e.py
tests/test_comparator_security.py
tests/test_comparator_primitives.py
isolation:
runs-on: epoch-research-x64-64core-256GB-2040GB
steps:
- uses: actions/checkout@v4
- name: Install uv
uses: astral-sh/setup-uv@v5
with:
enable-cache: true
cache-dependency-glob: uv.lock
- name: Set up Python
uses: actions/setup-python@v5
with:
python-version-file: pyproject.toml
- name: Install dependencies
run: uv sync
- name: Run the isolation suites
run: >-
uv run pytest
tests/test_oeis_isolation.py
tests/test_erdos_isolation.py
tests/test_fc100_isolation.py
gold-proofs:
runs-on: epoch-research-x64-64core-256GB-2040GB
steps:
- uses: actions/checkout@v4
- name: Install uv
uses: astral-sh/setup-uv@v5
with:
enable-cache: true
cache-dependency-glob: uv.lock
- name: Set up Python
uses: actions/setup-python@v5
with:
python-version-file: pyproject.toml
- name: Install dependencies
run: uv sync
- name: Run the gold-proof sweep
run: uv run pytest tests/test_gold_proofs.py