Repository navigation
CI/CD foundation + PR #241 consolidation (coverage, PHP, estate conformance) #14
Workflow file for this run
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 TWO JOBS DO DIFFERENT THINGS AND NEITHER PRETENDS TO BE THE OTHER | |
| # --------------------------------------------------------------------- | |
| # `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. | |
| # | |
| # 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" -- \ | |
| python3 scripts/proven/verify-ledger.py \ | |
| --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 | |
| python3 - <<'PY' | |
| import json | |
| agg = json.load(open('/tmp/proven-aggregate.json')) | |
| records = agg['proven_tests'] | |
| assert len(records) == 1, records | |
| record = records[0] | |
| assert record['defects'] == [], record['defects'] | |
| summary = record['summary'] | |
| assert summary['total'] > 0, summary | |
| print(f"proven-tests: {summary['passed']}/{summary['total']} passed, " | |
| f"{summary['covered_cells']}/{summary['cat_aspect_cells']} cells, " | |
| f"{summary['actually_proven']} actually-proven") | |
| PY | |
| - 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 | |
| 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: | |
| IDRIS2_VERSION: ${{ 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 |