Replace Euclidean n/260 hardness scalar with a holographic-screen geo… #86
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: tests | |
| on: | |
| push: | |
| branches: [main, "claude/**"] | |
| pull_request: | |
| jobs: | |
| # Lane 1 -- unit-fast: portable, may skip solver-dependent tests if the external | |
| # binaries are unavailable (shutil.which -> None). Green does not by itself assert | |
| # that external certification executed; that is lane 2's job. | |
| unit-fast: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| python-version: ["3.11", "3.12"] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Set up Python ${{ matrix.python-version }} | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: ${{ matrix.python-version }} | |
| - name: Install Python dependencies | |
| run: | | |
| python -m pip install --upgrade pip | |
| pip install -r backend/requirements.txt | |
| # Best-effort: install the external solvers so the @requires_kissat | |
| # integration tests run too. If a package is unavailable the tests skip | |
| # gracefully (shutil.which -> None), so this lane stays green either way. | |
| - name: Install SAT solvers (best effort) | |
| run: sudo apt-get update && sudo apt-get install -y kissat drat-trim cadical || true | |
| pip install -e .[dev] | |
| - name: Run test suite | |
| run: python -m pytest backend/tests/ -q | |
| # Lane 2 -- certification-hard: Kissat + drat-trim are MANDATORY. This lane fails | |
| # red if the external certification path does not actually execute -- it is the | |
| # lane that stands behind the repo's headline claim (verify, don't trust). | |
| certification-hard: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Set up Python | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: "3.12" | |
| - name: Set up Python 3.11 | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: "3.11" | |
| - name: Install Python dependencies | |
| run: | | |
| python -m pip install --upgrade pip | |
| pip install -r backend/requirements.txt | |
| # Mandatory, NOT best-effort: no "|| true". If these are unavailable the lane | |
| # must fail rather than silently skip the certification it is guarding. | |
| - name: Install Kissat + drat-trim (mandatory) | |
| run: sudo apt-get update && sudo apt-get install -y kissat drat-trim | |
| - name: Assert the external tools are present | |
| run: | | |
| command -v kissat | |
| command -v drat-trim | |
| - name: Certification smoke (real DRAT UNSAT + model-replay SAT) | |
| run: python .github/scripts/certification_smoke.py | |
| - name: Certification-relevant tests must run (not skip) | |
| run: python -m pytest backend/tests/test_integration.py backend/tests/test_kissat_wrapper.py -q | |
| pip install -e .[dev] | |
| - name: Build SAT/proof tools | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y build-essential git | |
| git clone --depth 1 https://github.com/arminbiere/kissat.git /tmp/kissat | |
| cd /tmp/kissat | |
| ./configure | |
| make -j2 | |
| sudo cp build/kissat /usr/local/bin/kissat | |
| git clone --depth 1 https://github.com/marijnheule/drat-trim.git /tmp/drat-trim | |
| make -C /tmp/drat-trim -j2 | |
| sudo cp /tmp/drat-trim/drat-trim /usr/local/bin/drat-trim | |
| command -v kissat | |
| command -v drat-trim | |
| - name: Run strict certification smoke tests | |
| run: | | |
| set +e | |
| python -m backend.cli examples/simple_sat.cnf --mode strict | |
| sat_code=$? | |
| python -m backend.cli examples/simple_unsat.cnf --mode strict | |
| unsat_code=$? | |
| test "$sat_code" -eq 10 | |
| test "$unsat_code" -eq 20 | |
| - name: Run full test suite with tools installed | |
| run: python -m pytest backend/tests/ -q |