Repository navigation
ci(abi): gate the Idris2 proofs on every PR, with module-shaped paths #150
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
| # SPDX-License-Identifier: MPL-2.0 | |
| # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> | |
| # | |
| # proven-tests.yml — the estate's evidence-graded test framework, wired. | |
| # | |
| # THE JOBS DO DIFFERENT THINGS AND NONE PRETENDS TO BE ANOTHER | |
| # --------------------------------------------------------------------- | |
| # `ledger` (every PR, blocking, minutes): derives a proven-tests run report from | |
| # THIS repo's suite — from a test inventory the runner emitted in the same | |
| # commit — and then feeds that report to `panic-attack aggregate | |
| # --proven-tests --fail-on-defect`, which applies the tier->verdict mapping and | |
| # refuses claims the report's own contents do not support (an Actually-Proven | |
| # entry with no ladder, a ladder step citing a file that is not there, a | |
| # summary that disagrees with the entries). A cell with no executed test is a | |
| # gate failure, not a rounding error. | |
| # | |
| # `framework` (schedule and dispatch only, tens of minutes): builds the | |
| # `proven-tests-and-benches` framework itself from a pinned commit with its | |
| # own Idris2 toolchain and runs its suite, so the *grader* is exercised rather | |
| # than trusted. This is deliberately off the PR path: bootstrapping Idris2 for | |
| # every pull request buys nothing that the ledger job does not already prove, | |
| # and it would make every contributor wait on a compiler that cannot change | |
| # for them. | |
| # | |
| # `abi-proofs` (every PR, blocking): type-checks this repository's own Idris2 | |
| # proofs in src/abi with the same pinned Idris2. It reuses the framework job's | |
| # toolchain cache, so it costs a compiler build only on a cold cache. | |
| # | |
| # WHY THE REPORT IS A FILE, NOT A PARAGRAPH: docs/INTEROP-PANIC-ATTACK.adoc in | |
| # proven-tests-and-benches fixes the mapping in prose; a report plus a verifier | |
| # is the same mapping with something at stake. | |
| name: Proven Tests | |
| on: | |
| pull_request: | |
| branches: ['**'] | |
| push: | |
| branches: [main, master] | |
| schedule: | |
| - cron: '41 4 * * 1' # Mondays, off the hour | |
| workflow_dispatch: | |
| permissions: | |
| contents: read | |
| concurrency: | |
| group: proven-tests-${{ github.ref }} | |
| cancel-in-progress: true | |
| env: | |
| # Pinned: the framework commit this repo's ledger was written against. | |
| PROVEN_TESTS_PIN: eca682bcd419554f6779e72969902e6faef4fd9d | |
| IDRIS2_VERSION: '0.7.0' | |
| jobs: | |
| ledger: | |
| name: Ledger — coverage derived from executed tests | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 30 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Install Rust toolchain | |
| uses: dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8 # v1 | |
| with: | |
| toolchain: stable | |
| - uses: Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0 # v2.9.3 | |
| with: | |
| key: proven-ledger | |
| # The suite must PASS before a report may claim anything about it: a | |
| # `result: passed` field written by a job that never ran the tests is | |
| # exactly the dishonesty this framework exists to remove. | |
| - name: Run the suite | |
| run: bash scripts/ci/annotate.sh "proven:suite" -- cargo test --locked --no-fail-fast | |
| - name: Inventory the tests that exist | |
| run: bash scripts/proven/inventory.sh /tmp/inventory.json | |
| - name: Derive the run report (cells must select real tests) | |
| run: | | |
| bash scripts/ci/annotate.sh "proven:ledger" -- \ | |
| bash scripts/proven/verify-ledger.sh \ | |
| --inventory /tmp/inventory.json \ | |
| --ledger proven/ledger.json \ | |
| --root . \ | |
| --out /tmp/proven-report.json | |
| - name: Build panic-attack | |
| run: cargo build --locked --release | |
| # The interop, actually executed: our own tool reads the framework's | |
| # report, applies the mapping in code, and fails on an unsupported claim. | |
| - name: Fold the report through aggregate --fail-on-defect | |
| run: | | |
| set -euo pipefail | |
| bash scripts/ci/annotate.sh "proven:aggregate" -- \ | |
| ./target/release/panic-attack aggregate \ | |
| --proven-tests /tmp/proven-report.json \ | |
| --proven-tests-root . \ | |
| --fail-on-defect \ | |
| --output /tmp/proven-aggregate.json | |
| jq -e '.proven_tests | type == "array" and length == 1 and (.[0].defects == []) and (.[0].summary.total | type == "number" and . > 0)' /tmp/proven-aggregate.json > /dev/null | |
| jq -r '.proven_tests[0].summary | "proven-tests: \(.passed)/\(.total) passed, \(.covered_cells)/\(.cat_aspect_cells) cells, \(.actually_proven) actually-proven"' /tmp/proven-aggregate.json | |
| - name: Publish to the job summary | |
| if: always() | |
| run: | | |
| { | |
| echo "## Proven-tests ledger" | |
| echo "" | |
| if [ -f /tmp/proven-report.json ]; then | |
| python3 - <<'PY' >> "$GITHUB_STEP_SUMMARY" | |
| import json | |
| r = json.load(open('/tmp/proven-report.json')) | |
| s = r['summary'] | |
| print(f"**{s['passed']}/{s['total']}** executed tests, " | |
| f"**{s['covered_cells']}/{s['cat_aspect_cells']}** category×aspect cells") | |
| print("") | |
| print(f"| tier | tests |\n|---|---|") | |
| print(f"| Actually-Proven | {s['actually_proven']} |") | |
| print(f"| Provisionally-Proven | {s['provisionally_proven']} |") | |
| print(f"| Unproven | {s['unproven']} |") | |
| print("") | |
| print("Cells declared absent, with the command that would test them, are in") | |
| print("`proven/ledger.json` — a to-do list, not a silencer.") | |
| PY | |
| else | |
| echo "_the report was not produced; see the failed step above_" | |
| fi | |
| } >> "$GITHUB_STEP_SUMMARY" | |
| - name: Upload the run report | |
| if: always() | |
| uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2 | |
| with: | |
| name: proven-report | |
| path: | | |
| /tmp/proven-report.json | |
| /tmp/proven-aggregate.json | |
| retention-days: 30 | |
| if-no-files-found: warn | |
| abi-proofs: | |
| # Every PR: type-check this repo's own Idris2 ABI proofs (src/abi). Without | |
| # this, src/abi/PanicAttack/ABI/Stripping.idr sat on main not compiling | |
| # while PROOF-NEEDS.adoc called it closed. The toolchain comes from the same | |
| # pinned installer and cache key as the framework job, so a warm cache makes | |
| # this a type-check, not a compiler build. | |
| name: Idris2 — src/abi proofs type-check | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 60 | |
| steps: | |
| - name: Checkout this repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Checkout proven-tests-and-benches at the pinned commit | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| repository: hyperpolymath/proven-tests-and-benches | |
| ref: ${{ env.PROVEN_TESTS_PIN }} | |
| path: .proven-tests | |
| persist-credentials: false | |
| - name: Cache the Idris2 toolchain | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: ~/.idris2 | |
| key: idris2-v${{ env.IDRIS2_VERSION }}-${{ runner.os }} | |
| - name: Install Idris2 (chez backend) | |
| working-directory: .proven-tests | |
| env: | |
| IDRIS2_VERSION: v${{ env.IDRIS2_VERSION }} | |
| run: bash scripts/install-idris2.sh | |
| - name: Type-check src/abi | |
| run: | | |
| set -euo pipefail | |
| export PATH="$HOME/.idris2/bin:$PATH" | |
| idris2 --version | |
| # `idris2 --check` can exit 0 while printing an error, so require | |
| # both a zero exit and no `Error:` line. | |
| status=0 | |
| out="$(idris2 --typecheck src/abi/panic-attack-abi.ipkg 2>&1)" || status=$? | |
| printf '%s\n' "$out" | |
| if [ "$status" -ne 0 ] || grep -q '^Error' <<<"$out"; then | |
| echo "::error::src/abi Idris2 proofs do not type-check (exit $status)" | |
| exit 1 | |
| fi | |
| framework: | |
| name: Framework — the grader is exercised (scheduled) | |
| if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 60 | |
| steps: | |
| - name: Checkout this repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Checkout proven-tests-and-benches at the pinned commit | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| repository: hyperpolymath/proven-tests-and-benches | |
| ref: ${{ env.PROVEN_TESTS_PIN }} | |
| path: .proven-tests | |
| persist-credentials: false | |
| - name: Cache the Idris2 toolchain | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: ~/.idris2 | |
| key: idris2-v${{ env.IDRIS2_VERSION }}-${{ runner.os }} | |
| - name: Install Idris2 (chez backend) | |
| working-directory: .proven-tests | |
| env: | |
| # The pinned older installer passes this verbatim to git --branch. | |
| # Idris2's release ref is v0.7.0, not 0.7.0. | |
| IDRIS2_VERSION: v${{ env.IDRIS2_VERSION }} | |
| run: bash scripts/install-idris2.sh | |
| - name: Build and run the framework's suite | |
| working-directory: .proven-tests | |
| run: | | |
| set -euo pipefail | |
| export PATH="$HOME/.idris2/bin:$PATH" | |
| idris2 --version | |
| bash scripts/ci-build.sh | |
| - name: Upload the framework's own run report | |
| if: always() | |
| uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2 | |
| with: | |
| name: proven-framework-report | |
| path: .proven-tests/build/report/*.json | |
| retention-days: 30 | |
| if-no-files-found: warn |