Native Backends Tier 2 #2
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: Native Backends Tier 2 | |
| on: | |
| schedule: | |
| - cron: '0 7 * * 1' | |
| workflow_dispatch: | |
| jobs: | |
| native-backend: | |
| runs-on: ubuntu-latest | |
| continue-on-error: true | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| backend: [tla, kani, dafny, verus, lean, alloy] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.11' | |
| - name: Cache cargo registry | |
| if: matrix.backend == 'kani' | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| key: cargo-${{ matrix.backend }}-${{ runner.os }} | |
| - name: Install backend | |
| run: bash scripts/ci/install_backend.sh ${{ matrix.backend }} | |
| continue-on-error: true | |
| - name: Install package | |
| run: pip install -e '.[dev]' | |
| - name: Run native backend tests | |
| run: pytest tests/test_native_backends.py -m native_backend -v -k ${{ matrix.backend }} | |
| env: | |
| OVK_NATIVE_BACKEND: ${{ matrix.backend }} | |
| native-backends-report: | |
| runs-on: ubuntu-latest | |
| needs: native-backend | |
| if: always() | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.11' | |
| - name: Install package | |
| run: pip install -e '.[dev]' | |
| - name: Write install status summary | |
| run: | | |
| python - <<'PY' >> "$GITHUB_STEP_SUMMARY" | |
| from ovk.core.native_backend_probe import probe_all_native_backends | |
| tier2 = {"tla+", "kani", "dafny", "verus", "lean", "alloy"} | |
| print("## Native Backend Tier 2 (informational)") | |
| print("| Backend | Binary | Contract | Native Used | Fixture Match |") | |
| print("|---------|--------|----------|-------------|---------------|") | |
| for result in probe_all_native_backends(): | |
| if result.backend not in tier2: | |
| continue | |
| print( | |
| f"| {result.backend} | " | |
| f"{'yes' if result.binary_present else 'no'} | " | |
| f"{'ok' if result.contract_roundtrip_ok else 'fail'} | " | |
| f"{result.native_binary_used} | " | |
| f"{result.fixture_matches_oracle} |" | |
| ) | |
| PY |