Skip to content
Checks

Add the wikipedia, arxiv, and oeis_open datasets (FC research-open sweep) #120

Sign in to view logs

Add the wikipedia, arxiv, and oeis_open datasets (FC research-open sweep)

Add the wikipedia, arxiv, and oeis_open datasets (FC research-open sweep) #120

Workflow file for this run

.github/workflows/checks.yml at 3613289
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 of sequential SafeVerify checks) and the
# isolation suites (~55m compiling every committed spec in-container) each
# dwarf the rest of the suite (~7m), so they run as their own jobs for
# early signal. All three 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_erdos_autoformalized_isolation.py
--ignore=tests/test_fc100_isolation.py
--ignore=tests/test_fc_open_isolation.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_erdos_autoformalized_isolation.py
tests/test_fc100_isolation.py
tests/test_fc_open_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